style(GroupTheory,RingTheory/Congruence/Basic): use where, fix whit…

…espace (#17362)
leanprover-community · Oct 3, 2024 · 4f0309f · 4f0309f
1 parent 915e456
commit 4f0309f
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 11 deletions.
diff --git a/Mathlib/GroupTheory/Congruence/Basic.lean b/Mathlib/GroupTheory/Congruence/Basic.lean
@@ -110,7 +110,6 @@ variable [Mul M] [Mul N] [Mul P] (c : Con M)
 instance : Inhabited (Con M) :=
   ⟨conGen EmptyRelation⟩
 
--- 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 (M → Prop) where

diff --git a/Mathlib/RingTheory/Congruence/Basic.lean b/Mathlib/RingTheory/Congruence/Basic.lean
@@ -67,16 +67,15 @@ section Basic
 
 variable [Add R] [Mul R] (c : RingCon R)
 
--- Porting note: upgrade to `FunLike`
 /-- A coercion from a congruence relation to its underlying binary relation. -/
-instance : FunLike (RingCon R) R (R → Prop) :=
-  { coe := fun c => c.r,
-    coe_injective' := fun x y h => by
-      rcases x with ⟨⟨x, _⟩, _⟩
-      rcases y with ⟨⟨y, _⟩, _⟩
-      congr!
-      rw [Setoid.ext_iff,(show x.Rel = y.Rel from h)]
-      simp}
+instance : FunLike (RingCon R) R (R → Prop) where
+  coe := fun c => c.r
+  coe_injective' x y h := by
+    rcases x with ⟨⟨x, _⟩, _⟩
+    rcases y with ⟨⟨y, _⟩, _⟩
+    congr!
+    rw [Setoid.ext_iff, (show x.Rel = y.Rel from h)]
+    simp
 
 theorem rel_eq_coe : c.r = c :=
   rfl
@@ -419,7 +418,6 @@ end Quotient
 The API in this section is copied from `Mathlib/GroupTheory/Congruence.lean`
 -/
 
-
 section Lattice
 
 variable [Add R] [Mul R]