chore: golf Definability (#1060)

equational_theories/Definability/Basic.lean

@@ -209,9 +209,8 @@ theorem definable_of_structural (h : L'.StructuralFrom L) : L'.DefinableFrom L :
 /-- If law L' is term-definable from L, then L' is definable from L. -/
 theorem definable_of_termDefinable (h : L'.TermDefinableFrom L) : L'.DefinableFrom L := by
   intro G M hGL
-  obtain ⟨M',h2,h3⟩ := h M hGL
-  use M', h2
-  exact h3.Definable (inst := M.FOStructure)
+  obtain ⟨M', h2, h3⟩ := h M hGL
+  exact ⟨M', h2, h3.Definable (inst := M.FOStructure)⟩
 
 end hierarchy
 
@@ -229,15 +228,16 @@ theorem TermDefinable.trans_aux {G : Type} {M M₂ M₃ : Magma G}
   intro n f
   by_cases hn : n = 2
   · subst hn
-    simp
-    eta_reduce
-    convert h₁
+    simp only [realize_functions, Magma.FOStructure_funMap']
+    exact h₁
   by_cases hn₂ : n = 0
   · subst hn₂
-    simp [MagmaLanguage, Language.withConstants, Language.sum] at f
+    simp only [withConstants, Language.sum, MagmaLanguage, constantsOn_Functions, constantsOnFunc,
+      constantsOn_Relations, OfNat.zero_ne_ofNat, ↓reduceIte] at f
     exact (isEmptyElim f)
   · exact isEmptyElim (show _ by
-      simp [MagmaLanguage, hn, hn₂, Language.withConstants, Language.sum] at f
+      simp only [withConstants, Language.sum, MagmaLanguage, constantsOn_Functions, constantsOnFunc,
+        constantsOn_Relations, hn, ↓reduceIte] at f
       exact f.elim id fun h ↦ (Equiv.equivEmpty _) ((Nat.succ_pred_eq_of_ne_zero hn₂) ▸ h)
     )
 
@@ -246,18 +246,14 @@ theorem TermDefinable.trans (h₁₂ : L₂.TermDefinableFrom L₁) (h₂₃ : L
   intro G M hGL₁
   obtain ⟨M₂,hGL₂,hA⟩ := h₁₂ M hGL₁
   obtain ⟨M₃,hGL₃,hB⟩ := h₂₃ M₂ hGL₂
-  use M₃, hGL₃
-  exact trans_aux hA hB
+  exact ⟨M₃, hGL₃, trans_aux hA hB⟩
 
 theorem TermStructural.trans (h₁₂ : L₂.TermStructuralFrom L₁) (h₂₃ : L₃.TermStructuralFrom L₂) :
     L₃.TermStructuralFrom L₁ := by
   intro G M hGL₁
   obtain ⟨M₂,hGL₂,hA1,hA2⟩ := h₁₂ M hGL₁
   obtain ⟨M₃,hGL₃,hB1,hB2⟩ := h₂₃ M₂ hGL₂
-  use M₃, hGL₃
-  constructor
-  · exact TermDefinable.trans_aux hA1 hB1
-  · exact TermDefinable.trans_aux hB2 hA2
+  exact ⟨M₃, hGL₃, TermDefinable.trans_aux hA1 hB1, TermDefinable.trans_aux hB2 hA2⟩
 
 theorem Definable.trans_aux {G : Type} {M M₂ M₃ : Magma G}
     (h₁ : @Set.Definable _ (∅:Set _) MagmaLanguage M.FOStructure _ M₂.FinArityOp.arityGraph)
@@ -268,15 +264,16 @@ theorem Definable.trans_aux {G : Type} {M M₂ M₃ : Magma G}
   intro n f
   by_cases hn : n = 2
   · subst hn
-    simp
-    eta_reduce
-    convert h₁
+    simp only [realize_functions, Magma.FOStructure_funMap']
+    exact h₁
   by_cases hn₂ : n = 0
   · subst hn₂
-    simp [MagmaLanguage, Language.withConstants, Language.sum] at f
+    simp only [withConstants, Language.sum, MagmaLanguage, constantsOn_Functions, constantsOnFunc,
+      constantsOn_Relations, OfNat.zero_ne_ofNat, ↓reduceIte] at f
     exact (isEmptyElim f)
   · exact isEmptyElim (show _ by
-      simp [MagmaLanguage, hn, hn₂, Language.withConstants, Language.sum] at f
+      simp only [withConstants, Language.sum, MagmaLanguage, constantsOn_Functions, constantsOnFunc,
+        constantsOn_Relations, hn, ↓reduceIte] at f
       exact f.elim id fun h ↦ (Equiv.equivEmpty _) ((Nat.succ_pred_eq_of_ne_zero hn₂) ▸ h)
     )
 
@@ -285,18 +282,14 @@ theorem Definable.trans (h₁₂ : L₂.DefinableFrom L₁) (h₂₃ : L₃.Defi
   intro G M hGL₁
   obtain ⟨M₂,hGL₂,hA⟩ := h₁₂ M hGL₁
   obtain ⟨M₃,hGL₃,hB⟩ := h₂₃ M₂ hGL₂
-  use M₃, hGL₃
-  exact trans_aux hA hB
+  exact ⟨M₃, hGL₃, trans_aux hA hB⟩
 
 theorem Structural.trans (h₁₂ : L₂.StructuralFrom L₁) (h₂₃ : L₃.StructuralFrom L₂) :
     L₃.StructuralFrom L₁ := by
   intro G M hGL₁
   obtain ⟨M₂,hGL₂,hA1,hA2⟩ := h₁₂ M hGL₁
   obtain ⟨M₃,hGL₃,hB1,hB2⟩ := h₂₃ M₂ hGL₂
-  use M₃, hGL₃
-  constructor
-  · exact Definable.trans_aux hA1 hB1
-  · exact Definable.trans_aux hB2 hA2
+  exact ⟨M₃, hGL₃, Definable.trans_aux hA1 hB1, Definable.trans_aux hB2 hA2⟩
 
 @[simp]
 theorem TermStructural.refl : L₁.TermStructuralFrom L₁ :=

equational_theories/Definability/Simple.lean

@@ -25,43 +25,30 @@ theorem FreeMagma.toTerm_realize {α M} (t : FreeMagma α)
 /-- Every law is TermStructural from its dual. -/
 theorem TermStructural_dual (L : NatMagmaLaw) : L.TermStructuralFrom L.dual := by
   intro G M hGL
-  use ⟨fun x y ↦ M.op y x⟩
-  constructor
+  refine ⟨⟨fun x y ↦ M.op y x⟩, ?_, ?_⟩
   · rw [← law_dual_dual L]
     exact @satisfies_dual_dual _ _ ⟨_⟩ _ hGL
-  constructor <;>
-  {
-    use Functions.apply₂ (Sum.inl ()) (Term.var 1) (Term.var 0)
-    funext
-    rfl
-  }
+  · constructor <;> exact ⟨Functions.apply₂ (Sum.inl ()) (Term.var 1) (Term.var 0), rfl⟩
 
 /-- The identity law x=x is TermDefinable from anything. This is a direct consequence of the
 fact that anything implies Eq1. -/
 theorem Equation1_termDefinableFrom_all (L : NatMagmaLaw) : Law1.TermDefinableFrom L := by
-  apply termDefinable_of_termStructural
-  apply termStructural_of_implies
-  intro
+  refine termDefinable_of_termStructural (termStructural_of_implies fun _ ↦ ?_)
   simp [Law1.models_iff, Equation1]
 
 /-- Anything is TermDefinable from Eq2. This is a direct consequence of the fact that Eq2 implies
 anything. -/
 theorem all_termDefinableFrom_Equation2 (L : NatMagmaLaw) : L.TermDefinableFrom Law2 := by
-  apply termDefinable_of_termStructural
-  apply termStructural_of_implies
+  refine termDefinable_of_termStructural (termStructural_of_implies ?_)
   simpa [implies] using Equation2_implies L
 
 /-- The left projection law is TermDefinable from anything. -/
 theorem Equation4_termDefinableFrom_all (L : NatMagmaLaw) : Law4.TermDefinableFrom L := by
   intro G M hGL
-  use ⟨fun x _ ↦ x⟩
-  constructor
+  refine ⟨⟨fun x _ ↦ x⟩, ?_, ?_⟩
   · rw [@Law4.models_iff]
-    intro x y
-    rfl
-  · use Term.var 0
-    funext
-    rfl
+    exact fun _ _ => rfl
+  · exact ⟨Term.var 0, rfl⟩
 
 /-- The right projection law is TermDefinable from anything. -/
 theorem Equation5_termDefinableFrom_all (L : NatMagmaLaw) : Law5.TermDefinableFrom L :=

equational_theories/Definability/Tarski543.lean

@@ -62,8 +62,7 @@ def CommSemigroupOf543 [Magma M] (h : Equation543 M) : CommSemigroup M :=
   have h4369 : ∀_,_ := Equation543_implies_Equation4369 h -- (1.3)
   have h11 : ∀_,_ := Equation543_implies_Equation11 h
   have h40 : ∀_,_ := Equation543_implies_Equation40 h
-  have hcomm' (x y : M) : x ◇ ((x ◇ x) ◇ y) = y ◇ ((y ◇ y) ◇ x) := by
-    rw [← h4369, h40]
+  have hcomm' (x y : M) : x ◇ ((x ◇ x) ◇ y) = y ◇ ((y ◇ y) ◇ x) := by rw [← h4369, h40]
   have hcomm (x y : M) : x * y = y * x :=
     hcomm' x y
   {
@@ -144,11 +143,9 @@ private lemma groupDef {M : Type*} [op : Magma M] (h : Equation543 M) :
   have h16 : ∀_,_ := Equation543_implies_Equation16 h
   have h3823 : ∀_,_ := Equation543_implies_Equation3823 h
   have h4369 : ∀_,_ := Equation543_implies_Equation4369 h
-  constructor
-  · intro h1
-    rw [← h1, ← h3823, ← h16]
-  · intro h1
-    rw [h16 y (z ◇ z), h1, h4369, ← h3823, h4369, h4369 _ _ y, ← h16, ← h3823, ← h11]
+  constructor <;> intro h1
+  · rw [← h1, ← h3823, ← h16]
+  · rw [h16 y (z ◇ z), h1, h4369, ← h3823, h4369, h4369 _ _ y, ← h16, ← h3823, ← h11]
 
 /-- Commuative structure, Equation 43, is given by a term from any magma obeying Tarski's
 one-equation abelian group subtraction law, Equation 543. -/