chore(*): split lines and move module doc `measure_theory/category/Me…

…as` (#6459)

src/deprecated/subgroup.lean

@@ -680,7 +680,8 @@ instance additive.simple_add_group [group G] [simple_group G] :
 theorem multiplicative.simple_group_iff [add_group A] :
   simple_group (multiplicative A) ↔ simple_add_group A :=
 ⟨λ hs, ⟨λ N h, @simple_group.simple _ _ hs _ (by exactI multiplicative.normal_subgroup_iff.2 h)⟩,
-  λ hs, ⟨λ N h, @simple_add_group.simple _ _ hs _ (by exactI multiplicative.normal_subgroup_iff.1 h)⟩⟩
+  λ hs, ⟨λ N h,
+          @simple_add_group.simple _ _ hs _ (by exactI multiplicative.normal_subgroup_iff.1 h)⟩⟩
 
 instance multiplicative.simple_group [add_group A] [simple_add_group A] :
 simple_group (multiplicative A) := multiplicative.simple_group_iff.2 (by apply_instance)

src/deprecated/subring.lean

@@ -12,7 +12,8 @@ open group
 
 variables {R : Type u} [ring R]
 
-/-- `S` is a subring: a set containing 1 and closed under multiplication, addition and and additive inverse. -/
+/-- `S` is a subring: a set containing 1 and closed under multiplication, addition and additive
+inverse. -/
 class is_subring (S : set R) extends is_add_subgroup S, is_submonoid S : Prop.
 
 /-- The ring structure on a subring coerced to a type. -/
@@ -130,7 +131,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/field_theory/chevalley_warning.lean

@@ -77,7 +77,8 @@ begin
   calc (∏ j : σ, (e a : σ → K) j ^ d j)
         = (e a : σ → K) i ^ d i * (∏ (j : {j // j ≠ i}), (e a : σ → K) j ^ d j) :
         by { rw [← e'.prod_comp, fintype.prod_sum_type, univ_unique, prod_singleton], refl }
-    ... = a ^ d i * (∏ (j : {j // j ≠ i}), (e a : σ → K) j ^ d j) : by rw equiv.subtype_equiv_codomain_symm_apply_eq
+    ... = a ^ d i * (∏ (j : {j // j ≠ i}), (e a : σ → K) j ^ d j) :
+        by rw equiv.subtype_equiv_codomain_symm_apply_eq
     ... = a ^ d i * (∏ j, x₀ j ^ d j) : congr_arg _ (fintype.prod_congr _ _ _) -- see below
     ... = (∏ j, x₀ j ^ d j) * a ^ d i : mul_comm _ _,
   { -- the remaining step of the calculation above
@@ -141,7 +142,8 @@ begin
   -- Now we prove the remaining step from the preceding calculation
   show (1 - f i ^ (q - 1)).total_degree ≤ (q - 1) * (f i).total_degree,
   calc (1 - f i ^ (q - 1)).total_degree
-        ≤ max (1 : mv_polynomial σ K).total_degree (f i ^ (q - 1)).total_degree : total_degree_sub _ _
+        ≤ max (1 : mv_polynomial σ K).total_degree (f i ^ (q - 1)).total_degree :
+        total_degree_sub _ _
     ... ≤ (f i ^ (q - 1)).total_degree : by simp only [max_eq_right, nat.zero_le, total_degree_one]
     ... ≤ (q - 1) * (f i).total_degree : total_degree_pow _ _
 end

src/field_theory/finite/basic.lean

@@ -18,7 +18,8 @@ Throughout most of this file, `K` denotes a finite field
 and `q` is notation for the cardinality of `K`.
 
 See `ring_theory.integral_domain` for the fact that the unit group of a finite field is a
-cyclic group, as well as the fact that every finite integral domain is a field (`field_of_integral_domain`).
+cyclic group, as well as the fact that every finite integral domain is a field
+(`field_of_integral_domain`).
 
 ## Main results
 
@@ -51,8 +52,8 @@ open polynomial
 
 /-- The cardinality of a field is at most `n` times the cardinality of the image of a degree `n`
   polynomial -/
-lemma card_image_polynomial_eval [decidable_eq R] [fintype R] {p : polynomial R} (hp : 0 < p.degree) :
-  fintype.card R ≤ nat_degree p * (univ.image (λ x, eval x p)).card :=
+lemma card_image_polynomial_eval [decidable_eq R] [fintype R] {p : polynomial R}
+  (hp : 0 < p.degree) : fintype.card R ≤ nat_degree p * (univ.image (λ x, eval x p)).card :=
 finset.card_le_mul_card_image _ _
   (λ a _, calc _ = (p - C a).roots.to_finset.card : congr_arg card
     (by simp [finset.ext_iff, mem_roots_sub_C hp])

src/field_theory/fixed.lean

@@ -24,8 +24,8 @@ then `findim (fixed_points G F) F = fintype.card G`.
 
 ## Main Definitions
 
-- `fixed_points G F`, the subfield consisting of elements of `F` fixed_points by every element of `G`, where
-`G` is a group that acts on `F`.
+- `fixed_points G F`, the subfield consisting of elements of `F` fixed_points by every element of
+`G`, where `G` is a group that acts on `F`.
 
 -/
 
@@ -74,7 +74,8 @@ lemma linear_independent_smul_of_linear_independent {s : finset F} :
   linear_independent (fixed_points G F) (λ i : (↑s : set F), (i : F)) →
   linear_independent F (λ i : (↑s : set F), mul_action.to_fun G F i) :=
 begin
-  refine finset.induction_on s (λ _, linear_independent_empty_type $ λ ⟨x⟩, x.2) (λ a s has ih hs, _),
+  refine finset.induction_on s (λ _, linear_independent_empty_type $ λ ⟨x⟩, x.2)
+    (λ a s has ih hs, _),
   rw coe_insert at hs ⊢,
   rw linear_independent_insert (mt mem_coe.1 has) at hs,
   rw linear_independent_insert' (mt mem_coe.1 has), refine ⟨ih hs.1, λ ha, _⟩,

src/field_theory/intermediate_field.lean

@@ -147,12 +147,14 @@ lemma multiset_sum_mem (m : multiset L) :
   (∀ a ∈ m, a ∈ S) → m.sum ∈ S :=
 S.to_subfield.multiset_sum_mem m
 
-/-- Product of elements of an intermediate field indexed by a `finset` is in the intermediate_field. -/
+/-- Product of elements of an intermediate field indexed by a `finset` is in the intermediate_field.
+-/
 lemma prod_mem {ι : Type*} {t : finset ι} {f : ι → L} (h : ∀ c ∈ t, f c ∈ S) :
   ∏ i in t, f i ∈ S :=
 S.to_subfield.prod_mem h
 
-/-- Sum of elements in a `intermediate_field` indexed by a `finset` is in the `intermediate_field`. -/
+/-- Sum of elements in a `intermediate_field` indexed by a `finset` is in the `intermediate_field`.
+-/
 lemma sum_mem {ι : Type*} {t : finset ι} {f : ι → L} (h : ∀ c ∈ t, f c ∈ S) :
   ∑ i in t, f i ∈ S :=
 S.to_subfield.sum_mem h

src/field_theory/primitive_element.lean

@@ -26,7 +26,8 @@ requires more unfolding without much obvious benefit.
 
 ## Tags
 
-primitive element, separable field extension, separable extension, intermediate field, adjoin, exists_adjoin_simple_eq_top
+primitive element, separable field extension, separable extension, intermediate field, adjoin,
+exists_adjoin_simple_eq_top
 
 -/
 

src/field_theory/splitting_field.lean

@@ -29,7 +29,7 @@ section splits
 
 variables (i : α →+* β)
 
-/-- a polynomial `splits` iff it is zero or all of its irreducible factors have `degree` 1 -/
+/-- A polynomial `splits` iff it is zero or all of its irreducible factors have `degree` 1. -/
 def splits (f : polynomial α) : Prop :=
 f = 0 ∨ ∀ {g : polynomial β}, irreducible g → g ∣ f.map i → degree g = 1
 
@@ -80,8 +80,10 @@ else or.inr $ λ p hp hpf, ((principal_ideal_ring.irreducible_iff_prime.1 hp).2.
 
 lemma splits_of_splits_mul {f g : polynomial α} (hfg : f * g ≠ 0) (h : splits i (f * g)) :
   splits i f ∧ splits i g :=
-⟨or.inr $ λ g hgi hg, or.resolve_left h hfg hgi (by rw map_mul; exact dvd.trans hg (dvd_mul_right _ _)),
- or.inr $ λ g hgi hg, or.resolve_left h hfg hgi (by rw map_mul; exact dvd.trans hg (dvd_mul_left _ _))⟩
+⟨or.inr $ λ g hgi hg, or.resolve_left h hfg hgi
+   (by rw map_mul; exact dvd.trans hg (dvd_mul_right _ _)),
+ or.inr $ λ g hgi hg, or.resolve_left h hfg hgi
+   (by rw map_mul; exact dvd.trans hg (dvd_mul_left _ _))⟩
 
 lemma splits_of_splits_of_dvd {f g : polynomial α} (hf0 : f ≠ 0) (hf : splits i f) (hgf : g ∣ f) :
   splits i g :=
@@ -381,12 +383,14 @@ begin
   { have hcoeff : p.leading_coeff ≠ 0,
     { intro h, exact hzero (leading_coeff_eq_zero.1 h) },
     have hrootsnorm : (normalize p).roots.card = (normalize p).nat_degree,
-    { rw [roots_normalize, normalize_apply, nat_degree_mul hzero (units.ne_zero _), hroots, coe_norm_unit,
-        nat_degree_C, add_zero], },
-    have hprod := prod_multiset_X_sub_C_of_monic_of_roots_card_eq (monic_normalize hzero) hrootsnorm,
+    { rw [roots_normalize, normalize_apply, nat_degree_mul hzero (units.ne_zero _), hroots,
+          coe_norm_unit, nat_degree_C, add_zero], },
+    have hprod := prod_multiset_X_sub_C_of_monic_of_roots_card_eq (monic_normalize hzero)
+                    hrootsnorm,
     rw [roots_normalize, normalize_apply, coe_norm_unit_of_ne_zero hzero] at hprod,
     calc (C p.leading_coeff) * (multiset.map (λ (a : α), X - C a) p.roots).prod
-        = p * C ((p.leading_coeff)⁻¹ * p.leading_coeff) : by rw [hprod, mul_comm, mul_assoc, ← C_mul]
+        = p * C ((p.leading_coeff)⁻¹ * p.leading_coeff) :
+        by rw [hprod, mul_comm, mul_assoc, ← C_mul]
     ... = p * C 1 : by field_simp
     ... = p : by simp only [mul_one, ring_hom.map_one], },
 end
@@ -495,7 +499,8 @@ end
 theorem factor_dvd_of_degree_ne_zero {f : polynomial α} (hf : f.degree ≠ 0) : factor f ∣ f :=
 factor_dvd_of_not_is_unit (mt degree_eq_zero_of_is_unit hf)
 
-theorem factor_dvd_of_nat_degree_ne_zero {f : polynomial α} (hf : f.nat_degree ≠ 0) : factor f ∣ f :=
+theorem factor_dvd_of_nat_degree_ne_zero {f : polynomial α} (hf : f.nat_degree ≠ 0) :
+  factor f ∣ f :=
 factor_dvd_of_degree_ne_zero (mt nat_degree_eq_of_degree_eq_some hf)
 
 /-- Divide a polynomial f by X - C r where r is a root of f in a bigger field extension. -/
@@ -510,7 +515,8 @@ mul_div_by_monic_eq_iff_is_root.2 $ by rw [is_root.def, eval_map, hg, eval₂_mu
 
 theorem nat_degree_remove_factor (f : polynomial α) :
   f.remove_factor.nat_degree = f.nat_degree - 1 :=
-by rw [remove_factor, nat_degree_div_by_monic _ (monic_X_sub_C _), nat_degree_map, nat_degree_X_sub_C]
+by rw [remove_factor, nat_degree_div_by_monic _ (monic_X_sub_C _), nat_degree_map,
+       nat_degree_X_sub_C]
 
 theorem nat_degree_remove_factor' {f : polynomial α} {n : ℕ} (hfn : f.nat_degree = n+1) :
   f.remove_factor.nat_degree = n :=
@@ -586,7 +592,8 @@ nat.rec_on n (λ α _ _ _ β _ j _, by exactI ⟨j, j.comp_id⟩) $ λ n ih α _
 have hndf : f.nat_degree ≠ 0, by { intro h, rw h at hf, cases hf },
 have hfn0 : f ≠ 0, by { intro h, rw h at hndf, exact hndf rfl },
 let ⟨r, hr⟩ := exists_root_of_splits _ (splits_of_splits_of_dvd j hfn0 hj
-  (factor_dvd_of_nat_degree_ne_zero hndf)) (mt is_unit_iff_degree_eq_zero.2 f.irreducible_factor.1) in
+  (factor_dvd_of_nat_degree_ne_zero hndf))
+  (mt is_unit_iff_degree_eq_zero.2 f.irreducible_factor.1) in
 have hmf0 : map (adjoin_root.of f.factor) f ≠ 0, from map_ne_zero hfn0,
 have hsf : splits (adjoin_root.lift j r hr) f.remove_factor,
 by { rw ← X_sub_C_mul_remove_factor _ hndf at hmf0, refine (splits_of_splits_mul _ hmf0 _).2,

src/field_theory/subfield.lean

@@ -446,8 +446,8 @@ lemma closure_eq_of_le {s : set K} {t : subfield K} (h₁ : s ⊆ t) (h₂ : t 
 le_antisymm (closure_le.2 h₁) h₂
 
 /-- An induction principle for closure membership. If `p` holds for `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 K} {p : K → Prop} {x} (h : x ∈ closure s)
   (Hs : ∀ x ∈ s, p x) (H1 : p 1)

src/measure_theory/category/Meas.lean

@@ -7,21 +7,22 @@ import topology.category.Top.basic
 import measure_theory.giry_monad
 import category_theory.monad.algebra
 
-/-
-* Meas, the category of measurable spaces
+/-!
+# The category of measurable spaces
+
+Measurable spaces and measurable functions form a (concrete) category `Meas`.
 
-Measurable spaces and measurable functions form a (concrete) category Meas.
+## Main definitions
 
-Measure : Meas ⥤ Meas is the functor which sends a measurable space X
-to the space of measures on X; it is a monad (the "Giry monad").
+* `Measure : Meas ⥤ Meas`: the functor which sends a measurable space `X`
+to the space of measures on `X`; it is a monad (the "Giry monad").
 
-Borel : Top ⥤ Meas sends a topological space X to X equipped with the
-σ-algebra of Borel sets (the σ-algebra generated by the open subsets of X).
+* `Borel : Top ⥤ Meas`: sends a topological space `X` to `X` equipped with the
+`σ`-algebra of Borel sets (the `σ`-algebra generated by the open subsets of `X`).
 
 ## Tags
 
 measurable space, giry monad, borel
-
 -/
 
 noncomputable theory

src/ring_theory/ideal/operations.lean

@@ -93,9 +93,11 @@ theorem smul_induction_on {p : M → Prop} {x} (H : x ∈ I • N)
 theorem mem_smul_span_singleton {I : ideal R} {m : M} {x : M} :
   x ∈ I • span R ({m} : set M) ↔ ∃ y ∈ I, y • m = x :=
 ⟨λ hx, smul_induction_on hx
-  (λ r hri n hnm, let ⟨s, hs⟩ := mem_span_singleton.1 hnm in ⟨r * s, I.mul_mem_right _ hri, hs ▸ mul_smul r s m⟩)
+  (λ r hri n hnm,
+    let ⟨s, hs⟩ := mem_span_singleton.1 hnm in ⟨r * s, I.mul_mem_right _ hri, hs ▸ mul_smul r s m⟩)
   ⟨0, I.zero_mem, by rw [zero_smul]⟩
-  (λ m1 m2 ⟨y1, hyi1, hy1⟩ ⟨y2, hyi2, hy2⟩, ⟨y1 + y2, I.add_mem hyi1 hyi2, by rw [add_smul, hy1, hy2]⟩)
+  (λ m1 m2 ⟨y1, hyi1, hy1⟩ ⟨y2, hyi2, hy2⟩,
+    ⟨y1 + y2, I.add_mem hyi1 hyi2, by rw [add_smul, hy1, hy2]⟩)
   (λ c r ⟨y, hyi, hy⟩, ⟨c * y, I.mul_mem_left _ hyi, by rw [mul_smul, hy]⟩),
 λ ⟨y, hyi, hy⟩, hy ▸ smul_mem_smul hyi (subset_span $ set.mem_singleton m)⟩
 

src/ring_theory/principal_ideal_domain.lean

@@ -122,7 +122,8 @@ instance euclidean_domain.to_principal_ideal_domain : is_principal_ideal_ring R
           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];
+    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