[Merged by Bors] - chore(*): reflow some long lines

archive/sensitivity.lean

@@ -28,8 +28,8 @@ by Leonardo de Moura at Microsoft Research, and his collaborators
 and using Lean's user maintained mathematics library
 (https://github.com/leanprover-community/mathlib).
 
-The project was developed at https://github.com/leanprover-community/lean-sensitivity
-and is now archived at https://github.com/leanprover-community/mathlib/blob/master/archive/sensitivity.lean
+The project was developed at https://github.com/leanprover-community/lean-sensitivity and is now
+archived at https://github.com/leanprover-community/mathlib/blob/master/archive/sensitivity.lean
 -/
 
 /-! The next two lines assert we do not want to give a constructive proof,
@@ -177,7 +177,8 @@ noncomputable def e : Π {n}, Q n → V n
 /-- The dual basis to `e`, defined inductively. -/
 noncomputable def ε : Π {n : ℕ} (p : Q n), V n →ₗ[ℝ] ℝ
 | 0 _ := linear_map.id
-| (n+1) p := cond (p 0) ((ε $ π p).comp $ linear_map.fst _ _ _) ((ε $ π p).comp $ linear_map.snd _ _ _)
+| (n+1) p := cond (p 0) ((ε $ π p).comp $ linear_map.fst _ _ _)
+               ((ε $ π p).comp $ linear_map.snd _ _ _)
 
 variable {n : ℕ}
 
@@ -211,7 +212,8 @@ begin
       let q : Q (n+1) := λ i, if h : i = 0 then ff else p (i.pred h)],
     all_goals {
       specialize h q,
-      rw [ε, show q 0 = tt, from rfl, cond_tt] at h <|> rw [ε, show q 0 = ff, from rfl, cond_ff] at h,
+      rw [ε, show q 0 = tt, from rfl, cond_tt] at h <|>
+        rw [ε, show q 0 = ff, from rfl, cond_ff] at h,
       rwa show p = π q, by { ext, simp [q, fin.succ_ne_zero, π] } } }
 end
 

src/algebra/algebra/basic.lean

@@ -121,7 +121,8 @@ it suffices to check the `algebra_map`s agree.
 -- We'll later use this to show `algebra ℤ M` is a subsingleton.
 @[ext]
 lemma algebra_ext {R : Type*} [comm_semiring R] {A : Type*} [semiring A] (P Q : algebra R A)
-  (w : ∀ (r : R), by { haveI := P, exact algebra_map R A r } = by { haveI := Q, exact algebra_map R A r }) :
+  (w : ∀ (r : R), by { haveI := P, exact algebra_map R A r } =
+    by { haveI := Q, exact algebra_map R A r }) :
   P = Q :=
 begin
   unfreezingI { rcases P with ⟨⟨P⟩⟩, rcases Q with ⟨⟨Q⟩⟩ },
@@ -699,7 +700,8 @@ by { ext, simp }
 by { ext, simp }
 
 /-- If an algebra morphism has an inverse, it is a algebra isomorphism. -/
-def of_alg_hom (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = alg_hom.id R A₂) (h₂ : g.comp f = alg_hom.id R A₁) : A₁ ≃ₐ[R] A₂ :=
+def of_alg_hom (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = alg_hom.id R A₂)
+  (h₂ : g.comp f = alg_hom.id R A₁) : A₁ ≃ₐ[R] A₂ :=
 { inv_fun   := g,
   left_inv  := alg_hom.ext_iff.1 h₂,
   right_inv := alg_hom.ext_iff.1 h₁,
@@ -799,8 +801,8 @@ include R S A
   Other than that, `algebra.comap` is now deprecated and replaced with `is_scalar_tower`. -/
 /- This is done to avoid a type class search with meta-variables `algebra R ?m_1` and
     `algebra ?m_1 A -/
-/- The `nolint` attribute is added because it has unused arguments `R` and `S`, but these are necessary for synthesizing the
-     appropriate type classes -/
+/- The `nolint` attribute is added because it has unused arguments `R` and `S`, but these are
+  necessary for synthesizing the appropriate type classes -/
 @[nolint unused_arguments]
 def comap : Type w := A
 

src/algebra/algebra/operations.lean

@@ -17,7 +17,8 @@ Let `R` be a commutative ring (or semiring) and aet `A` be an `R`-algebra.
 * `1 : submodule R A`       : the R-submodule R of the R-algebra A
 * `has_mul (submodule R A)` : multiplication of two sub-R-modules M and N of A is defined to be
                               the smallest submodule containing all the products `m * n`.
-* `has_div (submodule R A)` : `I / J` is defined to be the submodule consisting of all `a : A` such that `a • J ⊆ I`
+* `has_div (submodule R A)` : `I / J` is defined to be the submodule consisting of all `a : A` such
+                              that `a • J ⊆ I`
 
 It is proved that `submodule R A` is a semiring, and also an algebra over `set A`.
 
@@ -189,7 +190,8 @@ begin
     apply mul_subset_mul }
 end
 
-/-- `span` is a semiring homomorphism (recall multiplication is pointwise multiplication of subsets on either side). -/
+/-- `span` is a semiring homomorphism (recall multiplication is pointwise multiplication of subsets
+on either side). -/
 def span.ring_hom : set_semiring A →+* submodule R A :=
 { to_fun := submodule.span R,
   map_zero' := span_empty,

src/algebra/archimedean.lean

@@ -18,8 +18,8 @@ class archimedean (α) [ordered_add_comm_monoid α] : Prop :=
 namespace decidable_linear_ordered_add_comm_group
 variables [decidable_linear_ordered_add_comm_group α] [archimedean α]
 
-/-- An archimedean decidable linearly ordered `add_comm_group` has a version of the floor: for `a > 0`,
-any `g` in the group lies between some two consecutive multiples of `a`. -/
+/-- An archimedean decidable linearly ordered `add_comm_group` has a version of the floor: for
+`a > 0`, any `g` in the group lies between some two consecutive multiples of `a`. -/
 lemma exists_int_smul_near_of_pos {a : α} (ha : 0 < a) (g : α) :
   ∃ k, k •ℤ a ≤ g ∧ g < (k + 1) •ℤ a :=
 begin
@@ -167,8 +167,8 @@ instance : archimedean ℕ :=
 
 instance : archimedean ℤ :=
 ⟨λ n m m0, ⟨n.to_nat, le_trans (int.le_to_nat _) $
-by simpa only [nsmul_eq_mul, int.nat_cast_eq_coe_nat, zero_add, mul_one] using mul_le_mul_of_nonneg_left
-    (int.add_one_le_iff.2 m0) (int.coe_zero_le n.to_nat)⟩⟩
+by simpa only [nsmul_eq_mul, int.nat_cast_eq_coe_nat, zero_add, mul_one]
+  using mul_le_mul_of_nonneg_left (int.add_one_le_iff.2 m0) (int.coe_zero_le n.to_nat)⟩⟩
 
 /-- A linear ordered archimedean ring is a floor ring. This is not an `instance` because in some
 cases we have a computable `floor` function. -/

src/algebra/associated.lean

@@ -164,7 +164,8 @@ begin
   exact H _ o.1 _ o.2 h.symm
 end
 
-lemma irreducible_of_prime [comm_cancel_monoid_with_zero α] {p : α} (hp : prime p) : irreducible p :=
+lemma irreducible_of_prime [comm_cancel_monoid_with_zero α] {p : α} (hp : prime p) :
+  irreducible p :=
 ⟨hp.not_unit, λ a b hab,
   (show a * b ∣ a ∨ a * b ∣ b, from hab ▸ hp.div_or_div (hab ▸ (dvd_refl _))).elim
     (λ ⟨x, hx⟩, or.inr (is_unit_iff_dvd_one.2
@@ -298,7 +299,8 @@ lemma eq_zero_iff_of_associated [comm_monoid_with_zero α] {a b : α} (h : a ~
 lemma ne_zero_iff_of_associated [comm_monoid_with_zero α] {a b : α} (h : a ~ᵤ b) : a ≠ 0 ↔ b ≠ 0 :=
 by haveI := classical.dec; exact not_iff_not.2 (eq_zero_iff_of_associated h)
 
-lemma prime_of_associated [comm_monoid_with_zero α] {p q : α} (h : p ~ᵤ q) (hp : prime p) : prime q :=
+lemma prime_of_associated [comm_monoid_with_zero α] {p q : α} (h : p ~ᵤ q) (hp : prime p) :
+  prime q :=
 ⟨(ne_zero_iff_of_associated h).1 hp.ne_zero,
   let ⟨u, hu⟩ := h in
     ⟨λ ⟨v, hv⟩, hp.not_unit ⟨v * u⁻¹, by simp [hv, hu.symm]⟩,

src/algebra/big_operators/basic.lean

@@ -122,7 +122,8 @@ lemma ring_hom.map_multiset_sum [semiring β] [semiring γ] (f : β →+* γ) (s
   f s.sum = (s.map f).sum :=
 f.to_add_monoid_hom.map_multiset_sum s
 
-lemma ring_hom.map_prod [comm_semiring β] [comm_semiring γ] (g : β →+* γ) (f : α → β) (s : finset α) :
+lemma ring_hom.map_prod [comm_semiring β] [comm_semiring γ] (g : β →+* γ) (f : α → β)
+  (s : finset α) :
   g (∏ x in s, f x) = ∏ x in s, g (f x) :=
 g.to_monoid_hom.map_prod f s
 

src/algebra/big_operators/intervals.lean

@@ -20,7 +20,8 @@ open_locale big_operators nat
 
 namespace finset
 
-variables {α : Type u} {β : Type v} {γ : Type w} {s₂ s₁ s : finset α} {a : α} {g f : α → β} [comm_monoid β]
+variables {α : Type u} {β : Type v} {γ : Type w} {s₂ s₁ s : finset α} {a : α} {g f : α → β}
+  [comm_monoid β]
 
 lemma sum_Ico_add {δ : Type*} [add_comm_monoid δ] (f : ℕ → δ) (m n k : ℕ) :
   (∑ l in Ico m n, f (k + l)) = (∑ l in Ico (m + k) (n + k), f l) :=

src/algebra/big_operators/ring.lean

@@ -153,7 +153,8 @@ end comm_semiring
 /-- A product over all subsets of `s ∪ {x}` is obtained by multiplying the product over all subsets
 of `s`, and over all subsets of `s` to which one adds `x`. -/
 @[to_additive]
-lemma prod_powerset_insert [decidable_eq α] [comm_monoid β] {s : finset α} {x : α} (h : x ∉ s) (f : finset α → β) :
+lemma prod_powerset_insert [decidable_eq α] [comm_monoid β] {s : finset α} {x : α} (h : x ∉ s)
+  (f : finset α → β) :
   (∏ a in (insert x s).powerset, f a) =
     (∏ a in s.powerset, f a) * (∏ t in s.powerset, f (insert x t)) :=
 begin

src/algebra/category/Algebra/basic.lean

@@ -48,7 +48,8 @@ instance has_forget_to_Module : has_forget₂ (Algebra R) (Module R) :=
   { obj := λ M, Module.of R M,
     map := λ M₁ M₂ f, alg_hom.to_linear_map f, } }
 
-/-- The object in the category of R-algebras associated to a type equipped with the appropriate typeclasses. -/
+/-- The object in the category of R-algebras associated to a type equipped with the appropriate
+typeclasses. -/
 def of (X : Type v) [ring X] [algebra R X] : Algebra R := ⟨X⟩
 
 instance : inhabited (Algebra R) := ⟨of R R⟩
@@ -58,7 +59,8 @@ lemma coe_of (X : Type u) [ring X] [algebra R X] : (of R X : Type u) = X := rfl
 
 variables {R}
 
-/-- Forgetting to the underlying type and then building the bundled object returns the original algebra. -/
+/-- Forgetting to the underlying type and then building the bundled object returns the original
+algebra. -/
 @[simps]
 def of_self_iso (M : Algebra R) : Algebra.of R M ≅ M :=
 { hom := 𝟙 M, inv := 𝟙 M }
@@ -122,7 +124,8 @@ def to_alg_equiv {X Y : Algebra R} (i : X ≅ Y) : X ≃ₐ[R] Y :=
 
 end category_theory.iso
 
-/-- algebra equivalences between `algebras`s are the same as (isomorphic to) isomorphisms in `Algebra` -/
+/-- Algebra equivalences between `algebras`s are the same as (isomorphic to) isomorphisms in
+`Algebra`. -/
 @[simps]
 def alg_equiv_iso_Algebra_iso {X Y : Type u}
   [ring X] [ring Y] [algebra R X] [algebra R Y] :

src/algebra/category/CommRing/adjunctions.lean

@@ -30,7 +30,8 @@ def free : Type u ⥤ CommRing :=
 { obj := λ α, of (mv_polynomial α ℤ),
   map := λ X Y f, ((rename f : mv_polynomial X ℤ →ₐ[ℤ] mv_polynomial Y ℤ) :
                               (mv_polynomial X ℤ →+*   mv_polynomial Y ℤ)),
-  -- TODO these next two fields can be done by `tidy`, but the calls in `dsimp` and `simp` it generates are too slow.
+  -- TODO these next two fields can be done by `tidy`, but the calls in `dsimp` and `simp` it
+  -- generates are too slow.
   map_id' := λ X, ring_hom.ext $ rename_id,
   map_comp' := λ X Y Z f g, ring_hom.ext $ λ p, (rename_rename f g p).symm }
 

src/algebra/char_p.lean

@@ -355,8 +355,8 @@ lemma char_p_of_ne_zero (hn : fintype.card R = n) (hR : ∀ i < n, (i : R) = 0 
     { rintro ⟨k, rfl⟩, rw [nat.cast_mul, H, zero_mul] }
   end }
 
-lemma char_p_of_prime_pow_injective (p : ℕ) [hp : fact p.prime] (n : ℕ) (hn : fintype.card R = p ^ n)
-  (hR : ∀ i ≤ n, (p ^ i : R) = 0 → i = n) :
+lemma char_p_of_prime_pow_injective (p : ℕ) [hp : fact p.prime] (n : ℕ)
+  (hn : fintype.card R = p ^ n) (hR : ∀ i ≤ n, (p ^ i : R) = 0 → i = n) :
   char_p R (p ^ n) :=
 begin
   obtain ⟨c, hc⟩ := char_p.exists R, resetI,

src/algebra/continued_fractions/computation/basic.lean

@@ -14,10 +14,10 @@ import algebra.archimedean
 We formalise the standard computation of (regular) continued fractions for linear ordered floor
 fields. The algorithm is rather simple. Here is an outline of the procedure adapted from Wikipedia:
 
-Take a value `v`. We call `⌊v⌋` the *integer part* of `v` and `v − ⌊v⌋` the *fractional part* of `v`.
-A continued fraction representation of `v` can then be given by `[⌊v⌋; b₀, b₁, b₂,...]`,
-where `[b₀; b₁, b₂,...]` recursively is the continued fraction representation of `1 / (v − ⌊v⌋)`.
-This process stops when the fractional part hits 0.
+Take a value `v`. We call `⌊v⌋` the *integer part* of `v` and `v − ⌊v⌋` the *fractional part* of
+`v`.  A continued fraction representation of `v` can then be given by `[⌊v⌋; b₀, b₁, b₂,...]`, where
+`[b₀; b₁, b₂,...]` recursively is the continued fraction representation of `1 / (v − ⌊v⌋)`.  This
+process stops when the fractional part hits 0.
 
 In other words: to calculate a continued fraction representation of a number `v`, write down the
 integer part (i.e. the floor) of `v`. Subtract this integer part from `v`. If the difference is 0,
@@ -113,7 +113,8 @@ Creates the stream of integer and fractional parts of a value `v` needed to obta
 fraction representation of `v` in `generalized_continued_fraction.of`. More precisely, given a value
 `v : K`, it recursively computes a stream of option `ℤ × K` pairs as follows:
 - `stream v 0 = some ⟨⌊v⌋, v - ⌊v⌋⟩`
-- `stream v (n + 1) = some ⟨⌊frₙ⁻¹⌋, frₙ⁻¹ - ⌊frₙ⁻¹⌋⟩`, if `stream v n = some ⟨_, frₙ⟩` and `frₙ ≠ 0`
+- `stream v (n + 1) = some ⟨⌊frₙ⁻¹⌋, frₙ⁻¹ - ⌊frₙ⁻¹⌋⟩`,
+    if `stream v n = some ⟨_, frₙ⟩` and `frₙ ≠ 0`
 - `stream v (n + 1) = none`, otherwise
 
 For example, let `(v : ℚ) := 3.4`. The process goes as follows:
@@ -139,14 +140,14 @@ Uses `int_fract_pair.stream` to create a sequence with head (i.e. `seq1`) of int
 parts of a value `v`. The first value of `int_fract_pair.stream` is never `none`, so we can safely
 extract it and put the tail of the stream in the sequence part.
 
-This is just an intermediate representation and users should not (need to) directly interact with it.
-The setup of rewriting/simplification lemmas that make the definitions easy to use is done in
+This is just an intermediate representation and users should not (need to) directly interact with
+it. The setup of rewriting/simplification lemmas that make the definitions easy to use is done in
 `algebra.continued_fractions.computation.translations`.
 -/
 protected def seq1 (v : K) : seq1 $ int_fract_pair K :=
 ⟨ int_fract_pair.of v,--the head
-  seq.tail -- take the tail of `int_fract_pair.stream` since the first element is already in the head
-  -- create a sequence from `int_fract_pair.stream`
+  seq.tail -- take the tail of `int_fract_pair.stream` since the first element is already in the
+  -- head create a sequence from `int_fract_pair.stream`
   ⟨ int_fract_pair.stream v, -- the underlying stream
     @stream_is_seq _ _ _ v ⟩ ⟩ -- the proof that the stream is a sequence