chore(*): split some long lines (#5997)

src/algebra/group_power/lemmas.lean

@@ -407,7 +407,8 @@ by simpa only [add_sub_cancel'_right] using one_add_mul_le_pow this n
 end linear_ordered_ring
 
 /-- Bernoulli's inequality reformulated to estimate `(n : K)`. -/
-theorem nat.cast_le_pow_sub_div_sub {K : Type*} [linear_ordered_field K] {a : K} (H : 1 < a) (n : ℕ) :
+theorem nat.cast_le_pow_sub_div_sub {K : Type*} [linear_ordered_field K] {a : K} (H : 1 < a)
+  (n : ℕ) :
   (n : K) ≤ (a ^ n - 1) / (a - 1) :=
 (le_div_iff (sub_pos.2 H)).2 $ le_sub_left_of_add_le $
   one_add_mul_sub_le_pow ((neg_le_self $ @zero_le_one K _).trans H.le) _
@@ -584,7 +585,8 @@ section
 
 variables [semiring R] {a x y : R}
 
-@[simp] lemma cast_nat_mul_right (h : semiconj_by a x y) (n : ℕ) : semiconj_by a ((n : R) * x) (n * y) :=
+@[simp] lemma cast_nat_mul_right (h : semiconj_by a x y) (n : ℕ) :
+  semiconj_by a ((n : R) * x) (n * y) :=
 semiconj_by.mul_right (nat.commute_cast _ _) h
 
 @[simp] lemma cast_nat_mul_left (h : semiconj_by a x y) (n : ℕ) : semiconj_by ((n : R) * a) x y :=

src/algebra/group_with_zero/power.lean

@@ -150,7 +150,8 @@ theorem commute.fpow_self (a : G₀) (n : ℤ) : commute (a^n) a := (commute.ref
 
 theorem commute.self_fpow (a : G₀) (n : ℤ) : commute a (a^n) := (commute.refl a).fpow_right n
 
-theorem commute.fpow_fpow_self (a : G₀) (m n : ℤ) : commute (a^m) (a^n) := (commute.refl a).fpow_fpow m n
+theorem commute.fpow_fpow_self (a : G₀) (m n : ℤ) : commute (a^m) (a^n) :=
+(commute.refl a).fpow_fpow m n
 
 theorem fpow_bit0 (a : G₀) (n : ℤ) : a ^ bit0 n = a ^ n * a ^ n :=
 begin

src/algebraic_geometry/locally_ringed_space.lean

@@ -13,9 +13,9 @@ import ring_theory.ideal.basic
 /-!
 # The category of locally ringed spaces
 
-We define (bundled) locally ringed spaces
-(as `SheafedSpace CommRing` along with the fact that the stalks are local rings),
-and morphisms between these (morphisms in `SheafedSpace` with `is_local_ring_hom` on the stalk maps).
+We define (bundled) locally ringed spaces (as `SheafedSpace CommRing` along with the fact that the
+stalks are local rings), and morphisms between these (morphisms in `SheafedSpace` with
+`is_local_ring_hom` on the stalk maps).
 
 ## Future work
 * Define the restriction along an open embedding
@@ -62,7 +62,8 @@ def 𝒪 : sheaf CommRing X.to_Top := X.to_SheafedSpace.sheaf
 /-- A morphism of locally ringed spaces is a morphism of ringed spaces
  such that the morphims induced on stalks are local ring homomorphisms. -/
 def hom (X Y : LocallyRingedSpace) : Type* :=
-{ f : X.to_SheafedSpace ⟶ Y.to_SheafedSpace // ∀ x, is_local_ring_hom (PresheafedSpace.stalk_map f x) }
+{ f : X.to_SheafedSpace ⟶ Y.to_SheafedSpace //
+    ∀ x, is_local_ring_hom (PresheafedSpace.stalk_map f x) }
 
 instance : has_hom LocallyRingedSpace := ⟨hom⟩
 

src/analysis/convex/extrema.lean

@@ -47,7 +47,7 @@ begin
       ... ≤ ya • f a + yx • f x
                 : h_conv.2 (left_mem_Icc.mpr (le_of_lt a_lt_b)) ⟨h_ax, h_xb⟩ (ya_pos)
                     (le_of_lt yx_pos) yax
-      ... < ya • f a + yx • f a       : add_lt_add_left (smul_lt_smul_of_pos fx_lt_fa yx_pos) (ya • f a)
+      ... < ya • f a + yx • f a       : add_lt_add_left (smul_lt_smul_of_pos fx_lt_fa yx_pos) _
       ... = f a                       : by rw [←add_smul, yax, one_smul] },
   by_cases h_xz : x ≤ z,
   { exact not_lt_of_ge (ge_on_nhd x (show x ∈ Icc a z, by exact ⟨h_ax, h_xz⟩)) fx_lt_fa, },

src/category_theory/adjunction/limits.lean

@@ -47,7 +47,8 @@ The counit for the adjunction for `cocones.functoriality K F : cocone K ⥤ coco
 
 Auxiliary definition for `functoriality_is_left_adjoint`.
 -/
-@[simps] def functoriality_counit : functoriality_right_adjoint adj K ⋙ cocones.functoriality _ F ⟶ 𝟭 (cocone (K ⋙ F)) :=
+@[simps] def functoriality_counit :
+  functoriality_right_adjoint adj K ⋙ cocones.functoriality _ F ⟶ 𝟭 (cocone (K ⋙ F)) :=
 { app := λ c, { hom := adj.counit.app c.X } }
 
 /-- The functor `cocones.functoriality K F : cocone K ⥤ cocone (K ⋙ F)` is a left adjoint. -/
@@ -134,15 +135,17 @@ The unit for the adjunction for`cones.functoriality K G : cone K ⥤ cone (K ⋙
 
 Auxiliary definition for `functoriality_is_right_adjoint`.
 -/
-@[simps] def functoriality_unit' : 𝟭 (cone (K ⋙ G)) ⟶ functoriality_left_adjoint adj K ⋙ cones.functoriality _ G :=
+@[simps] def functoriality_unit' :
+  𝟭 (cone (K ⋙ G)) ⟶ functoriality_left_adjoint adj K ⋙ cones.functoriality _ G :=
 { app := λ c, { hom := adj.unit.app c.X, } }
 
 /--
 The counit for the adjunction for`cones.functoriality K G : cone K ⥤ cone (K ⋙ G)`.
 
 Auxiliary definition for `functoriality_is_right_adjoint`.
 -/
-@[simps] def functoriality_counit' : cones.functoriality _ G ⋙ functoriality_left_adjoint adj K ⟶ 𝟭 (cone K) :=
+@[simps] def functoriality_counit' :
+  cones.functoriality _ G ⋙ functoriality_left_adjoint adj K ⟶ 𝟭 (cone K) :=
 { app := λ c, { hom := adj.counit.app c.X, } }
 
 /-- The functor `cones.functoriality K G : cone K ⥤ cone (K ⋙ G)` is a right adjoint. -/

src/category_theory/limits/shapes/zero.lean

@@ -64,7 +64,8 @@ variables {C}
 
 /-- This lemma will be immediately superseded by `ext`, below. -/
 private lemma ext_aux (I J : has_zero_morphisms C)
-  (w : ∀ X Y : C, (@has_zero_morphisms.has_zero _ _ I X Y).zero = (@has_zero_morphisms.has_zero _ _ J X Y).zero) : I = J :=
+  (w : ∀ X Y : C, (@has_zero_morphisms.has_zero _ _ I X Y).zero =
+    (@has_zero_morphisms.has_zero _ _ J X Y).zero) : I = J :=
 begin
   casesI I, casesI J,
   congr,
@@ -121,7 +122,8 @@ variables [has_zero_morphisms C] [has_zero_morphisms D]
 lemma equivalence_preserves_zero_morphisms (F : C ≌ D) (X Y : C) :
   F.functor.map (0 : X ⟶ Y) = (0 : F.functor.obj X ⟶ F.functor.obj Y) :=
 begin
-  have t : F.functor.map (0 : X ⟶ Y) = F.functor.map (0 : X ⟶ Y) ≫ (0 : F.functor.obj Y ⟶ F.functor.obj Y),
+  have t : F.functor.map (0 : X ⟶ Y) =
+    F.functor.map (0 : X ⟶ Y) ≫ (0 : F.functor.obj Y ⟶ F.functor.obj Y),
   { apply faithful.map_injective (F.inverse),
     rw [functor.map_comp, equivalence.inv_fun_map],
     dsimp,
@@ -268,7 +270,8 @@ the identities on both `X` and `Y` are zero.
 -/
 @[simps]
 def is_iso_zero_equiv (X Y : C) : is_iso (0 : X ⟶ Y) ≃ (𝟙 X = 0 ∧ 𝟙 Y = 0) :=
-{ to_fun := begin introsI i, rw ←is_iso.hom_inv_id (0 : X ⟶ Y), rw ←is_iso.inv_hom_id (0 : X ⟶ Y), simp, end,
+{ to_fun := by { introsI i, rw ←is_iso.hom_inv_id (0 : X ⟶ Y),
+    rw ←is_iso.inv_hom_id (0 : X ⟶ Y), simp },
   inv_fun := λ h, { inv := (0 : Y ⟶ X), },
   left_inv := by tidy,
   right_inv := by tidy, }

src/data/nat/cast.lean

@@ -115,7 +115,8 @@ eq_sub_of_add_eq $ by rw [← cast_add, nat.sub_add_cancel h]
 | (n+1) := (cast_add _ _).trans $
 show ((m * n : ℕ) : α) + m = m * (n + 1), by rw [cast_mul n, left_distrib, mul_one]
 
-@[simp] theorem cast_dvd {α : Type*} [field α] {m n : ℕ} (n_dvd : n ∣ m) (n_nonzero : (n:α) ≠ 0) : ((m / n : ℕ) : α) = m / n :=
+@[simp] theorem cast_dvd {α : Type*} [field α] {m n : ℕ} (n_dvd : n ∣ m) (n_nonzero : (n:α) ≠ 0) :
+  ((m / n : ℕ) : α) = m / n :=
 begin
   rcases n_dvd with ⟨k, rfl⟩,
   have : n ≠ 0, {rintro rfl, simpa using n_nonzero},

src/data/qpf/multivariate/constructions/cofix.lean

@@ -296,13 +296,15 @@ end
 lemma cofix.dest_mk {α : typevec n} (x : F (α.append1 $ cofix F α)) : cofix.dest (cofix.mk x) = x :=
 begin
   have : cofix.mk ∘ cofix.dest = @_root_.id (cofix F α) := funext cofix.mk_dest,
-  rw [cofix.mk, cofix.dest_corec, ←comp_map, ←cofix.mk, ← append_fun_comp, this, id_comp, append_fun_id_id, mvfunctor.id_map]
+  rw [cofix.mk, cofix.dest_corec, ←comp_map, ←cofix.mk, ← append_fun_comp, this, id_comp,
+    append_fun_id_id, mvfunctor.id_map]
 end
 
 lemma cofix.ext {α : typevec n} (x y : cofix F α) (h : x.dest = y.dest) : x = y :=
 by rw [← cofix.mk_dest x,h,cofix.mk_dest]
 
-lemma cofix.ext_mk {α : typevec n} (x y : F (α ::: cofix F α)) (h : cofix.mk x = cofix.mk  y) : x = y :=
+lemma cofix.ext_mk {α : typevec n} (x y : F (α ::: cofix F α)) (h : cofix.mk x = cofix.mk  y) :
+  x = y :=
 by rw [← cofix.dest_mk x,h,cofix.dest_mk]
 
 /-!

src/deprecated/group.lean

@@ -38,8 +38,8 @@ is_group_hom, is_monoid_hom, monoid_hom
 
 /--
 We have lemmas stating that the composition of two morphisms is again a morphism.
-Since composition is reducible, type class inference will always succeed in applying these instances.
-For example when the goal is just `⊢ is_mul_hom f` the instance `is_mul_hom.comp`
+Since composition is reducible, type class inference will always succeed in applying these
+instances. For example when the goal is just `⊢ is_mul_hom f` the instance `is_mul_hom.comp`
 will still succeed, unifying `f` with `f ∘ (λ x, x)`.  This causes type class inference to loop.
 To avoid this, we do not make these lemmas instances.
 -/

src/deprecated/ring.lean

@@ -8,8 +8,8 @@ import deprecated.group
 /-!
 # Unbundled semiring and ring homomorphisms (deprecated)
 
-This file defines typeclasses for unbundled semiring and ring homomorphisms. Though these classes are
-deprecated, they are still widely used in mathlib, and probably will not go away before Lean 4
+This file defines typeclasses for unbundled semiring and ring homomorphisms. Though these classes
+are deprecated, they are still widely used in mathlib, and probably will not go away before Lean 4
 because Lean 3 often fails to coerce a bundled homomorphism to a function.
 
 ## main definitions

src/deprecated/subgroup.lean

@@ -70,7 +70,8 @@ local attribute [instance] subtype.group subtype.add_group
 lemma is_subgroup.coe_inv {s : set G} [is_subgroup s] (a : s) : ((a⁻¹ : s) : G) = a⁻¹ := rfl
 attribute [norm_cast] is_add_subgroup.coe_neg
 
-@[simp, norm_cast] lemma is_subgroup.coe_gpow {s : set G} [is_subgroup s] (a : s) (n : ℤ) : ((a ^ n : s) : G) = a ^ n :=
+@[simp, norm_cast] lemma is_subgroup.coe_gpow {s : set G} [is_subgroup s] (a : s) (n : ℤ) :
+  ((a ^ n : s) : G) = a ^ n :=
 by induction n; simp [is_submonoid.coe_pow a]
 
 @[simp, norm_cast] lemma is_add_subgroup.gsmul_coe {s : set A} [is_add_subgroup s] (a : s) (n : ℤ) :
@@ -137,7 +138,8 @@ lemma is_subgroup.gpow_mem {a : G} {s : set G} [is_subgroup s] (h : a ∈ s) : 
 | (n : ℕ) := is_submonoid.pow_mem h
 | -[1+ n] := is_subgroup.inv_mem (is_submonoid.pow_mem h)
 
-lemma is_add_subgroup.gsmul_mem {a : A} {s : set A} [is_add_subgroup s] : a ∈ s → ∀{i:ℤ}, gsmul i a ∈ s :=
+lemma is_add_subgroup.gsmul_mem {a : A} {s : set A} [is_add_subgroup s] :
+  a ∈ s → ∀{i:ℤ}, gsmul i a ∈ s :=
 @is_subgroup.gpow_mem (multiplicative A) _ _ _ (multiplicative.is_subgroup _)
 
 lemma gpowers_subset {a : G} {s : set G} [is_subgroup s] (h : a ∈ s) : gpowers a ⊆ s :=
@@ -552,12 +554,14 @@ theorem closure_eq_mclosure {s : set G} : closure s = monoid.closure (s ∪ has_
 set.subset.antisymm
   (@closure_subset _ _ _ (monoid.closure (s ∪ has_inv.inv ⁻¹' s))
     { inv_mem := λ x hx, monoid.in_closure.rec_on hx
-      (λ x hx, or.cases_on hx (λ hx, monoid.subset_closure $ or.inr $ show x⁻¹⁻¹ ∈ s, from (inv_inv x).symm ▸ hx)
+      (λ x hx, or.cases_on hx (λ hx, monoid.subset_closure $ or.inr $
+        show x⁻¹⁻¹ ∈ s, from (inv_inv x).symm ▸ hx)
         (λ hx, monoid.subset_closure $ or.inl hx))
       ((@one_inv G _).symm ▸ is_submonoid.one_mem)
       (λ x y hx hy ihx ihy, (mul_inv_rev x y).symm ▸ is_submonoid.mul_mem ihy ihx) }
     (set.subset.trans (set.subset_union_left _ _) monoid.subset_closure))
-  (monoid.closure_subset $ set.union_subset subset_closure $ λ x hx, inv_inv x ▸ (is_subgroup.inv_mem $ subset_closure hx))
+  (monoid.closure_subset $ set.union_subset subset_closure $
+    λ x hx, inv_inv x ▸ (is_subgroup.inv_mem $ subset_closure hx))
 
 @[to_additive]
 theorem mem_closure_union_iff {G : Type*} [comm_group G] {s t : set G} {x : G} :

src/field_theory/algebraic_closure.lean

@@ -63,7 +63,8 @@ theorem of_exists_root (H : ∀ p : polynomial k, p.monic → irreducible p →
  let ⟨x, hx⟩ := H (q * C (leading_coeff q)⁻¹) (monic_mul_leading_coeff_inv hq.ne_zero) this in
  degree_mul_leading_coeff_inv q hq.ne_zero ▸ degree_eq_one_of_irreducible_of_root this hx⟩
 
-lemma degree_eq_one_of_irreducible [is_alg_closed k] {p : polynomial k} (h_nz : p ≠ 0) (hp : irreducible p) :
+lemma degree_eq_one_of_irreducible [is_alg_closed k] {p : polynomial k} (h_nz : p ≠ 0)
+  (hp : irreducible p) :
   p.degree = 1 :=
 degree_eq_one_of_irreducible_of_splits h_nz hp (polynomial.splits' _)
 
@@ -111,7 +112,8 @@ open mv_polynomial
 def eval_X_self (f : monic_irreducible k) : mv_polynomial (monic_irreducible k) k :=
 polynomial.eval₂ mv_polynomial.C (X f) f
 
-/-- The span of `f(x_f)` across monic irreducible polynomials `f` where `x_f` is an indeterminate. -/
+/-- The span of `f(x_f)` across monic irreducible polynomials `f` where `x_f` is an
+indeterminate. -/
 def span_eval : ideal (mv_polynomial (monic_irreducible k) k) :=
 ideal.span $ set.range $ eval_X_self k
 
@@ -259,7 +261,8 @@ instance to_step_of_le.directed_system :
 
 end algebraic_closure
 
-/-- The canonical algebraic closure of a field, the direct limit of adding roots to the field for each polynomial over the field. -/
+/-- The canonical algebraic closure of a field, the direct limit of adding roots to the field for
+each polynomial over the field. -/
 def algebraic_closure : Type u :=
 ring.direct_limit (algebraic_closure.step k) (λ i j h, algebraic_closure.to_step_of_le k i j h)
 

src/linear_algebra/finite_dimensional.lean

@@ -184,7 +184,8 @@ noncomputable def findim (K V : Type*) [field K]
   [add_comm_group V] [vector_space K V] : ℕ :=
 if h : dim K V < omega.{v} then classical.some (lt_omega.1 h) else 0
 
-/-- In a finite-dimensional space, its dimension (seen as a cardinal) coincides with its `findim`. -/
+/-- In a finite-dimensional space, its dimension (seen as a cardinal) coincides with its
+`findim`. -/
 lemma findim_eq_dim (K : Type u) (V : Type v) [field K]
   [add_comm_group V] [vector_space K V] [finite_dimensional K V] :
   (findim K V : cardinal.{v}) = dim K V :=
@@ -334,7 +335,8 @@ begin
   rw linear_dependent_iff at this,
   obtain ⟨s, g, sum, z, zm, nonzero⟩ := this,
   -- Now we have to extend `g` to all of `t`, then to all of `V`.
-  let f : V → K := λ x, if h : x ∈ t then if (⟨x, h⟩ : (↑t : set V)) ∈ s then g ⟨x, h⟩ else 0 else 0,
+  let f : V → K :=
+    λ x, if h : x ∈ t then if (⟨x, h⟩ : (↑t : set V)) ∈ s then g ⟨x, h⟩ else 0 else 0,
   -- and finally clean up the mess caused by the extension.
   refine ⟨f, _, _⟩,
   { dsimp [f],
@@ -491,7 +493,8 @@ end
 by simp
 
 /-- The submodule generated by a finite set is finite-dimensional. -/
-theorem span_of_finite {A : set V} (hA : set.finite A) : finite_dimensional K (submodule.span K A) :=
+theorem span_of_finite {A : set V} (hA : set.finite A) :
+  finite_dimensional K (submodule.span K A) :=
 is_noetherian_span_of_finite K hA
 
 /-- The submodule generated by a single element is finite-dimensional. -/
@@ -542,7 +545,8 @@ end
   ((submodule.eq_bot_iff _).1 $ eq.symm $ bot_eq_top_of_dim_eq_zero h) ⟨x, hx⟩ submodule.mem_top,
 λ h, by rw [h, dim_bot]⟩
 
-@[simp] theorem findim_eq_zero {S : submodule K V} [finite_dimensional K S] : findim K S = 0 ↔ S = ⊥ :=
+@[simp] theorem findim_eq_zero {S : submodule K V} [finite_dimensional K S] :
+  findim K S = 0 ↔ S = ⊥ :=
 by rw [← dim_eq_zero, ← findim_eq_dim, ← @nat.cast_zero cardinal, cardinal.nat_cast_inj]
 
 end zero_dim
@@ -598,7 +602,8 @@ end
 lemma findim_le [finite_dimensional K V] (s : submodule K V) : findim K s ≤ findim K V :=
 by { rw ← s.findim_quotient_add_findim, exact nat.le_add_left _ _ }
 
-/-- The dimension of a strict submodule is strictly bounded by the dimension of the ambient space. -/
+/-- The dimension of a strict submodule is strictly bounded by the dimension of the ambient
+space. -/
 lemma findim_lt [finite_dimensional K V] {s : submodule K V} (h : s < ⊤) :
   findim K s < findim K V :=
 begin
@@ -665,7 +670,8 @@ theorem nonempty_linear_equiv_of_findim_eq [finite_dimensional K V] [finite_dime
 nonempty_linear_equiv_of_lift_dim_eq $ by simp only [← findim_eq_dim, cond, lift_nat_cast]
 
 /--
-Two finite-dimensional vector spaces are isomorphic if and only if they have the same (finite) dimension.
+Two finite-dimensional vector spaces are isomorphic if and only if they have the same (finite)
+dimension.
 -/
 theorem nonempty_linear_equiv_iff_findim_eq [finite_dimensional K V] [finite_dimensional K V₂] :
    nonempty (V ≃ₗ[K] V₂) ↔ findim K V = findim K V₂ :=

src/linear_algebra/lagrange.lean

@@ -96,7 +96,7 @@ end
 
 theorem degree_interpolate_lt : (interpolate s f).degree < s.card :=
 if H : s = ∅ then by { subst H, rw [interpolate_empty, degree_zero], exact with_bot.bot_lt_coe _ }
-else lt_of_le_of_lt (degree_sum_le _ _) $ (finset.sup_lt_iff $ with_bot.bot_lt_coe s.card).2 $ λ b _,
+else (degree_sum_le _ _).trans_lt $ (finset.sup_lt_iff $ with_bot.bot_lt_coe s.card).2 $ λ b _,
 calc  (C (f b) * basis s b).degree
     ≤ (C (f b)).degree + (basis s b).degree : degree_mul_le _ _
 ... ≤ 0 + (basis s b).degree : add_le_add_right degree_C_le _

src/linear_algebra/linear_independent.lean

@@ -647,7 +647,8 @@ begin
 end
 
 /-- Dedekind's linear independence of characters -/
--- See, for example, Keith Conrad's note <https://kconrad.math.uconn.edu/blurbs/galoistheory/linearchar.pdf>
+-- See, for example, Keith Conrad's note
+--  <https://kconrad.math.uconn.edu/blurbs/galoistheory/linearchar.pdf>
 theorem linear_independent_monoid_hom (G : Type*) [monoid G] (L : Type*) [comm_ring L]
   [no_zero_divisors L] :
   @linear_independent _ L (G → L) (λ f, f : (G →* L) → (G → L)) _ _ _ :=
@@ -664,7 +665,8 @@ exact linear_independent_iff'.2
 -- and it remains to prove that `g` vanishes on `insert a s`.
 
 -- We now make the key calculation:
--- For any character `i` in the original `finset`, we have `g i • i = g i • a` as functions on the monoid `G`.
+-- For any character `i` in the original `finset`, we have `g i • i = g i • a` as functions on the
+-- monoid `G`.
 have h1 : ∀ i ∈ s, (g i • i : G → L) = g i • a, from λ i his, funext $ λ x : G,
   -- We prove these expressions are equal by showing
   -- the differences of their values on each monoid element `x` is zero
@@ -707,11 +709,13 @@ have h4 : g a = 0, from calc
   ... = (g a • a : G → L) 1 : by rw ← a.map_one; refl
   ... = (∑ i in insert a s, (g i • i : G → L)) 1 : begin
       rw finset.sum_eq_single a,
-      { intros i his hia, rw finset.mem_insert at his, rw [h3 i (his.resolve_left hia), zero_smul] },
+      { intros i his hia, rw finset.mem_insert at his,
+        rw [h3 i (his.resolve_left hia), zero_smul] },
       { intros haas, exfalso, apply haas, exact finset.mem_insert_self a s }
     end
   ... = 0 : by rw hg; refl,
--- Now we're done; the last two facts together imply that `g` vanishes on every element of `insert a s`.
+-- Now we're done; the last two facts together imply that `g` vanishes on every element
+-- of `insert a s`.
 (finset.forall_mem_insert _ _ _).2 ⟨h4, h3⟩)
 
 lemma le_of_span_le_span [nontrivial R] {s t u: set M}
@@ -906,7 +910,8 @@ assume t, finset.induction_on t
         have s ⊆ (span K ↑(insert b₂ s' ∪ t) : submodule K V), from
           assume b₃ hb₃,
           have ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t) : set V),
-            by simp [insert_eq, -singleton_union, -union_singleton, union_subset_union, subset.refl, subset_union_right],
+            by simp [insert_eq, -singleton_union, -union_singleton, union_subset_union, subset.refl,
+              subset_union_right],
           have hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t) : set V)),
             from span_mono this (hss' hb₃),
           have s ⊆ (span K (insert b₁ ↑(s' ∪ t)) : submodule K V),