chore(*): split lines (#6323)

Author: Julian-Kuelshammer

src/algebraic_geometry/sheafed_space.lean

@@ -80,7 +80,8 @@ local attribute [simp] id comp
 
 lemma id_c (X : SheafedSpace C) :
   ((𝟙 X) : X ⟶ X).c =
-  (((functor.left_unitor _).inv) ≫ (whisker_right (nat_trans.op (opens.map_id (X.carrier)).hom) _)) := rfl
+  (((functor.left_unitor _).inv) ≫
+  (whisker_right (nat_trans.op (opens.map_id (X.carrier)).hom) _)) := rfl
 
 @[simp] lemma id_c_app (X : SheafedSpace C) (U) :
   ((𝟙 X) : X ⟶ X).c.app U = eq_to_hom (by { op_induction U, cases U, refl }) :=

src/group_theory/eckmann_hilton.lean

@@ -95,8 +95,8 @@ omit h₁ h₂ distrib
 then the group is commutative. -/
 @[to_additive "If a type carries an additive group structure that distributes
 over a unital binary operation, then the additive group is commutative."]
-def comm_group [G : group X] (distrib : ∀ a b c d, ((a * b) <m₁> (c * d)) = ((a <m₁> c) * (b <m₁> d))) :
-  comm_group X :=
+def comm_group [G : group X]
+  (distrib : ∀ a b c d, ((a * b) <m₁> (c * d)) = ((a <m₁> c) * (b <m₁> d))) : comm_group X :=
 { mul_comm := (eckmann_hilton.comm_monoid h₁ group.is_unital distrib).mul_comm,
   ..G }
 

src/group_theory/semidirect_product.lean

@@ -49,7 +49,8 @@ variables {N G} {φ : G →* mul_aut N}
 private def one_aux : N ⋊[φ] G := ⟨1, 1⟩
 private def mul_aux (a b : N ⋊[φ] G) : N ⋊[φ] G := ⟨a.1 * φ a.2 b.1, a.right * b.right⟩
 private def inv_aux (a : N ⋊[φ] G) : N ⋊[φ] G := let i := a.2⁻¹ in ⟨φ i a.1⁻¹, i⟩
-private lemma mul_assoc_aux (a b c : N ⋊[φ] G) : mul_aux (mul_aux a b) c = mul_aux a (mul_aux b c) :=
+private lemma mul_assoc_aux (a b c : N ⋊[φ] G) :
+  mul_aux (mul_aux a b) c = mul_aux a (mul_aux b c) :=
 by simp [mul_aux, mul_assoc, mul_equiv.map_mul]
 private lemma mul_one_aux (a : N ⋊[φ] G) : mul_aux a one_aux = a :=
 by cases a; simp [mul_aux, one_aux]

src/group_theory/subgroup.lean

@@ -397,7 +397,8 @@ begin
   congr',
 end
 
-@[to_additive] lemma nontrivial_iff_exists_ne_one (H : subgroup G) : nontrivial H ↔ ∃ x ∈ H, x ≠ (1:G) :=
+@[to_additive] lemma nontrivial_iff_exists_ne_one (H : subgroup G) :
+  nontrivial H ↔ ∃ x ∈ H, x ≠ (1:G) :=
 begin
   split,
   { introI h,
@@ -873,7 +874,8 @@ instance top_normal : normal (⊤ : subgroup G) := ⟨λ _ _, mem_top⟩
 
 variable (G)
 /-- The center of a group `G` is the set of elements that commute with everything in `G` -/
-@[to_additive "The center of a group `G` is the set of elements that commute with everything in `G`"]
+@[to_additive "The center of a group `G` is the set of elements that commute with everything in
+`G`"]
 def center : subgroup G :=
 { carrier := {z | ∀ g, g * z = z * g},
   one_mem' := by simp,
@@ -908,7 +910,8 @@ def normalizer : subgroup G :=
 -- variant for sets.
 -- TODO should this replace `normalizer`?
 /-- The `set_normalizer` of `S` is the subgroup of `G` whose elements satisfy `g*S*g⁻¹=S` -/
-@[to_additive "The `set_normalizer` of `S` is the subgroup of `G` whose elements satisfy `g+S-g=S`."]
+@[to_additive "The `set_normalizer` of `S` is the subgroup of `G` whose elements satisfy
+`g+S-g=S`."]
 def set_normalizer (S : set G) : subgroup G :=
 { carrier := {g : G | ∀ n, n ∈ S ↔ g * n * g⁻¹ ∈ S},
   one_mem' := by simp,

src/group_theory/submonoid/operations.lean

@@ -557,7 +557,8 @@ begin
     exact ⟨h x, by { rintros rfl, exact S.one_mem }⟩ },
 end
 
-@[to_additive] lemma nontrivial_iff_exists_ne_one (S : submonoid M) : nontrivial S ↔ ∃ x ∈ S, x ≠ (1:M) :=
+@[to_additive] lemma nontrivial_iff_exists_ne_one (S : submonoid M) :
+  nontrivial S ↔ ∃ x ∈ S, x ≠ (1:M) :=
 begin
   split,
   { introI h,

src/ring_theory/noetherian.lean

@@ -176,7 +176,8 @@ begin
   have : f x ∈ map f s, { rw mem_map, exact ⟨x, hx, rfl⟩ },
   rw [← ht1,← set.image_id ↑t1, finsupp.mem_span_iff_total] at this,
   rcases this with ⟨l, hl1, hl2⟩,
-  refine mem_sup.2 ⟨(finsupp.total M M R id).to_fun ((finsupp.lmap_domain R R g : (P →₀ R) → M →₀ R) l), _,
+  refine mem_sup.2 ⟨(finsupp.total M M R id).to_fun
+    ((finsupp.lmap_domain R R g : (P →₀ R) → M →₀ R) l), _,
     x - finsupp.total M M R id ((finsupp.lmap_domain R R g : (P →₀ R) → M →₀ R) l),
     _, add_sub_cancel'_right _ _⟩,
   { rw [← set.image_id (g '' ↑t1), finsupp.mem_span_iff_total], refine ⟨_, _, rfl⟩,
@@ -389,8 +390,9 @@ lemma well_founded_submodule_gt (R M) [ring R] [add_comm_group M] [module R M] :
   ∀ [is_noetherian R M], well_founded ((>) : submodule R M → submodule R M → Prop) :=
 is_noetherian_iff_well_founded.mp
 
-lemma finite_of_linear_independent {R M} [comm_ring R] [nontrivial R] [add_comm_group M] [module R M]
-  [is_noetherian R M] {s : set M} (hs : linear_independent R (coe : s → M)) : s.finite :=
+lemma finite_of_linear_independent {R M} [comm_ring R] [nontrivial R] [add_comm_group M]
+  [module R M] [is_noetherian R M] {s : set M} (hs : linear_independent R (coe : s → M)) :
+  s.finite :=
 begin
   refine classical.by_contradiction (λ hf, rel_embedding.well_founded_iff_no_descending_seq.1
     (well_founded_submodule_gt R M) ⟨_⟩),
@@ -409,9 +411,11 @@ begin
     by dsimp [gt]; simp only [lt_iff_le_not_le, (this _ _).symm]; tauto⟩
 end
 
-/-- A module is Noetherian iff every nonempty set of submodules has a maximal submodule among them. -/
+/-- A module is Noetherian iff every nonempty set of submodules has a maximal submodule among them.
+-/
 theorem set_has_maximal_iff_noetherian {R M} [ring R] [add_comm_group M] [module R M] :
-  (∀ a : set $ submodule R M, a.nonempty → ∃ M' ∈ a, ∀ I ∈ a, M' ≤ I → I = M') ↔ is_noetherian R M :=
+  (∀ a : set $ submodule R M, a.nonempty → ∃ M' ∈ a, ∀ I ∈ a, M' ≤ I → I = M') ↔
+  is_noetherian R M :=
 by rw [is_noetherian_iff_well_founded, well_founded.well_founded_iff_has_max']
 
 /-- If `∀ I > J, P I` implies `P J`, then `P` holds for all submodules. -/
@@ -578,11 +582,12 @@ end
 variables {A : Type*} [integral_domain A] [is_noetherian_ring A]
 
 /--In a noetherian integral domain which is not a field, every non-zero ideal contains a non-zero
-  product of prime ideals; in a field, the whole ring is a non-zero ideal containing only 0 as product
-  or prime ideals ([samuel, § 3.3, Lemma 3])
+  product of prime ideals; in a field, the whole ring is a non-zero ideal containing only 0 as
+  product or prime ideals ([samuel, § 3.3, Lemma 3])
 -/
 
-lemma exists_prime_spectrum_prod_le_and_ne_bot_of_domain (h_fA : ¬ is_field A) {I : ideal A} (h_nzI: I ≠ ⊥) :
+lemma exists_prime_spectrum_prod_le_and_ne_bot_of_domain (h_fA : ¬ is_field A) {I : ideal A}
+  (h_nzI: I ≠ ⊥) :
   ∃ (Z : multiset (prime_spectrum A)), multiset.prod (Z.map (coe : subtype _ → ideal A)) ≤ I ∧
     multiset.prod (Z.map (coe : subtype _ → ideal A)) ≠ ⊥ :=
 begin

src/ring_theory/principal_ideal_domain.lean

@@ -118,13 +118,12 @@ instance euclidean_domain.to_principal_ideal_domain : is_principal_ideal_ring R
         (ideal.mem_span_singleton.2 $ dvd_add (dvd_mul_right _ _) $
         have (x % (well_founded.min wf {x : R | x ∈ S ∧ x ≠ 0} h) ∉ {x : R | x ∈ S ∧ x ≠ 0}),
           from λ h₁, well_founded.not_lt_min wf _ h h₁ (mod_lt x hmin.2),
-        have x % well_founded.min wf {x : R | x ∈ S ∧ x ≠ 0} h = 0, by finish [(mod_mem_iff hmin.1).2 hx],
+        have x % well_founded.min wf {x : R | x ∈ S ∧ x ≠ 0} h = 0,
+          by finish [(mod_mem_iff hmin.1).2 hx],
         by simp *),
       λ hx, let ⟨y, hy⟩ := ideal.mem_span_singleton.1 hx in hy.symm ▸ S.mul_mem_right _ hmin.1⟩⟩
-    else ⟨0, submodule.ext $ λ a, by rw [← @submodule.bot_coe R R _ _ _, span_eq, submodule.mem_bot]; exact
-      ⟨λ haS, by_contradiction $ λ ha0, h ⟨a, ⟨haS, ha0⟩⟩,
-      λ h₁, h₁.symm ▸ S.zero_mem⟩⟩⟩ }
-
+    else ⟨0, submodule.ext $ λ a, by rw [← @submodule.bot_coe R R _ _ _, span_eq, submodule.mem_bot];
+      exact ⟨λ haS, by_contradiction $ λ ha0, h ⟨a, ⟨haS, ha0⟩⟩, λ h₁, h₁.symm ▸ S.zero_mem⟩⟩⟩ }
 end
 
 namespace principal_ideal_ring

src/ring_theory/roots_of_unity.lean

@@ -147,7 +147,8 @@ is_cyclic_of_subgroup_integral_domain ((units.coe_hom R).comp (roots_of_unity k
 
 lemma card_roots_of_unity : fintype.card (roots_of_unity k R) ≤ k :=
 calc  fintype.card (roots_of_unity k R)
-    = fintype.card {x // x ∈ nth_roots k (1 : R)} : fintype.card_congr (roots_of_unity_equiv_nth_roots R k)
+    = fintype.card {x // x ∈ nth_roots k (1 : R)} :
+          fintype.card_congr (roots_of_unity_equiv_nth_roots R k)
 ... ≤ (nth_roots k (1 : R)).attach.card           : multiset.card_le_of_le (multiset.erase_dup_le _)
 ... = (nth_roots k (1 : R)).card                  : multiset.card_attach
 ... ≤ k                                           : card_nth_roots k 1

src/ring_theory/subring.lean

@@ -407,14 +407,16 @@ instance : has_inf (subring R) :=
 @[simp] lemma mem_inf {p p' : subring R} {x : R} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p' := iff.rfl
 
 instance : has_Inf (subring R) :=
-⟨λ s, subring.mk' (⋂ t ∈ s, ↑t) (⨅ t ∈ s, subring.to_submonoid t ) (⨅ t ∈ s, subring.to_add_subgroup t) (by simp) (by simp)⟩
+⟨λ s, subring.mk' (⋂ t ∈ s, ↑t) (⨅ t ∈ s, subring.to_submonoid t )
+  (⨅ t ∈ s, subring.to_add_subgroup t) (by simp) (by simp)⟩
 
 @[simp, norm_cast] lemma coe_Inf (S : set (subring R)) :
   ((Inf S : subring R) : set R) = ⋂ s ∈ S, ↑s := rfl
 
 lemma mem_Inf {S : set (subring R)} {x : R} : x ∈ Inf S ↔ ∀ p ∈ S, x ∈ p := set.mem_bInter_iff
 
-@[simp] lemma Inf_to_submonoid (s : set (subring R)) : (Inf s).to_submonoid = ⨅ t ∈ s, subring.to_submonoid t := mk'_to_submonoid _ _
+@[simp] lemma Inf_to_submonoid (s : set (subring R)) :
+  (Inf s).to_submonoid = ⨅ t ∈ s, subring.to_submonoid t := mk'_to_submonoid _ _
 
 @[simp] lemma Inf_to_add_subgroup (s : set (subring R)) :
   (Inf s).to_add_subgroup = ⨅ t ∈ s, subring.to_add_subgroup t := mk'_to_add_subgroup _ _
@@ -458,8 +460,8 @@ lemma closure_eq_of_le {s : set R} {t : subring R} (h₁ : s ⊆ t) (h₂ : t 
 le_antisymm (closure_le.2 h₁) h₂
 
 /-- An induction principle for closure membership. If `p` holds for `0`, `1`, and all elements
-of `s`, and is preserved under addition, negation, and multiplication, then `p` holds for all elements
-of the closure of `s`. -/
+of `s`, and is preserved under addition, negation, and multiplication, then `p` holds for all
+elements of the closure of `s`. -/
 @[elab_as_eliminator]
 lemma closure_induction {s : set R} {p : R → Prop} {x} (h : x ∈ closure s)
   (Hs : ∀ x ∈ s, p x) (H0 : p 0) (H1 : p 1)
@@ -480,10 +482,12 @@ lemma mem_closure_iff {s : set R} {x} :
     ( λ p hp, add_subgroup.subset_closure ((submonoid.closure s).mul_mem hp hq) )
     ( begin rw zero_mul q, apply add_subgroup.zero_mem _, end )
     ( λ p₁ p₂ ihp₁ ihp₂, begin rw add_mul p₁ p₂ q, apply add_subgroup.add_mem _ ihp₁ ihp₂, end )
-    ( λ x hx, begin have f : -x * q = -(x*q) := by simp, rw f, apply add_subgroup.neg_mem _ hx, end ) )
+    ( λ x hx, begin have f : -x * q = -(x*q) :=
+      by simp, rw f, apply add_subgroup.neg_mem _ hx, end ) )
   ( begin rw mul_zero x, apply add_subgroup.zero_mem _, end )
   ( λ q₁ q₂ ihq₁ ihq₂, begin rw mul_add x q₁ q₂, apply add_subgroup.add_mem _ ihq₁ ihq₂ end )
-  ( λ z hz, begin have f : x * -z = -(x*z) := by simp, rw f, apply add_subgroup.neg_mem _ hz, end ) ),
+  ( λ z hz, begin have f : x * -z = -(x*z) := by simp,
+            rw f, apply add_subgroup.neg_mem _ hz, end ) ),
  λ h, add_subgroup.closure_induction h
  ( λ x hx, submonoid.closure_induction hx
   ( λ x hx, subset_closure hx )
@@ -767,7 +771,8 @@ begin
   { rw [list.map_cons, list.sum_cons],
     exact ha this (ih HL.2) },
   replace HL := HL.1, clear ih tl,
-  suffices : ∃ L : list R, (∀ x ∈ L, x ∈ s) ∧ (list.prod hd = list.prod L ∨ list.prod hd = -list.prod L),
+  suffices : ∃ L : list R, (∀ x ∈ L, x ∈ s) ∧
+    (list.prod hd = list.prod L ∨ list.prod hd = -list.prod L),
   { rcases this with ⟨L, HL', HP | HP⟩,
     { rw HP, clear HP HL hd, induction L with hd tl ih, { exact h1 },
       rw list.forall_mem_cons at HL',

src/ring_theory/tensor_product.lean

@@ -485,7 +485,8 @@ lemma assoc_aux_2 (r : R) :
 -- variables {R A B C}
 
 -- @[simp] theorem assoc_tmul (a : A) (b : B) (c : C) :
---   ((tensor_product.assoc R A B C) : (A ⊗[R] B) ⊗[R] C → A ⊗[R] (B ⊗[R] C)) ((a ⊗ₜ b) ⊗ₜ c) = a ⊗ₜ (b ⊗ₜ c) :=
+--   ((tensor_product.assoc R A B C) :
+--   (A ⊗[R] B) ⊗[R] C → A ⊗[R] (B ⊗[R] C)) ((a ⊗ₜ b) ⊗ₜ c) = a ⊗ₜ (b ⊗ₜ c) :=
 -- rfl
 
 end