Wrap lines

leanprover-community · Jan 17, 2024 · 4145626 · 4145626
1 parent 680197f
commit 4145626
Show file tree

Hide file tree

Showing 7 changed files with 18 additions and 10 deletions.
diff --git a/Mathlib/Analysis/Normed/Group/Hom.lean b/Mathlib/Analysis/Normed/Group/Hom.lean
@@ -92,7 +92,9 @@ instance toAddMonoidHomClass : AddMonoidHomClass (NormedAddGroupHom V₁ V₂) V
   map_add f := f.map_add'
   map_zero f := (AddMonoidHom.mk' f.toFun f.map_add').map_zero
 
-/-- Helper instance for when there are too many metavariables to apply `DFunLike.coeFun` directly. -/
+/--
+Helper instance for when there are too many metavariables to apply `DFunLike.coeFun` directly.
+-/
 instance coeFun : CoeFun (NormedAddGroupHom V₁ V₂) fun _ => V₁ → V₂ :=
   ⟨DFunLike.coe⟩
 

diff --git a/Mathlib/LinearAlgebra/FinsuppVectorSpace.lean b/Mathlib/LinearAlgebra/FinsuppVectorSpace.lean
@@ -79,7 +79,8 @@ protected def basis {φ : ι → Type*} (b : ∀ i, Basis (φ i) R M) : Basis (
             (b i).repr.symm (g.comapDomain _ (Set.injOn_of_injective sigma_mk_injective _))
           support := g.support.image Sigma.fst
           mem_support_toFun := fun i => by
-            rw [Ne.def, ← (b i).repr.injective.eq_iff, (b i).repr.apply_symm_apply, DFunLike.ext_iff]
+            rw [Ne.def, ← (b i).repr.injective.eq_iff, (b i).repr.apply_symm_apply,
+                DFunLike.ext_iff]
             simp only [exists_prop, LinearEquiv.map_zero, comapDomain_apply, zero_apply,
               exists_and_right, mem_support_iff, exists_eq_right, Sigma.exists, Finset.mem_image,
               not_forall] }

diff --git a/Mathlib/RingTheory/Ideal/QuotientOperations.lean b/Mathlib/RingTheory/Ideal/QuotientOperations.lean
@@ -600,7 +600,8 @@ def quotientEquivAlg (I : Ideal A) (J : Ideal B) (f : A ≃ₐ[R₁] B) (hIJ : J
   { quotientEquiv I J (f : A ≃+* B) hIJ with
     commutes' := fun r => by
       -- Porting note: Needed to add the below lemma because Equivs coerce weird
-      have : ∀ (e : RingEquiv (A ⧸ I) (B ⧸ J)), Equiv.toFun e.toEquiv = DFunLike.coe e := fun _ ↦ rfl
+      have : ∀ (e : RingEquiv (A ⧸ I) (B ⧸ J)), Equiv.toFun e.toEquiv = DFunLike.coe e :=
+        fun _ ↦ rfl
       rw [this]
       simp only [quotientEquiv_apply, RingHom.toFun_eq_coe, quotientMap_algebraMap,
       RingEquiv.coe_toRingHom, AlgEquiv.coe_ringEquiv, AlgEquiv.commutes, Quotient.mk_algebraMap]}

diff --git a/Mathlib/Topology/Algebra/Module/Basic.lean b/Mathlib/Topology/Algebra/Module/Basic.lean
@@ -710,7 +710,8 @@ theorem one_apply (x : M₁) : (1 : M₁ →L[R₁] M₁) x = x :=
 #align continuous_linear_map.one_apply ContinuousLinearMap.one_apply
 
 instance [Nontrivial M₁] : Nontrivial (M₁ →L[R₁] M₁) :=
-  ⟨0, 1, fun e ↦ have ⟨x, hx⟩ := exists_ne (0 : M₁); hx (by simpa using DFunLike.congr_fun e.symm x)⟩
+  ⟨0, 1, fun e ↦
+    have ⟨x, hx⟩ := exists_ne (0 : M₁); hx (by simpa using DFunLike.congr_fun e.symm x)⟩
 
 section Add
 

diff --git a/Mathlib/Topology/Category/CompHaus/EffectiveEpi.lean b/Mathlib/Topology/Category/CompHaus/EffectiveEpi.lean
@@ -54,8 +54,9 @@ def struct {B X : CompHaus.{u}} (π : X ⟶ B) (hπ : Function.Surjective π) :
     (by ext; exact hab)) a)
   uniq e h g hm := by
     suffices g = (QuotientMap.of_surjective_continuous hπ π.continuous).liftEquiv ⟨e,
-      fun a b hab ↦ DFunLike.congr_fun (h ⟨fun _ ↦ a, continuous_const⟩ ⟨fun _ ↦ b, continuous_const⟩
-      (by ext; exact hab)) a⟩ by assumption
+      fun a b hab ↦ DFunLike.congr_fun
+        (h ⟨fun _ ↦ a, continuous_const⟩ ⟨fun _ ↦ b, continuous_const⟩ (by ext; exact hab))
+        a⟩ by assumption
     rw [← Equiv.symm_apply_eq (QuotientMap.of_surjective_continuous hπ π.continuous).liftEquiv]
     ext
     simp only [QuotientMap.liftEquiv_symm_apply_coe, ContinuousMap.comp_apply, ← hm]

diff --git a/Mathlib/Topology/Category/Profinite/EffectiveEpi.lean b/Mathlib/Topology/Category/Profinite/EffectiveEpi.lean
@@ -52,8 +52,9 @@ def struct {B X : Profinite.{u}} (π : X ⟶ B) (hπ : Function.Surjective π) :
     (by ext; exact hab)) a)
   uniq e h g hm := by
     suffices g = (QuotientMap.of_surjective_continuous hπ π.continuous).liftEquiv ⟨e,
-      fun a b hab ↦ DFunLike.congr_fun (h ⟨fun _ ↦ a, continuous_const⟩ ⟨fun _ ↦ b, continuous_const⟩
-      (by ext; exact hab)) a⟩ by assumption
+      fun a b hab ↦ DFunLike.congr_fun
+        (h ⟨fun _ ↦ a, continuous_const⟩ ⟨fun _ ↦ b, continuous_const⟩ (by ext; exact hab))
+        a⟩ by assumption
     rw [← Equiv.symm_apply_eq (QuotientMap.of_surjective_continuous hπ π.continuous).liftEquiv]
     ext
     simp only [QuotientMap.liftEquiv_symm_apply_coe, ContinuousMap.comp_apply, ← hm]

diff --git a/Mathlib/Topology/Category/Stonean/EffectiveEpi.lean b/Mathlib/Topology/Category/Stonean/EffectiveEpi.lean
@@ -51,8 +51,9 @@ def struct {B X : Stonean.{u}} (π : X ⟶ B) (hπ : Function.Surjective π) : E
     (by ext; exact hab)) a)
   uniq e h g hm := by
     suffices g = (QuotientMap.of_surjective_continuous hπ π.continuous).liftEquiv ⟨e,
-      fun a b hab ↦ DFunLike.congr_fun (h ⟨fun _ ↦ a, continuous_const⟩ ⟨fun _ ↦ b, continuous_const⟩
-      (by ext; exact hab)) a⟩ by assumption
+      fun a b hab ↦ DFunLike.congr_fun
+        (h ⟨fun _ ↦ a, continuous_const⟩ ⟨fun _ ↦ b, continuous_const⟩ (by ext; exact hab))
+        a⟩ by assumption
     rw [← Equiv.symm_apply_eq (QuotientMap.of_surjective_continuous hπ π.continuous).liftEquiv]
     ext
     simp only [QuotientMap.liftEquiv_symm_apply_coe, ContinuousMap.comp_apply, ← hm]