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

archive/100-theorems-list/82_cubing_a_cube.lean

@@ -12,7 +12,8 @@ Proof that a cube (in dimension n ≥ 3) cannot be cubed:
 There does not exist a partition of a cube into finitely many smaller cubes (at least two)
 of different sizes.
 
-We follow the proof described here: http://www.alaricstephen.com/main-featured/2017/9/28/cubing-a-cube-proof
+We follow the proof described here:
+http://www.alaricstephen.com/main-featured/2017/9/28/cubing-a-cube-proof
 -/
 
 
@@ -262,7 +263,8 @@ lemma two_le_mk_bcubes : 2 ≤ cardinal.mk (bcubes cs c) :=
 begin
   rw [two_le_iff],
   rcases v.1 c.b_mem_bottom with ⟨_, ⟨i, rfl⟩, hi⟩,
-  have h2i : i ∈ bcubes cs c := ⟨hi.1.symm, v.2.1 i hi.1.symm ⟨tail c.b, hi.2, λ j, c.b_mem_side j.succ⟩⟩,
+  have h2i : i ∈ bcubes cs c :=
+    ⟨hi.1.symm, v.2.1 i hi.1.symm ⟨tail c.b, hi.2, λ j, c.b_mem_side j.succ⟩⟩,
   let j : fin (n+1) := ⟨2, h.2.2.2.2⟩,
   have hj : 0 ≠ j := by { simp only [fin.ext_iff, ne.def], contradiction },
   let p : fin (n+1) → ℝ := λ j', if j' = j then c.b j + (cs i).w else c.b j',
@@ -291,7 +293,8 @@ end
 /-- There is a smallest cube in the valley -/
 lemma exists_mi : ∃(i : ι), i ∈ bcubes cs c ∧ ∀(i' ∈ bcubes cs c),
   (cs i).w ≤ (cs i').w :=
-by simpa using (bcubes cs c).exists_min_image (λ i, (cs i).w) (finite.of_fintype _) (nonempty_bcubes h v)
+by simpa
+  using (bcubes cs c).exists_min_image (λ i, (cs i).w) (finite.of_fintype _) (nonempty_bcubes h v)
 
 /-- We let `mi` be the (index for the) smallest cube in the valley `c` -/
 def mi : ι := classical.some $ exists_mi h v

docs/tutorial/category_theory/intro.lean

@@ -65,7 +65,8 @@ variables (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z)
 This says "let `C` be a category, let `W`, `X`, `Y`, `Z` be objects of `C`, and let `f : W ⟶ X`, `g
 : X ⟶ Y` and `h : Y ⟶ Z` be morphisms in `C` (with the specified source and targets)".
 
-Note that we need to explicitly tell Lean the universe that the morphisms live in, by writing `category.{v} C`, because Lean cannot guess this from `C` alone.
+Note that we need to explicitly tell Lean the universe that the morphisms live in, by writing
+`category.{v} C`, because Lean cannot guess this from `C` alone.
 
 The order in which universes are introduced at the top of the file matters: we put the universes for
 morphisms first (typically `v`, `v₁` and so on), and then universes for objects (typically `u`, `u₁`

src/algebra/algebra/subalgebra.lean

@@ -409,7 +409,8 @@ theorem surjective_algebra_map_iff :
 ⟨λ h, eq_bot_iff.2 $ λ y _, let ⟨x, hx⟩ := h y in hx ▸ subalgebra.algebra_map_mem _ _,
 λ h y, algebra.mem_bot.1 $ eq_bot_iff.1 h (algebra.mem_top : y ∈ _)⟩
 
-theorem bijective_algebra_map_iff {R A : Type*} [field R] [semiring A] [nontrivial A] [algebra R A] :
+theorem bijective_algebra_map_iff {R A : Type*} [field R] [semiring A] [nontrivial A]
+  [algebra R A] :
   function.bijective (algebra_map R A) ↔ (⊤ : subalgebra R A) = ⊥ :=
 ⟨λ h, surjective_algebra_map_iff.1 h.2,
 λ h, ⟨(algebra_map R A).injective, surjective_algebra_map_iff.2 h⟩⟩

src/algebra/continued_fractions/computation/approximations.lean

@@ -18,12 +18,13 @@ for the values involved in the continued fractions computation `gcf.of`.
 ## Main Theorems
 
 - `gcf.of_part_num_eq_one`: shows that all partial numerators `aᵢ` are equal to one.
-- `gcf.exists_int_eq_of_part_denom`: shows that all partial denominators `bᵢ` correspond to an integer.
+- `gcf.exists_int_eq_of_part_denom`: shows that all partial denominators `bᵢ` correspond to an
+  integer.
 - `gcf.one_le_of_nth_part_denom`: shows that `1 ≤ bᵢ`.
-- `gcf.succ_nth_fib_le_of_nth_denom`: shows that the `n`th denominator `Bₙ` is greater than or equal to
-  the `n + 1`th fibonacci number `nat.fib (n + 1)`.
-- `gcf.le_of_succ_nth_denom`: shows that `Bₙ₊₁ ≥ bₙ * Bₙ`, where `bₙ` is the `n`th partial denominator
-  of the continued fraction.
+- `gcf.succ_nth_fib_le_of_nth_denom`: shows that the `n`th denominator `Bₙ` is greater than or equal
+  to the `n + 1`th fibonacci number `nat.fib (n + 1)`.
+- `gcf.le_of_succ_nth_denom`: shows that `Bₙ₊₁ ≥ bₙ * Bₙ`, where `bₙ` is the `n`th partial
+  denominator of the continued fraction.
 
 ## References
 

src/algebra/continued_fractions/computation/correctness_terminating.lean

@@ -45,7 +45,8 @@ variables {K : Type*} [linear_ordered_field K] {v : K} {n : ℕ}
 /--
 Given two continuants `pconts` and `conts` and a value `fr`, this function returns
 - `conts.a / conts.b` if `fr = 0`
-- `exact_conts.a / exact_conts.b` where `exact_conts = next_continuants 1 fr⁻¹ pconts conts` otherwise.
+- `exact_conts.a / exact_conts.b` where `exact_conts = next_continuants 1 fr⁻¹ pconts conts`
+  otherwise.
 
 This function can be used to compute the exact value approxmated by a continued fraction `gcf.of v`
 as described in lemma `comp_exact_value_correctness_of_stream_eq_some`.
@@ -79,9 +80,9 @@ fraction. Here is an example to illustrate the idea:
 Let `(v : ℚ) := 3.4`. We have
 - `gcf.int_fract_pair.stream v 0 = some ⟨3, 0.4⟩`, and
 - `gcf.int_fract_pair.stream v 1 = some ⟨2, 0.5⟩`.
-Now `(gcf.of v).convergents' 1 = 3 + 1/2`, and our fractional term at position `2` is `0.5`. We hence
-have `v = 3 + 1/(2 + 0.5) = 3 + 1/2.5 = 3.4`. This computation corresponds exactly to the one using
-the recurrence equation in `comp_exact_value`.
+Now `(gcf.of v).convergents' 1 = 3 + 1/2`, and our fractional term at position `2` is `0.5`. We
+hence have `v = 3 + 1/(2 + 0.5) = 3 + 1/2.5 = 3.4`. This computation corresponds exactly to the one
+using the recurrence equation in `comp_exact_value`.
 -/
 lemma comp_exact_value_correctness_of_stream_eq_some :
   ∀ {ifp_n : int_fract_pair K}, int_fract_pair.stream v n = some ifp_n →
@@ -145,8 +146,9 @@ begin
       have : ifp_n' = ifp_n, by injection (eq.trans (nth_stream_eq').symm nth_stream_eq),
       cases this,
       -- get the correspondence between ifp_n and g.s.nth n
-      have s_nth_eq : g.s.nth n = some ⟨1, (⌊ifp_n.fr⁻¹⌋ : K)⟩, from
-        gcf.nth_of_eq_some_of_nth_int_fract_pair_stream_fr_ne_zero nth_stream_eq ifp_n_fract_ne_zero,
+      have s_nth_eq : g.s.nth n = some ⟨1, (⌊ifp_n.fr⁻¹⌋ : K)⟩,
+        from gcf.nth_of_eq_some_of_nth_int_fract_pair_stream_fr_ne_zero nth_stream_eq
+          ifp_n_fract_ne_zero,
       -- the claim now follows by unfolding the definitions and tedious calculations
       -- some shorthand notation
       let ppA := ppconts.a, let ppB := ppconts.b,
@@ -207,7 +209,8 @@ have int_fract_pair.stream v (n + 1) = none, from
   gcf.of_terminated_at_n_iff_succ_nth_int_fract_pair_stream_eq_none.elim_left terminated_at_n,
  of_correctness_of_nth_stream_eq_none this
 
-/-- If `gcf.of v` terminates, then there is `n : ℕ` such that the `n`th convergent is exactly `v`. -/
+/-- If `gcf.of v` terminates, then there is `n : ℕ` such that the `n`th convergent is exactly
+`v`. -/
 lemma of_correctness_of_terminates (terminates : (gcf.of v).terminates) :
   ∃ (n : ℕ), v = (gcf.of v).convergents n :=
 exists.elim terminates

src/algebra/continued_fractions/computation/translations.lean

@@ -14,14 +14,15 @@ This is a collection of simple lemmas between the different structures used for
 of continued fractions defined in `algebra.continued_fractions.computation.basic`. The file consists
 of three sections:
 1. Recurrences and inversion lemmas for `int_fract_pair.stream`: these lemmas give us inversion
-   rules and recurrences for the computation of the stream of integer and fractional parts of a value.
+   rules and recurrences for the computation of the stream of integer and fractional parts of
+   a value.
 2. Translation lemmas for the head term: these lemmas show us that the head term of the computed
    continued fraction of a value `v` is `⌊v⌋` and how this head term is moved along the structures
    used in the computation process.
 3. Translation lemmas for the sequence: these lemmas show how the sequences of the involved
-   structures (`int_fract_pair.stream`, `int_fract_pair.seq1`, and `generalized_continued_fraction.of`)
-   are connected, i.e. how the values are moved along the structures and the termination of one
-   sequence implies the termination of another sequence.
+   structures (`int_fract_pair.stream`, `int_fract_pair.seq1`, and
+   `generalized_continued_fraction.of`) are connected, i.e. how the values are moved along the
+   structures and the termination of one sequence implies the termination of another sequence.
 
 ## Main Theorems
 
@@ -31,7 +32,8 @@ of three sections:
   of integer and fractional parts of a value in case of termination.
 - `nth_of_eq_some_of_succ_nth_int_fract_pair_stream` and
   `nth_of_eq_some_of_nth_int_fract_pair_stream_fr_ne_zero` show how the entries of the sequence
-  of the computed continued fraction can be obtained from the stream of integer and fractional parts.
+  of the computed continued fraction can be obtained from the stream of integer and fractional
+  parts.
 -/
 
 namespace generalized_continued_fraction
@@ -89,7 +91,8 @@ begin
     have : int_fract_pair.stream v (n + 1) ≠ none, by simp [stream_succ_nth_eq],
     have : ¬int_fract_pair.stream v n = none
            ∧ ¬(∃ ifp, int_fract_pair.stream v n = some ifp ∧ ifp.fr = 0), by
-    { have not_none_not_fract_zero, from (not_iff_not_of_iff succ_nth_stream_eq_none_iff).elim_left this,
+    { have not_none_not_fract_zero,
+        from (not_iff_not_of_iff succ_nth_stream_eq_none_iff).elim_left this,
       exact (not_or_distrib.elim_left not_none_not_fract_zero) },
     cases this with stream_nth_ne_none nth_fr_ne_zero,
     replace nth_fr_ne_zero : ∀ ifp, int_fract_pair.stream v n = some ifp → ifp.fr ≠ 0, by
@@ -99,7 +102,8 @@ begin
     existsi ifp_n,
     have ifp_n_fr_ne_zero : ifp_n.fr ≠ 0, from nth_fr_ne_zero ifp_n stream_nth_eq,
     cases ifp_n with _ ifp_n_fr,
-    suffices : int_fract_pair.of ifp_n_fr⁻¹ = ifp_succ_n, by simpa [stream_nth_eq, ifp_n_fr_ne_zero],
+    suffices : int_fract_pair.of ifp_n_fr⁻¹ = ifp_succ_n,
+      by simpa [stream_nth_eq, ifp_n_fr_ne_zero],
     simp only [int_fract_pair.stream, stream_nth_eq, ifp_n_fr_ne_zero, option.some_bind, if_false]
       at stream_succ_nth_eq,
     injection stream_succ_nth_eq },
@@ -109,7 +113,7 @@ end
 lemma exists_succ_nth_stream_of_fr_zero {ifp_succ_n : int_fract_pair K}
   (stream_succ_nth_eq : int_fract_pair.stream v (n + 1) = some ifp_succ_n)
   (succ_nth_fr_eq_zero : ifp_succ_n.fr = 0) :
-  ∃ (ifp_n : int_fract_pair K), int_fract_pair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ⌊ifp_n.fr⁻¹⌋ :=
+  ∃ ifp_n : int_fract_pair K, int_fract_pair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ⌊ifp_n.fr⁻¹⌋ :=
 begin
   -- get the witness from `succ_nth_stream_eq_some_iff` and prove that it has the additional
   -- properties
@@ -159,8 +163,8 @@ section sequence
 
 Here we state some lemmas that show how the sequences of the involved structures
 (`int_fract_pair.stream`, `int_fract_pair.seq1`, and `generalized_continued_fraction.of`) are
-connected, i.e. how the values are moved along the structures and how the termination of one sequence
-implies the termination of another sequence.
+connected, i.e. how the values are moved along the structures and how the termination of one
+sequence implies the termination of another sequence.
 -/
 
 variable {n : ℕ}

src/algebra/divisibility.lean

@@ -227,7 +227,8 @@ section comm_monoid_with_zero
 
 variable [comm_monoid_with_zero α]
 
-/-- `dvd_not_unit a b` expresses that `a` divides `b` "strictly", i.e. that `b` divided by `a` is not a unit. -/
+/-- `dvd_not_unit a b` expresses that `a` divides `b` "strictly", i.e. that `b` divided by `a`
+is not a unit. -/
 def dvd_not_unit (a b : α) : Prop := a ≠ 0 ∧ ∃ x, ¬is_unit x ∧ b = a * x
 
 lemma dvd_not_unit_of_dvd_of_not_dvd {a b : α} (hd : a ∣ b) (hnd : ¬ b ∣ a) :

src/algebra/group/prod.lean

@@ -252,13 +252,16 @@ end monoid_hom
 namespace mul_equiv
 variables {M N} [monoid M] [monoid N]
 
-/-- The equivalence between `M × N` and `N × M` given by swapping the components is multiplicative. -/
-@[to_additive prod_comm "The equivalence between `M × N` and `N × M` given by swapping the components is
-additive."]
+/-- The equivalence between `M × N` and `N × M` given by swapping the components
+is multiplicative. -/
+@[to_additive prod_comm "The equivalence between `M × N` and `N × M` given by swapping the
+components is additive."]
 def prod_comm : M × N ≃* N × M :=
 { map_mul' := λ ⟨x₁, y₁⟩ ⟨x₂, y₂⟩, rfl, ..equiv.prod_comm M N }
 
-@[simp, to_additive coe_prod_comm] lemma coe_prod_comm : ⇑(prod_comm : M × N ≃* N × M) = prod.swap := rfl
+@[simp, to_additive coe_prod_comm] lemma coe_prod_comm :
+  ⇑(prod_comm : M × N ≃* N × M) = prod.swap := rfl
+
 @[simp, to_additive coe_prod_comm_symm] lemma coe_prod_comm_symm :
   ⇑((prod_comm : M × N ≃* N × M).symm) = prod.swap := rfl
 

src/algebra/quandle.lean

@@ -62,12 +62,14 @@ Use `open_locale quandles` to use these.
 
 ## Todo
 
-* If g is the Lie algebra of a Lie group G, then (x ◃ y) = Ad (exp x) x forms a quandle
-* If X is a symmetric space, then each point has a corresponding involution that acts on X, forming a quandle.
-* Alexander quandle with `a ◃ b = t * b + (1 - t) * b`, with `a` and `b` elements of a module over Z[t,t⁻¹].
-* If G is a group, H a subgroup, and z in H, then there is a quandle `(G/H;z)` defined by
-  `yH ◃ xH = yzy⁻¹xH`.  Every homogeneous quandle (i.e., a quandle Q whose automorphism group acts
-  transitively on Q as a set) is isomorphic to such a quandle.
+* If `g` is the Lie algebra of a Lie group `G`, then `(x ◃ y) = Ad (exp x) x` forms a quandle.
+* If `X` is a symmetric space, then each point has a corresponding involution that acts on `X`,
+  forming a quandle.
+* Alexander quandle with `a ◃ b = t * b + (1 - t) * b`, with `a` and `b` elements
+  of a module over `Z[t,t⁻¹]`.
+* If `G` is a group, `H` a subgroup, and `z` in `H`, then there is a quandle `(G/H;z)` defined by
+  `yH ◃ xH = yzy⁻¹xH`.  Every homogeneous quandle (i.e., a quandle `Q` whose automorphism group acts
+  transitively on `Q` as a set) is isomorphic to such a quandle.
   There is a generalization to this arbitrary quandles in [Joyce's paper (Theorem 7.2)][Joyce1982].
 
 ## Tags
@@ -459,7 +461,8 @@ Relations for the enveloping group. This is a type-valued relation because
 is well-defined.  The relation `pre_envel_group_rel` is the `Prop`-valued version,
 which is used to define `envel_group` itself.
 -/
-inductive pre_envel_group_rel' (R : Type u) [rack R] : pre_envel_group R → pre_envel_group R → Type u
+inductive pre_envel_group_rel' (R : Type u) [rack R] :
+  pre_envel_group R → pre_envel_group R → Type u
 | refl {a : pre_envel_group R} : pre_envel_group_rel' a a
 | symm {a b : pre_envel_group R} (hab : pre_envel_group_rel' a b) : pre_envel_group_rel' b a
 | trans {a b c : pre_envel_group R}

src/algebra/ring_quot.lean

@@ -43,7 +43,8 @@ inductive rel (r : R → R → Prop) : R → R → Prop
 theorem rel.add_right {r : R → R → Prop} ⦃a b c : R⦄ (h : rel r b c) : rel r (a + b) (a + c) :=
 by { rw [add_comm a b, add_comm a c], exact rel.add_left h }
 
-theorem rel.neg {R : Type u₁} [ring R] {r : R → R → Prop} ⦃a b : R⦄ (h : rel r a b) : rel r (-a) (-b) :=
+theorem rel.neg {R : Type u₁} [ring R] {r : R → R → Prop} ⦃a b : R⦄ (h : rel r a b) :
+  rel r (-a) (-b) :=
 by simp only [neg_eq_neg_one_mul a, neg_eq_neg_one_mul b, rel.mul_right h]
 
 theorem rel.smul {r : A → A → Prop} (k : S) ⦃a b : A⦄ (h : rel r a b) : rel r (k • a) (k • b) :=
@@ -290,7 +291,8 @@ def lift_alg_hom {s : A → A → Prop} :
   right_inv := λ F, by { ext, simp, refl } }
 
 @[simp]
-lemma lift_alg_hom_mk_alg_hom_apply (f : A →ₐ[S] B) {s : A → A → Prop} (w : ∀ ⦃x y⦄, s x y → f x = f y) (x) :
+lemma lift_alg_hom_mk_alg_hom_apply (f : A →ₐ[S] B) {s : A → A → Prop}
+  (w : ∀ ⦃x y⦄, s x y → f x = f y) (x) :
   (lift_alg_hom S ⟨f, w⟩) ((mk_alg_hom S s) x) = f x :=
 rfl
 

src/analysis/normed_space/finite_dimension.lean

@@ -174,7 +174,8 @@ affine_map.continuous_linear_iff.1 f.linear.continuous_of_finite_dimensional
 def linear_map.to_continuous_linear_map [finite_dimensional 𝕜 E] (f : E →ₗ[𝕜] F') : E →L[𝕜] F' :=
 { cont := f.continuous_of_finite_dimensional, ..f }
 
-/-- The continuous linear equivalence induced by a linear equivalence on a finite dimensional space. -/
+/-- The continuous linear equivalence induced by a linear equivalence on a finite dimensional
+space. -/
 def linear_equiv.to_continuous_linear_equiv [finite_dimensional 𝕜 E] (e : E ≃ₗ[𝕜] F) : E ≃L[𝕜] F :=
 { continuous_to_fun := e.to_linear_map.continuous_of_finite_dimensional,
   continuous_inv_fun := begin
@@ -287,7 +288,8 @@ begin
   obtain ⟨u : ℕ → F, hu : dense_range u⟩ := exists_dense_seq F,
   obtain ⟨v : fin d → E, hv : is_basis 𝕜 v⟩ := finite_dimensional.fin_basis 𝕜 E,
   obtain ⟨C : ℝ, C_pos : 0 < C,
-          hC : ∀ {φ : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ i, ∥φ (v i)∥ ≤ M) → ∥φ∥ ≤ C * M⟩ := hv.op_norm_le,
+          hC : ∀ {φ : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ i, ∥φ (v i)∥ ≤ M) → ∥φ∥ ≤ C * M⟩ :=
+    hv.op_norm_le,
   have h_2C : 0 < 2*C := mul_pos zero_lt_two C_pos,
   have hε2C : 0 < ε/(2*C) := div_pos ε_pos h_2C,
   have : ∀ φ : E →L[𝕜] F, ∃ n : fin d → ℕ, ∥φ - (hv.constrL $ u ∘ n)∥ ≤ ε/2,

src/category_theory/hom_functor.lean

@@ -18,7 +18,8 @@ namespace category_theory.functor
 
 variables (C : Type u) [category.{v} C]
 
-/-- `functor.hom` is the hom-pairing, sending (X,Y) to X → Y, contravariant in X and covariant in Y. -/
+/-- `functor.hom` is the hom-pairing, sending `(X, Y)` to `X ⟶ Y`, contravariant in `X` and
+covariant in `Y`. -/
 definition hom : Cᵒᵖ × C ⥤ Type v :=
 { obj       := λ p, unop p.1 ⟶ p.2,
   map       := λ X Y f, λ h, f.1.unop ≫ h ≫ f.2 }

src/category_theory/isomorphism.lean

@@ -109,7 +109,8 @@ infixr ` ≪≫ `:80 := iso.trans -- type as `\ll \gg`.
   iso.trans
     {hom := hom, inv := inv, hom_inv_id' := hom_inv_id, inv_hom_id' := inv_hom_id}
     {hom := hom', inv := inv', hom_inv_id' := hom_inv_id', inv_hom_id' := inv_hom_id'} =
-  {hom := hom ≫ hom', inv := inv' ≫ inv, hom_inv_id' := hom_inv_id'', inv_hom_id' := inv_hom_id''} :=
+  { hom := hom ≫ hom', inv := inv' ≫ inv, hom_inv_id' := hom_inv_id'',
+    inv_hom_id' := inv_hom_id''} :=
 rfl
 
 @[simp] lemma trans_symm (α : X ≅ Y) (β : Y ≅ Z) : (α ≪≫ β).symm = β.symm ≪≫ α.symm := rfl
@@ -233,7 +234,8 @@ instance epi_of_iso (f : X ⟶ Y) [is_iso f] : epi f  :=
 @[priority 100] -- see Note [lower instance priority]
 instance mono_of_iso (f : X ⟶ Y) [is_iso f] : mono f :=
 { right_cancellation := λ Z g h w,
-  by rw [←category.comp_id g, ←category.comp_id h, ←is_iso.hom_inv_id f, ←category.assoc, w, ←category.assoc] }
+  by rw [← category.comp_id g, ← category.comp_id h, ← is_iso.hom_inv_id f, ← category.assoc, w,
+    ← category.assoc] }
 
 end is_iso