style: merge "List" lines

Archive/Imo/Imo1997Q3.lean

@@ -82,12 +82,10 @@ lemma sign_eq_of_contra
       congr! 3 with j mj; rw [Perm.mul_apply, ← hi]; congr
       rw [mem_compl, mem_insert, mem_singleton, not_or] at mj
       exact swap_apply_of_ne_of_ne mj.1 mj.2
-    rw [cg, add_sub_add_right_eq_sub,
-      sum_pair castSucc_lt_succ.ne, sum_pair castSucc_lt_succ.ne,
-      Perm.mul_apply, Perm.mul_apply, ← hi, swap_apply_left, swap_apply_right,
-      add_comm, add_sub_add_comm, ← sub_mul, ← sub_mul,
-      val_succ, val_castSucc, Nat.cast_add, Nat.cast_one, add_sub_cancel_left, sub_add_cancel_left,
-      one_mul, neg_one_mul]
+    rw [cg, add_sub_add_right_eq_sub, sum_pair castSucc_lt_succ.ne, sum_pair castSucc_lt_succ.ne,
+      Perm.mul_apply, Perm.mul_apply, ← hi, swap_apply_left, swap_apply_right, add_comm,
+      add_sub_add_comm, ← sub_mul, ← sub_mul, val_succ, val_castSucc, Nat.cast_add, Nat.cast_one,
+      add_sub_cancel_left, sub_add_cancel_left, one_mul, neg_one_mul]
     calc
       _ ≤ |x (p i.succ)| + |-x (p i.castSucc)| := abs_add_le ..
       _ ≤ ((n + 1 : ℕ) + 1) / 2 + ((n + 1 : ℕ) + 1) / 2 := by

Archive/Imo/Imo2006Q5.lean

@@ -194,6 +194,5 @@ theorem imo2006_q5 {P : Polynomial ℤ} (hP : 1 < P.natDegree) {k : ℕ} (hk : 0
     simpa [Nat.iterate] using Polynomial.iterate_comp_sub_X_ne hP zero_lt_two
   replace ht := isRoot_of_mem_roots (Multiset.mem_toFinset.1 ht)
   rw [IsRoot.def, eval_sub, iterate_comp_eval, eval_X, sub_eq_zero] at ht
-  rw [Multiset.mem_toFinset, mem_roots hP', IsRoot.def, eval_sub, eval_comp, eval_X,
-    sub_eq_zero]
+  rw [Multiset.mem_toFinset, mem_roots hP', IsRoot.def, eval_sub, eval_comp, eval_X, sub_eq_zero]
   exact Polynomial.isPeriodicPt_eval_two ⟨k, hk, ht⟩

Archive/MiuLanguage/DecisionSuf.lean

@@ -115,8 +115,7 @@ theorem der_cons_replicate_I_replicate_U_append_of_der_cons_replicate_I_append (
   | succ a ha =>
     specialize ha (U :: xs)
     -- We massage the goal into a form amenable to the application of `ha`.
-    rw [replicate_add, ← append_assoc, ← cons_append, replicate_one, append_assoc,
-      singleton_append]
+    rw [replicate_add, ← append_assoc, ← cons_append, replicate_one, append_assoc, singleton_append]
     apply ha
     apply Derivable.r3
     change Derivable (↑(M :: replicate (c + 3 * a) I) ++ ↑(replicate 3 I) ++ xs)
@@ -267,8 +266,7 @@ theorem base_case_suf (en : Miustr) (h : Decstr en) (hu : count U en = 0) : Deri
   rcases h with ⟨⟨mhead, nmtail⟩, hi⟩
   have : en ≠ nil := by
     intro k
-    simp only [k, count, countP, countP.go, zero_mod, zero_ne_one, false_or,
-      reduceCtorEq] at hi
+    simp only [k, count, countP, countP.go, zero_mod, zero_ne_one, false_or, reduceCtorEq] at hi
   rcases exists_cons_of_ne_nil this with ⟨y, ys, rfl⟩
   rcases mhead
   rsuffices ⟨c, rfl, hc⟩ : ∃ c, replicate c I = ys ∧ (c % 3 = 1 ∨ c % 3 = 2)

Archive/Sensitivity.lean

@@ -128,8 +128,7 @@ theorem adj_iff_proj_adj {p q : Q n.succ} (h₀ : p 0 = q 0) :
   · rintro ⟨i, h_eq, h_uni⟩
     use i.succ, h_eq
     intro y hy
-    rw [← Fin.pred_inj (ha := (?ha : y ≠ 0)) (hb := (?hb : i.succ ≠ 0)),
-      Fin.pred_succ]
+    rw [← Fin.pred_inj (ha := (?ha : y ≠ 0)) (hb := (?hb : i.succ ≠ 0)), Fin.pred_succ]
     case ha =>
       contrapose hy
       rw [hy, h₀]
@@ -302,8 +301,7 @@ theorem f_matrix (p q : Q n) : |ε q (f n (e p))| = if p ∈ q.adjacent then 1 e
     all_goals
       repeat rw [Bool.cond_true]
       repeat rw [Bool.cond_false]
-      simp [hp, hq, IH, duality, abs_of_nonneg ite_nonneg, Q.adj_iff_proj_eq,
-        Q.adj_iff_proj_adj]
+      simp [hp, hq, IH, duality, abs_of_nonneg ite_nonneg, Q.adj_iff_proj_eq, Q.adj_iff_proj_adj]
 
 /-- The linear operator $g_m$ corresponding to Knuth's matrix $B_m$. -/
 noncomputable def g (m : ℕ) : V m →ₗ[ℝ] V m.succ :=

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -214,8 +214,7 @@ theorem first_vote_pos :
         count_countedSequence, count_countedSequence, one_mul, zero_mul, add_zero,
         Nat.cast_add, Nat.cast_one, mul_comm, ← div_eq_mul_inv, ENNReal.div_eq_div_iff]
       · norm_cast
-        rw [mul_comm _ (p + 1), add_right_comm, Nat.add_one_mul_choose_eq,
-          mul_comm]
+        rw [mul_comm _ (p + 1), add_right_comm, Nat.add_one_mul_choose_eq, mul_comm]
       all_goals simp [(Nat.choose_pos <| le_add_of_nonneg_right zero_le).ne']
     · simp
 

Archive/Wiedijk100Theorems/BuffonsNeedle.lean

@@ -239,9 +239,8 @@ With this lemma, in the short case, the inner integral's domain simplifies to
 lemma short_needle_inter_eq (h : l ≤ d) (θ : ℝ) :
     Set.Icc (-d / 2) (d / 2) ∩ Set.Icc (-θ.sin * l / 2) (θ.sin * l / 2) =
     Set.Icc (-θ.sin * l / 2) (θ.sin * l / 2) := by
-  rw [Set.Icc_inter_Icc, max_div_div_right zero_le_two,
-    min_div_div_right zero_le_two, neg_mul, max_neg_neg, mul_comm,
-    min_eq_right ((mul_le_of_le_one_right hl.le θ.sin_le_one).trans h)]
+  rw [Set.Icc_inter_Icc, max_div_div_right zero_le_two, min_div_div_right zero_le_two, neg_mul,
+    max_neg_neg, mul_comm, min_eq_right ((mul_le_of_le_one_right hl.le θ.sin_le_one).trans h)]
 
 include hd hBₘ hB hl in
 /--
@@ -250,9 +249,8 @@ equals `(2 * l) / (d * π)`.
 -/
 theorem buffon_short (h : l ≤ d) : ℙ[N l B] = (2 * l) * (d * π)⁻¹ := by
   simp_rw [buffon_integral d l hd B hBₘ hB, short_needle_inter_eq d l hl h _,
-    MeasureTheory.setIntegral_const, MeasureTheory.measureReal_def,
-    Real.volume_Icc, smul_eq_mul, mul_one, mul_comm (d * π)⁻¹ _,
-    mul_eq_mul_right_iff]
+    MeasureTheory.setIntegral_const, MeasureTheory.measureReal_def, Real.volume_Icc, smul_eq_mul,
+    mul_one, mul_comm (d * π)⁻¹ _, mul_eq_mul_right_iff]
   apply Or.inl
   ring_nf
   have : ∀ᵐ θ, θ ∈ Set.Icc 0 π → ENNReal.toReal (ENNReal.ofReal (θ.sin * l)) = θ.sin * l := by
@@ -328,13 +326,11 @@ include hd hBₘ hB hl in
 /-- Buffon's Needle, the long case (`d ≤ l`) -/
 theorem buffon_long (h : d ≤ l) :
     ℙ[N l B] = (2 * l) / (d * π) - 2 / (d * π) * (√(l ^ 2 - d ^ 2) + d * (d / l).arcsin) + 1 := by
-  simp only [
-    buffon_integral d l hd B hBₘ hB, MeasureTheory.integral_const, smul_eq_mul, mul_one,
+  simp only [buffon_integral d l hd B hBₘ hB, MeasureTheory.integral_const, smul_eq_mul, mul_one,
     MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter, Set.Icc_inter_Icc, Real.volume_Icc,
-    min_div_div_right zero_le_two d, max_div_div_right zero_le_two (-d),
-    div_sub_div_same, neg_mul, max_neg_neg, sub_neg_eq_add, ← mul_two,
-    mul_div_cancel_right₀ (min d (Real.sin _ * l)) two_ne_zero, MeasureTheory.measureReal_def
-  ]
+    min_div_div_right zero_le_two d, max_div_div_right zero_le_two (-d), div_sub_div_same, neg_mul,
+    max_neg_neg, sub_neg_eq_add, ← mul_two,
+    mul_div_cancel_right₀ (min d (Real.sin _ * l)) two_ne_zero, MeasureTheory.measureReal_def]
   have : ∀ᵐ θ, θ ∈ Set.Icc 0 π →
       ENNReal.toReal (ENNReal.ofReal (min d (θ.sin * l))) = min d (θ.sin * l) := by
     have (θ : ℝ) (hθ : θ ∈ Set.Icc 0 π) : 0 ≤ min d (θ.sin * l) := by

Archive/Wiedijk100Theorems/FriendshipGraphs.lean

@@ -210,8 +210,7 @@ open scoped Classical in
 theorem adjMatrix_sq_mul_const_one_of_regular (hd : G.IsRegularOfDegree d) :
     G.adjMatrix R * of (fun _ _ => 1) = of (fun _ _ => (d : R)) := by
   ext x
-  simp only [← hd x, degree, adjMatrix_mul_apply, sum_const, Nat.smul_one_eq_cast,
-    of_apply]
+  simp only [← hd x, degree, adjMatrix_mul_apply, sum_const, Nat.smul_one_eq_cast, of_apply]
 
 open scoped Classical in
 theorem adjMatrix_mul_const_one_mod_p_of_regular {p : ℕ} (dmod : (d : ZMod p) = 1)
@@ -265,8 +264,7 @@ theorem false_of_three_le_degree (hd : G.IsRegularOfDegree d) (h : 3 ≤ d) : Fa
   -- but the trace is 1 mod p when computed the other way
   rw [adjMatrix_pow_mod_p_of_regular hG dmod hd hp2]
   dsimp only [Fintype.card] at Vmod
-  simp only [Matrix.trace, Matrix.diag, mul_one, nsmul_eq_mul, sum_const,
-    of_apply, Ne]
+  simp only [Matrix.trace, Matrix.diag, mul_one, nsmul_eq_mul, sum_const, of_apply, Ne]
   rw [Vmod, ← Nat.cast_one (R := ZMod (Nat.minFac (d - 1))), ZMod.natCast_eq_zero_iff,
     Nat.dvd_one, Nat.minFac_eq_one_iff]
   lia

Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean

@@ -169,8 +169,7 @@ theorem card_le_two_pow_mul_sqrt {x k : ℕ} : #(M x k) ≤ 2 ^ k * Nat.sqrt x :
   -- smaller than or equal to `k`.
   have h1 : M x k ⊆ image f K := by
     intro m hm
-    simp only [f, K, M, M₁, M₂, mem_image, Prod.exists, mem_product,
-               mem_filter, mem_range] at hm ⊢
+    simp only [f, K, M, M₁, M₂, mem_image, Prod.exists, mem_product, mem_filter, mem_range] at hm ⊢
     have hm' := m.zero_lt_succ
     obtain ⟨a, b, hab₁, hab₂⟩ := Nat.sq_mul_squarefree_of_pos' hm'
     obtain ⟨ham, hbm⟩ := Dvd.intro_left _ hab₁, Dvd.intro _ hab₁

Counterexamples/AharoniKorman.lean

@@ -840,12 +840,11 @@ lemma square_subset_above (h : (C ∩ level n).Finite) :
   -- With this pair, we can use the "base" of the square as `max a b + 1`.
   rw [eventually_atTop]
   refine ⟨max a b + 1, ?_⟩
-  simp +contextual only [sup_le_iff, embed, RelEmbedding.coe_mk,
-    Function.Embedding.coeFn_mk, Set.mem_inter_iff, and_imp, «forall», toHollom_mem_level_iff,
-    Prod.forall, Set.subset_def, Set.mem_image, Set.mem_Ici, Prod.exists, Prod.mk_le_mk,
-    Set.mem_ofPred_eq, forall_exists_index, Prod.mk.injEq,
-    toHollom_le_toHollom_iff_fixed_right, Set.mem_sdiff, and_true, ← max_add_add_right,
-    Hollom.ext_iff]
+  simp +contextual only [sup_le_iff, embed, RelEmbedding.coe_mk, Function.Embedding.coeFn_mk,
+    Set.mem_inter_iff, and_imp, «forall», toHollom_mem_level_iff, Prod.forall, Set.subset_def,
+    Set.mem_image, Set.mem_Ici, Prod.exists, Prod.mk_le_mk, Set.mem_ofPred_eq, forall_exists_index,
+    Prod.mk.injEq, toHollom_le_toHollom_iff_fixed_right, Set.mem_sdiff, and_true,
+    ← max_add_add_right, Hollom.ext_iff]
   -- After simplifying, direct calculations show the subset relation as required.
   rintro k hak hbk _ _ _ f g hkf hkg rfl rfl rfl
   constructor
@@ -1156,8 +1155,7 @@ theorem not_S_mapsTo_previous (hC : IsChain (· ≤ ·) C)
     _ ⊆ S n C \ (C ∩ level n) := ha
   -- ...and it has length `2a+1`.
   have card_F : #F = 2 * a + 1 := by
-    rw [Finset.card_image_of_injective _ (embed n).injective,
-      card_chainBetween (by lia) (by simp)]
+    rw [Finset.card_image_of_injective _ (embed n).injective, card_chainBetween (by lia) (by simp)]
     lia
   let T := {x ∈ C ∩ level (n - 1) | line x < 2 * a}
   -- Therefore, the image of `F` is within `C ∩ level (n - 1)`, and each of its points must be

Mathlib/Algebra/BigOperators/Fin.lean

@@ -525,8 +525,7 @@ lemma partialProd_contractNth {G : Type*} [Monoid G] {n : ℕ}
     simp only [Function.comp_apply, succ_succAbove_succ] at *
     rw [partialProd_succ, partialProd_succ, hi]
     rcases lt_trichotomy (i : ℕ) a with (h | h | h)
-    · rw [succAbove_of_castSucc_lt, contractNth_apply_of_lt _ _ _ _ h,
-        succAbove_of_castSucc_lt] <;>
+    · rw [succAbove_of_castSucc_lt, contractNth_apply_of_lt _ _ _ _ h, succAbove_of_castSucc_lt] <;>
       simp only [lt_def, val_castSucc, val_succ] <;>
       lia
     · rw [succAbove_of_castSucc_lt, contractNth_apply_of_eq _ _ _ _ h,
@@ -559,9 +558,8 @@ theorem inv_partialProd_mul_eq_contractNth {G : Type*} [Group G] (g : Fin (n + 1
     · assumption
     · rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
       exact le_of_lt h
-  · rwa [succAbove_of_castSucc_lt, succAbove_of_le_castSucc, partialProd_succ,
-    castSucc_succ, ← mul_assoc,
-      partialProd_right_inv, contractNth_apply_of_eq]
+  · rwa [succAbove_of_castSucc_lt, succAbove_of_le_castSucc, partialProd_succ, castSucc_succ,
+    ← mul_assoc, partialProd_right_inv, contractNth_apply_of_eq]
     · simp [le_iff_val_le_val, ← h]
     · rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
       exact le_of_eq h

Mathlib/Algebra/BigOperators/Group/Finset/Gaps.lean

@@ -56,10 +56,8 @@ theorem Finset.prod_intervalGapsWithin_mul_prod_eq_div :
     (∏ i ∈ Finset.range (k + 1),
       g (F.intervalGapsWithin h a b i).2 / g (F.intervalGapsWithin h a b i).1) *
       ∏ z ∈ F, g z.2 / g z.1 = g b / g a := by
-  rw [F.prod_eq_prod_range_intervalGapsWithin h (fun x y ↦ g y / g x), mul_comm,
-      prod_range_succ, ← mul_assoc,
-      ← prod_mul_distrib,
-      prod_congr rfl (fun _ _ ↦ div_mul_div_cancel _ _ _),
+  rw [F.prod_eq_prod_range_intervalGapsWithin h (fun x y ↦ g y / g x), mul_comm, prod_range_succ,
+      ← mul_assoc, ← prod_mul_distrib, prod_congr rfl (fun _ _ ↦ div_mul_div_cancel _ _ _),
       prod_range_div (fun i ↦ g (F.intervalGapsWithin h a b i).1)]
   simp
 

Mathlib/Algebra/BigOperators/Group/List/Basic.lean

@@ -162,8 +162,7 @@ lemma prod_range_succ' (f : ℕ → M) (n : ℕ) :
   induction l with
   | nil => rfl
   | cons i l hil =>
-    rw [List.prod_cons, hil fun x hx ↦ hl _ (mem_cons_of_mem i hx),
-      hl _ mem_cons_self, one_mul]
+    rw [List.prod_cons, hil fun x hx ↦ hl _ (mem_cons_of_mem i hx), hl _ mem_cons_self, one_mul]
 
 @[to_additive] lemma exists_mem_ne_one_of_prod_ne_one (h : l.prod ≠ 1) :
     ∃ x ∈ l, x ≠ (1 : M) := by simpa only [not_forall, exists_prop] using mt prod_eq_one h

Mathlib/Algebra/Category/CoalgCat/ComonEquivalence.lean

@@ -132,10 +132,9 @@ theorem tensorObj_comul (K L : CoalgCat R) :
       = (TensorProduct.tensorTensorTensorComm R K K L L).toLinearMap
       ∘ₗ TensorProduct.map Coalgebra.comul Coalgebra.comul := by
   rw [ofComonObjCoalgebraStruct_comul]
-  simp only [Comon.monoidal_tensorObj_comon_comul,
-    MonObj.tensorObj.mul_def, unop_comp, unop_tensorObj, unop_tensorHom,
-    BraidedCategory.unop_tensorμ, tensorμ_eq_tensorTensorTensorComm, ModuleCat.hom_comp,
-    ModuleCat.hom_ofHom]
+  simp only [Comon.monoidal_tensorObj_comon_comul, MonObj.tensorObj.mul_def, unop_comp,
+    unop_tensorObj, unop_tensorHom, BraidedCategory.unop_tensorμ, tensorμ_eq_tensorTensorTensorComm,
+    ModuleCat.hom_comp, ModuleCat.hom_ofHom]
   rfl
 
 theorem tensorHom_toLinearMap (f : M →ₗc[R] N) (g : P →ₗc[R] Q) :

Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean

@@ -90,11 +90,9 @@ noncomputable def unitIsoAux (F : C ⥤ AddCommGrpCat.{v}) [PreservesFiniteLimit
   dsimp [-Functor.comp_map, -ConcreteCategory.forget_map_eq_ofHom]
   have : F.Additive := Functor.additive_of_preserves_binary_products _
   simp only [Category.id_comp]
-  rw [Functor.obj.μ_def X (F := F ⋙ forget AddCommGrpCat), Preadditive.mul_def X,
-    Functor.comp_map, F.map_add,
-    Functor.Monoidal.μ_comp F (forget AddCommGrpCat) X X,
-    Category.assoc, ← Functor.map_comp, Preadditive.comp_add, Functor.Monoidal.μ_fst,
-    Functor.Monoidal.μ_snd]
+  rw [Functor.obj.μ_def X (F := F ⋙ forget AddCommGrpCat), Preadditive.mul_def X, Functor.comp_map,
+    F.map_add, Functor.Monoidal.μ_comp F (forget AddCommGrpCat) X X, Category.assoc,
+    ← Functor.map_comp, Preadditive.comp_add, Functor.Monoidal.μ_fst, Functor.Monoidal.μ_snd]
   ext
   -- `simp [types_tensorObj_def]` says
   simp only [types_tensorObj_def, TypeCat.Fun.toFun_apply, CategoryTheory.comp_apply,

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -183,10 +183,9 @@ instance : (free R).Monoidal :=
         dsimp
         rw [μIso_inv_freeMk, MonoidalCategory.whiskerRight_apply, μIso_inv_freeMk,
           MonoidalCategory.whiskerRight_apply, μIso_hom_freeMk_tmul_freeMk,
-          μIso_hom_freeMk_tmul_freeMk, free_map_apply,
-          CategoryTheory.associator_hom_apply, MonoidalCategory.associator_hom_apply,
-          MonoidalCategory.whiskerLeft_apply, μIso_hom_freeMk_tmul_freeMk,
-          μIso_hom_freeMk_tmul_freeMk]
+          μIso_hom_freeMk_tmul_freeMk, free_map_apply, CategoryTheory.associator_hom_apply,
+          MonoidalCategory.associator_hom_apply, MonoidalCategory.whiskerLeft_apply,
+          μIso_hom_freeMk_tmul_freeMk, μIso_hom_freeMk_tmul_freeMk]
       left_unitality := fun X ↦ by
         rw [← cancel_epi (λ_ _).inv, Iso.inv_hom_id]
         aesop

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -970,8 +970,7 @@ set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 lemma extendScalarsId_hom_app_one_tmul (M : ModuleCat R) (m : M) :
     (extendScalarsId R).hom.app M ((1 : R) ⊗ₜ m) = m := by
-  rw [← extendRestrictScalarsAdj_homEquiv_apply,
-    homEquiv_extendScalarsId]
+  rw [← extendRestrictScalarsAdj_homEquiv_apply, homEquiv_extendScalarsId]
   dsimp
 
 section
@@ -996,10 +995,9 @@ lemma homEquiv_extendScalarsComp (M : ModuleCat R₁) :
         (restrictScalars f₁₂).map ((extendRestrictScalarsAdj f₂₃).unit.app _) ≫
         (restrictScalarsComp f₁₂ f₂₃).inv.app _ := by
   dsimp [extendScalarsComp, conjugateIsoEquiv, conjugateEquiv]
-  simp only [Functor.comp_obj, Category.assoc, Category.id_comp,
-    Category.comp_id, Adjunction.comp_unit_app, Adjunction.homEquiv_unit,
-    Functor.map_comp, Adjunction.unit_naturality_assoc,
-    Adjunction.right_triangle_components]
+  simp only [Functor.comp_obj, Category.assoc, Category.id_comp, Category.comp_id,
+    Adjunction.comp_unit_app, Adjunction.homEquiv_unit, Functor.map_comp,
+    Adjunction.unit_naturality_assoc, Adjunction.right_triangle_components]
   rfl
 
 set_option backward.isDefEq.respectTransparency false in
@@ -1061,8 +1059,7 @@ lemma extendScalars_comp_id :
       (Functor.rightUnitor _).hom = 𝟙 _ := by
   ext M m
   dsimp
-  erw [extendScalarsComp_hom_app_one_tmul f₁₂ (RingHom.id R₂) M m,
-    extendScalarsId_hom_app_one_tmul]
+  erw [extendScalarsComp_hom_app_one_tmul f₁₂ (RingHom.id R₂) M m, extendScalarsId_hom_app_one_tmul]
   rfl
 
 end

Mathlib/Algebra/Category/ModuleCat/Monoidal/Adjunction.lean

@@ -61,17 +61,15 @@ noncomputable instance : (extendScalars f).Monoidal :=
         ext m
         dsimp
         rw [MonoidalCategory.leftUnitor_inv_apply]
-        erw [AlgebraTensorModule.distribBaseChange_tmul,
-          MonoidalCategory.whiskerRight_apply,
+        erw [AlgebraTensorModule.distribBaseChange_tmul, MonoidalCategory.whiskerRight_apply,
           AlgebraTensorModule.rid_tmul]
         rw [one_smul]
         rfl)
       (oplax_right_unitality := fun M ↦ by
         ext m
         dsimp
         rw [MonoidalCategory.rightUnitor_inv_apply]
-        erw [AlgebraTensorModule.distribBaseChange_tmul,
-          MonoidalCategory.whiskerLeft_apply,
+        erw [AlgebraTensorModule.distribBaseChange_tmul, MonoidalCategory.whiskerLeft_apply,
           AlgebraTensorModule.rid_tmul]
         rw [one_smul]
         rfl))
@@ -132,8 +130,7 @@ lemma restrictScalars_μ_tmul (M₁ M₂ : ModuleCat S) (m₁ : M₁) (m₂ : M
   dsimp [Adjunction.rightAdjointLaxMonoidal_μ]
   rw [extendRestrictScalarsAdj_homEquiv_apply]
   dsimp
-  rw [extendScalars_δ_tmul, tensorHom_tmul,
-    extendRestrictScalarsAdj_counit_app_apply_one_tmul,
+  rw [extendScalars_δ_tmul, tensorHom_tmul, extendRestrictScalarsAdj_counit_app_apply_one_tmul,
     extendRestrictScalarsAdj_counit_app_apply_one_tmul]
 
 end ModuleCat

Mathlib/Algebra/Category/ModuleCat/Sheaf/PullbackContinuous.lean

@@ -88,8 +88,7 @@ noncomputable def adjunction :
         intros
         dsimp [Functor.FullyFaithful.homEquiv]
         -- these erw seem difficult to remove
-        erw [Adjunction.homEquiv_naturality_left_symm,
-          Adjunction.homEquiv_naturality_left_symm]
+        erw [Adjunction.homEquiv_naturality_left_symm, Adjunction.homEquiv_naturality_left_symm]
         dsimp [pushforward_obj_val]
         simp only [Functor.map_comp, Category.assoc]
       homEquiv_naturality_right := by

Mathlib/Algebra/Category/ModuleCat/Subobject.lean

@@ -41,8 +41,7 @@ noncomputable def subobjectModule : Subobject M ≃o Submodule R M :=
             (LinearMap.range S.arrow.hom) S.arrow.hom _)
           constructor
           · simp [← LinearMap.ker_eq_bot, ker_eq_bot_of_mono]
-          · rw [← LinearMap.range_eq_top, LinearMap.range_codRestrict,
-              Submodule.comap_subtype_self]
+          · rw [← LinearMap.range_eq_top, LinearMap.range_codRestrict, Submodule.comap_subtype_self]
             exact LinearMap.mem_range_self _
         · ext x
           rfl)

Mathlib/Algebra/Category/MonCat/FilteredColimits.lean

@@ -138,8 +138,7 @@ theorem colimitMulAux_eq_of_rel_right {x y y' : Σ j, F.obj j}
       (IsFiltered.leftToMax j₂ j₃) (IsFiltered.rightToMax j₂ j₃) f g
   apply M.mk_eq
   use s, α, γ
-  simp_rw [map_mul, ← comp_apply, ← F.map_comp, h₁, h₂, h₃, F.map_comp,
-    comp_apply, hfg]
+  simp_rw [map_mul, ← comp_apply, ← F.map_comp, h₁, h₂, h₃, F.map_comp, comp_apply, hfg]
 
 /-- Multiplication in the colimit. See also `colimitMulAux`. -/
 @[to_additive /-- Addition in the colimit. See also `colimitAddAux`. -/]