From def132b20b56736481b75ea5db6b95af8ab5f575 Mon Sep 17 00:00:00 2001
From: grunweg <rothgami@math.hu-berlin.de>
Date: Sat, 25 May 2024 13:23:06 +0000
Subject: [PATCH] style: remove last isolated where (#13202)

Discovered when tweaking the rewritten style linter in #13199.
---
 .../CategoryTheory/Limits/Shapes/BinaryProducts.lean | 12 ++++--------
 Mathlib/Tactic/CC/Addition.lean                      |  3 +--
 Mathlib/Topology/Homotopy/Product.lean               |  3 +--
 test/FBinop.lean                                     |  6 ++----
 4 files changed, 8 insertions(+), 16 deletions(-)

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
index 8e20373d80b86..12beabf1ac5a4 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
@@ -50,8 +50,7 @@ open WalkingPair
 
 /-- The equivalence swapping left and right.
 -/
-def WalkingPair.swap : WalkingPair ≃ WalkingPair
-    where
+def WalkingPair.swap : WalkingPair ≃ WalkingPair where
   toFun j := WalkingPair.recOn j right left
   invFun j := WalkingPair.recOn j right left
   left_inv j := by cases j; repeat rfl
@@ -80,8 +79,7 @@ theorem WalkingPair.swap_symm_apply_ff : WalkingPair.swap.symm right = left :=
 
 /-- An equivalence from `WalkingPair` to `Bool`, sometimes useful when reindexing limits.
 -/
-def WalkingPair.equivBool : WalkingPair ≃ Bool
-    where
+def WalkingPair.equivBool : WalkingPair ≃ Bool where
   toFun j := WalkingPair.recOn j true false
   -- to match equiv.sum_equiv_sigma_bool
   invFun b := Bool.recOn b right left
@@ -1012,8 +1010,7 @@ variable {C}
 
 /-- The braiding isomorphism which swaps a binary product. -/
 @[simps]
-def prod.braiding (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] : P ⨯ Q ≅ Q ⨯ P
-    where
+def prod.braiding (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] : P ⨯ Q ≅ Q ⨯ P where
   hom := prod.lift prod.snd prod.fst
   inv := prod.lift prod.snd prod.fst
 #align category_theory.limits.prod.braiding CategoryTheory.Limits.prod.braiding
@@ -1288,8 +1285,7 @@ theorem prodComparison_natural (f : A ⟶ A') (g : B ⟶ B') :
 -/
 @[simps]
 def prodComparisonNatTrans [HasBinaryProducts C] [HasBinaryProducts D] (F : C ⥤ D) (A : C) :
-    prod.functor.obj A ⋙ F ⟶ F ⋙ prod.functor.obj (F.obj A)
-    where
+    prod.functor.obj A ⋙ F ⟶ F ⋙ prod.functor.obj (F.obj A) where
   app B := prodComparison F A B
   naturality f := by simp [prodComparison_natural]
 #align category_theory.limits.prod_comparison_nat_trans CategoryTheory.Limits.prodComparisonNatTrans
diff --git a/Mathlib/Tactic/CC/Addition.lean b/Mathlib/Tactic/CC/Addition.lean
index c17759fcd77a7..46fbc6275c3ca 100644
--- a/Mathlib/Tactic/CC/Addition.lean
+++ b/Mathlib/Tactic/CC/Addition.lean
@@ -375,8 +375,7 @@ partial def mkCongrProofCore (lhs rhs : Expr) (heqProofs : Bool) : CCM Expr := d
   guard (← pureIsDefEq (← inferType lhsFn) (← inferType rhsFn))
   /- Create `r`, a proof for
         `lhsFn lhsArgs[0] ... lhsArgs[n-1] = lhsFn rhsArgs[0] ... rhsArgs[n-1]`
-     where
-        `n := lhsArgs.size` -/
+     where `n := lhsArgs.size` -/
   let some specLemma ← mkCCHCongrTheorem lhsFn lhsArgs.size | failure
   let mut kindsIt := specLemma.argKinds
   let mut lemmaArgs : Array Expr := #[]
diff --git a/Mathlib/Topology/Homotopy/Product.lean b/Mathlib/Topology/Homotopy/Product.lean
index 7fe0d069f3954..09a17a45c8bd5 100644
--- a/Mathlib/Topology/Homotopy/Product.lean
+++ b/Mathlib/Topology/Homotopy/Product.lean
@@ -61,8 +61,7 @@ variable {I A : Type*} {X : I → Type*} [∀ i, TopologicalSpace (X i)] [Topolo
 -- Porting note: this definition is already in `Topology.Homotopy.Basic`
 -- /-- The product homotopy of `homotopies` between functions `f` and `g` -/
 -- @[simps]
--- def Homotopy.pi (homotopies : ∀ i, Homotopy (f i) (g i)) : Homotopy (pi f) (pi g)
---     where
+-- def Homotopy.pi (homotopies : ∀ i, Homotopy (f i) (g i)) : Homotopy (pi f) (pi g) where
 --   toFun t i := homotopies i t
 --   map_zero_left t := by ext i; simp only [pi_eval, Homotopy.apply_zero]
 --   map_one_left t := by ext i; simp only [pi_eval, Homotopy.apply_one]
diff --git a/test/FBinop.lean b/test/FBinop.lean
index 47992b840a3f1..c3a399a8647ef 100644
--- a/test/FBinop.lean
+++ b/test/FBinop.lean
@@ -66,8 +66,7 @@ example (s : Finset α) (t : Finset β) :
 structure SubObj (X : Type _) where
   carrier : Set X
 
-instance : SetLike (SubObj X) X
-    where
+instance : SetLike (SubObj X) X where
   coe s := s.carrier
   coe_injective' p q h := by cases p; cases q; congr
 
@@ -79,8 +78,7 @@ def SubObj.prod (s : SubObj X) (t : SubObj Y) : SubObj (X × Y) where
 structure DecSubObj (X : Type _) [DecidableEq X] where
   carrier : Set X
 
-instance [DecidableEq X] : SetLike (DecSubObj X) X
-    where
+instance [DecidableEq X] : SetLike (DecSubObj X) X where
   coe s := s.carrier
   coe_injective' p q h := by cases p; cases q; congr