From 55eb81242f484e2dcd21da1fece398065f8de1db Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 27 Nov 2023 09:11:38 +0000
Subject: [PATCH] chore(GroupTheory/Congruence): small cleanups (#8314)

Switches to `where` notation in a couple of places and removes a default `lt` field.

Also replaces uses of `.r` with `coeFn`, since the latter is declared simp-normal by this file.
---
 Mathlib/GroupTheory/Congruence.lean | 105 +++++++++++++---------------
 Mathlib/GroupTheory/CoprodI.lean    |   2 +-
 2 files changed, 50 insertions(+), 57 deletions(-)

diff --git a/Mathlib/GroupTheory/Congruence.lean b/Mathlib/GroupTheory/Congruence.lean
index 6a6b88ae91f20..dfdf33111e291 100644
--- a/Mathlib/GroupTheory/Congruence.lean
+++ b/Mathlib/GroupTheory/Congruence.lean
@@ -121,13 +121,13 @@ instance : Inhabited (Con M) :=
 --Porting note: upgraded to FunLike
 /-- A coercion from a congruence relation to its underlying binary relation. -/
 @[to_additive "A coercion from an additive congruence relation to its underlying binary relation."]
-instance : FunLike (Con M) M (fun _ => M → Prop) :=
-  { coe := fun c => fun x y => @Setoid.r _ c.toSetoid x y
-    coe_injective' := fun x y h => by
-      rcases x with ⟨⟨x, _⟩, _⟩
-      rcases y with ⟨⟨y, _⟩, _⟩
-      have : x = y := h
-      subst x; rfl }
+instance : FunLike (Con M) M (fun _ => M → Prop) where
+  coe c := c.r
+  coe_injective' := fun x y h => by
+    rcases x with ⟨⟨x, _⟩, _⟩
+    rcases y with ⟨⟨y, _⟩, _⟩
+    have : x = y := h
+    subst x; rfl
 
 @[to_additive (attr := simp)]
 theorem rel_eq_coe (c : Con M) : c.r = c :=
@@ -178,11 +178,7 @@ variable {c}
 /-- The map sending a congruence relation to its underlying binary relation is injective. -/
 @[to_additive "The map sending an additive congruence relation to its underlying binary relation
 is injective."]
-theorem ext' {c d : Con M} (H : c.r = d.r) : c = d := by
-  rcases c with ⟨⟨⟩⟩
-  rcases d with ⟨⟨⟩⟩
-  cases H
-  congr
+theorem ext' {c d : Con M} (H : ⇑c = ⇑d) : c = d := FunLike.coe_injective H
 #align con.ext' Con.ext'
 #align add_con.ext' AddCon.ext'
 
@@ -211,10 +207,9 @@ theorem ext_iff {c d : Con M} : (∀ x y, c x y ↔ d x y) ↔ c = d :=
 /-- Two congruence relations are equal iff their underlying binary relations are equal. -/
 @[to_additive "Two additive congruence relations are equal iff their underlying binary relations
 are equal."]
-theorem ext'_iff {c d : Con M} : c.r = d.r ↔ c = d :=
-  ⟨ext', fun h => h ▸ rfl⟩
-#align con.ext'_iff Con.ext'_iff
-#align add_con.ext'_iff AddCon.ext'_iff
+theorem coe_inj {c d : Con M} : ⇑c = ⇑d ↔ c = d := FunLike.coe_injective.eq_iff
+#align con.ext'_iff Con.coe_inj
+#align add_con.ext'_iff AddCon.coe_inj
 
 /-- The kernel of a multiplication-preserving function as a congruence relation. -/
 @[to_additive "The kernel of an addition-preserving function as an additive congruence relation."]
@@ -413,8 +408,8 @@ protected def congr {c d : Con M} (h : c = d) : c.Quotient ≃* d.Quotient :=
     `x` is related to `y` by `d` if `x` is related to `y` by `c`. -/
 @[to_additive "For additive congruence relations `c, d` on a type `M` with an addition, `c ≤ d` iff
 `∀ x y ∈ M`, `x` is related to `y` by `d` if `x` is related to `y` by `c`."]
-instance : LE (Con M) :=
-  ⟨fun c d => ∀ ⦃x y⦄, c x y → d x y⟩
+instance : LE (Con M) where
+  le c d := ∀ ⦃x y⦄, c x y → d x y
 
 /-- Definition of `≤` for congruence relations. -/
 @[to_additive "Definition of `≤` for additive congruence relations."]
@@ -426,12 +421,12 @@ theorem le_def {c d : Con M} : c ≤ d ↔ ∀ {x y}, c x y → d x y :=
 /-- The infimum of a set of congruence relations on a given type with a multiplication. -/
 @[to_additive "The infimum of a set of additive congruence relations on a given type with
 an addition."]
-instance : InfSet (Con M) :=
-  ⟨fun S =>
-    ⟨⟨fun x y => ∀ c : Con M, c ∈ S → c x y,
-        ⟨fun x c _ => c.refl x, fun h c hc => c.symm <| h c hc, fun h1 h2 c hc =>
-          c.trans (h1 c hc) <| h2 c hc⟩⟩,
-      fun h1 h2 c hc => c.mul (h1 c hc) <| h2 c hc⟩⟩
+instance : InfSet (Con M) where
+  sInf S :=
+    { r := fun x y => ∀ c : Con M, c ∈ S → c x y
+      iseqv := ⟨fun x c _ => c.refl x, fun h c hc => c.symm <| h c hc,
+        fun h1 h2 c hc => c.trans (h1 c hc) <| h2 c hc⟩
+      mul' := fun h1 h2 c hc => c.mul (h1 c hc) <| h2 c hc }
 
 /-- The infimum of a set of congruence relations is the same as the infimum of the set's image
     under the map to the underlying equivalence relation. -/
@@ -445,51 +440,49 @@ theorem sInf_toSetoid (S : Set (Con M)) : (sInf S).toSetoid = sInf (toSetoid ''
 
 /-- The infimum of a set of congruence relations is the same as the infimum of the set's image
     under the map to the underlying binary relation. -/
-@[to_additive "The infimum of a set of additive congruence relations is the same as the infimum
-of the set's image under the map to the underlying binary relation."]
-theorem sInf_def (S : Set (Con M)) :
-    ⇑(sInf S) = sInf (@Set.image (Con M) (M → M → Prop) (↑) S) := by
+@[to_additive (attr := simp, norm_cast)
+  "The infimum of a set of additive congruence relations is the same as the infimum
+  of the set's image under the map to the underlying binary relation."]
+theorem coe_sInf (S : Set (Con M)) :
+    ⇑(sInf S) = sInf ((⇑) '' S) := by
   ext
   simp only [sInf_image, iInf_apply, iInf_Prop_eq]
   rfl
-#align con.Inf_def Con.sInf_def
-#align add_con.Inf_def AddCon.sInf_def
+#align con.Inf_def Con.coe_sInf
+#align add_con.Inf_def AddCon.coe_sInf
 
 @[to_additive]
 instance : PartialOrder (Con M) where
-  le := (· ≤ ·)
-  lt c d := c ≤ d ∧ ¬d ≤ c
   le_refl _ _ _ := id
   le_trans _ _ _ h1 h2 _ _ h := h2 <| h1 h
-  lt_iff_le_not_le _ _ := Iff.rfl
   le_antisymm _ _ hc hd := ext fun _ _ => ⟨fun h => hc h, fun h => hd h⟩
 
 /-- The complete lattice of congruence relations on a given type with a multiplication. -/
 @[to_additive "The complete lattice of additive congruence relations on a given type with
 an addition."]
-instance : CompleteLattice (Con M) :=
-  { (completeLatticeOfInf (Con M)) fun s =>
+instance : CompleteLattice (Con M) where
+  __ := completeLatticeOfInf (Con M) fun s =>
       ⟨fun r hr x y h => (h : ∀ r ∈ s, (r : Con M) x y) r hr, fun r hr x y h r' hr' =>
         hr hr'
-          h⟩ with
-    inf := fun c d =>
-      ⟨c.toSetoid ⊓ d.toSetoid, fun h1 h2 => ⟨c.mul h1.1 h2.1, d.mul h1.2 h2.2⟩⟩
-    inf_le_left := fun _ _ _ _ h => h.1
-    inf_le_right := fun _ _ _ _ h => h.2
-    le_inf := fun _ _ _ hb hc _ _ h => ⟨hb h, hc h⟩
-    top := { Setoid.completeLattice.top with mul' := by tauto }
-    le_top := fun _ _ _ _ => trivial
-    bot := { Setoid.completeLattice.bot with mul' := fun h1 h2 => h1 ▸ h2 ▸ rfl }
-    bot_le := fun c x y h => h ▸ c.refl x }
+          h⟩
+  inf c d := ⟨c.toSetoid ⊓ d.toSetoid, fun h1 h2 => ⟨c.mul h1.1 h2.1, d.mul h1.2 h2.2⟩⟩
+  inf_le_left _ _ := fun _ _ h => h.1
+  inf_le_right _ _ := fun _ _ h => h.2
+  le_inf  _ _ _ hb hc := fun _ _ h => ⟨hb h, hc h⟩
+  top := { Setoid.completeLattice.top with mul' := by tauto }
+  le_top _ := fun _ _ _ => trivial
+  bot := { Setoid.completeLattice.bot with mul' := fun h1 h2 => h1 ▸ h2 ▸ rfl }
+  bot_le c := fun x y h => h ▸ c.refl x
 
 /-- The infimum of two congruence relations equals the infimum of the underlying binary
     operations. -/
-@[to_additive "The infimum of two additive congruence relations equals the infimum of the
-underlying binary operations."]
-theorem inf_def {c d : Con M} : (c ⊓ d).r = c.r ⊓ d.r :=
+@[to_additive (attr := simp, norm_cast)
+  "The infimum of two additive congruence relations equals the infimum of the underlying binary
+  operations."]
+theorem coe_inf {c d : Con M} : ⇑(c ⊓ d) = ⇑c ⊓ ⇑d :=
   rfl
-#align con.inf_def Con.inf_def
-#align add_con.inf_def AddCon.inf_def
+#align con.inf_def Con.coe_inf
+#align add_con.inf_def AddCon.coe_inf
 
 /-- Definition of the infimum of two congruence relations. -/
 @[to_additive "Definition of the infimum of two additive congruence relations."]
@@ -505,9 +498,9 @@ containing a binary relation `r` equals the infimum of the set of additive congr
 containing `r`."]
 theorem conGen_eq (r : M → M → Prop) : conGen r = sInf { s : Con M | ∀ x y, r x y → s x y } :=
   le_antisymm
-    (le_sInf (fun s hs x y (hxy : (conGen r).r x y) =>
-      show s.r x y by
-        apply ConGen.Rel.recOn (motive := fun x y _ => s.r x y) hxy
+    (le_sInf (fun s hs x y (hxy : (conGen r) x y) =>
+      show s x y by
+        apply ConGen.Rel.recOn (motive := fun x y _ => s x y) hxy
         · exact fun x y h => hs x y h
         · exact s.refl'
         · exact fun _ => s.symm'
@@ -521,7 +514,7 @@ theorem conGen_eq (r : M → M → Prop) : conGen r = sInf { s : Con M | ∀ x y
     congruence relation containing `r`. -/
 @[to_additive addConGen_le "The smallest additive congruence relation containing a binary
 relation `r` is contained in any additive congruence relation containing `r`."]
-theorem conGen_le {r : M → M → Prop} {c : Con M} (h : ∀ x y, r x y → @Setoid.r _ c.toSetoid x y) :
+theorem conGen_le {r : M → M → Prop} {c : Con M} (h : ∀ x y, r x y → c x y) :
     conGen r ≤ c := by rw [conGen_eq]; exact sInf_le h
 #align con.con_gen_le Con.conGen_le
 #align add_con.add_con_gen_le AddCon.addConGen_le
@@ -571,7 +564,7 @@ theorem sup_eq_conGen (c d : Con M) : c ⊔ d = conGen fun x y => c x y ∨ d x
     the supremum of the underlying binary operations. -/
 @[to_additive "The supremum of two additive congruence relations equals the smallest additive
 congruence relation containing the supremum of the underlying binary operations."]
-theorem sup_def {c d : Con M} : c ⊔ d = conGen (c.r ⊔ d.r) := by rw [sup_eq_conGen]; rfl
+theorem sup_def {c d : Con M} : c ⊔ d = conGen (⇑c ⊔ ⇑d) := by rw [sup_eq_conGen]; rfl
 #align con.sup_def Con.sup_def
 #align add_con.sup_def AddCon.sup_def
 
@@ -596,7 +589,7 @@ theorem sSup_eq_conGen (S : Set (Con M)) :
 additive congruence relation containing the supremum of the set's image under the map to the
 underlying binary relation."]
 theorem sSup_def {S : Set (Con M)} :
-    sSup S = conGen (sSup (@Set.image (Con M) (M → M → Prop) ((⇑) : Con M → M → M → Prop) S)) := by
+    sSup S = conGen (sSup ((⇑) '' S)) := by
   rw [sSup_eq_conGen, sSup_image]
   congr with (x y)
   simp only [sSup_image, iSup_apply, iSup_Prop_eq, exists_prop, rel_eq_coe]
diff --git a/Mathlib/GroupTheory/CoprodI.lean b/Mathlib/GroupTheory/CoprodI.lean
index 89b835c227d00..8722cd4736ff6 100644
--- a/Mathlib/GroupTheory/CoprodI.lean
+++ b/Mathlib/GroupTheory/CoprodI.lean
@@ -152,7 +152,7 @@ def lift : (∀ i, M i →* N) ≃ (CoprodI M →* N) where
   toFun fi :=
     Con.lift _ (FreeMonoid.lift fun p : Σi, M i => fi p.fst p.snd) <|
       Con.conGen_le <| by
-        simp_rw [Con.rel_eq_coe, Con.ker_rel]
+        simp_rw [Con.ker_rel]
         rintro _ _ (i | ⟨x, y⟩)
         · change FreeMonoid.lift _ (FreeMonoid.of _) = FreeMonoid.lift _ 1
           simp only [MonoidHom.map_one, FreeMonoid.lift_eval_of]