From 4f0309fc7dfd2e07731434f6bb1dd6ef2e4cd85b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Martin=20Dvo=C5=99=C3=A1k?= <martin.dvorak@matfyz.cz>
Date: Thu, 3 Oct 2024 15:18:46 +0000
Subject: [PATCH] style(GroupTheory,RingTheory/Congruence/Basic): use `where`,
 fix whitespace (#17362)

---
 Mathlib/GroupTheory/Congruence/Basic.lean |  1 -
 Mathlib/RingTheory/Congruence/Basic.lean  | 18 ++++++++----------
 2 files changed, 8 insertions(+), 11 deletions(-)

diff --git a/Mathlib/GroupTheory/Congruence/Basic.lean b/Mathlib/GroupTheory/Congruence/Basic.lean
index a3011ab4ba7d6..59ad69ed64e0d 100644
--- 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
index c6c46c89d1b9b..6d8463a131488 100644
--- 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]