lint(*): split long lines (#6833)

src/analysis/convex/caratheodory.lean

@@ -72,8 +72,7 @@ begin
       { apply div_nonneg (fpos i₀ (mem_of_subset (filter_subset _ t) mem)) (le_of_lt hg) },
       { simpa only [mem_filter, het, true_and, not_lt] using hes }, } },
   { simp only [subtype.coe_mk, center_mass_eq_of_sum_1 _ id ksum, id],
-    calc ∑ e in t.erase i₀, k e • e = ∑ e in t, k e • e :
-      by conv_rhs { rw [← insert_erase hi₀, sum_insert (not_mem_erase i₀ t), hk, zero_smul, zero_add], }
+    calc ∑ e in t.erase i₀, k e • e = ∑ e in t, k e • e : sum_erase _ (by rw [hk, zero_smul])
     ... = ∑ e in t, (f e - f i₀ / g i₀ * g e) • e : rfl
     ... = t.center_mass f id : _,
     simp only [sub_smul, mul_smul, sum_sub_distrib, ← smul_sum, gcombo, smul_zero,

src/analysis/specific_limits.lean

@@ -211,7 +211,8 @@ begin
   suffices : is_O _ (λ n : ℕ, (r' ^ k) ^ n) at_top,
     from this.trans_is_o (is_o_pow_pow_of_lt_left (pow_nonneg h0 _) hr'),
   conv in ((r' ^ _) ^ _) { rw [← pow_mul, mul_comm, pow_mul] },
-  suffices : ∀ n : ℕ, ∥(n : R)∥ ≤ (r' - 1)⁻¹ * ∥(1 : R)∥ * ∥r' ^ n∥, from (is_O_of_le' _ this).pow _,
+  suffices : ∀ n : ℕ, ∥(n : R)∥ ≤ (r' - 1)⁻¹ * ∥(1 : R)∥ * ∥r' ^ n∥,
+    from (is_O_of_le' _ this).pow _,
   intro n, rw mul_right_comm,
   refine n.norm_cast_le.trans (mul_le_mul_of_nonneg_right _ (norm_nonneg _)),
   simpa [div_eq_inv_mul, real.norm_eq_abs, abs_of_nonneg h0] using n.cast_le_pow_div_sub h1

src/data/padics/hensel.lean

@@ -163,12 +163,14 @@ have hdzne' : (↑(F.derivative.eval z) : ℚ_[p]) ≠ 0, from
   λ h, hdzne $ subtype.ext_iff_val.2 h,
 let ⟨q, hq⟩ := F.binom_expansion z (-z1) in
 have ∥(↑(F.derivative.eval z) * (↑(F.eval z) / ↑(F.derivative.eval z)) : ℚ_[p])∥ ≤ 1,
-  by {rw padic_norm_e.mul, apply mul_le_one, apply padic_int.norm_le_one, apply norm_nonneg, apply h1},
+  by { rw padic_norm_e.mul, exact mul_le_one (padic_int.norm_le_one _) (norm_nonneg _) h1 },
 have F.derivative.eval z * (-z1) = -F.eval z, from calc
   F.derivative.eval z * (-z1)
     = (F.derivative.eval z) * -⟨↑(F.eval z) / ↑(F.derivative.eval z), h1⟩ : by rw [hzeq]
-... = -((F.derivative.eval z) * ⟨↑(F.eval z) / ↑(F.derivative.eval z), h1⟩) : by simp [subtype.ext_iff_val]
-... = -(⟨↑(F.derivative.eval z) * (↑(F.eval z) / ↑(F.derivative.eval z)), this⟩) : subtype.ext_iff_val.2 $ by simp
+... = -((F.derivative.eval z) * ⟨↑(F.eval z) / ↑(F.derivative.eval z), h1⟩) :
+  by simp [subtype.ext_iff_val]
+... = -(⟨↑(F.derivative.eval z) * (↑(F.eval z) / ↑(F.derivative.eval z)), this⟩) :
+  subtype.ext $ by simp
 ... = -(F.eval z) : by simp [mul_div_cancel' _ hdzne'],
 have heq : F.eval z' = q * z1^2, by simpa [sub_eq_add_neg, this, hz'] using hq,
 ⟨q, heq⟩
@@ -178,7 +180,8 @@ private def calc_eval_z'_norm {z z' z1 : ℤ_[p]} {n} (hz : ih n z) {q}
   (hzeq : z1 = ⟨_, h1⟩) : ∥F.eval z'∥ ≤ ∥F.derivative.eval a∥^2 * T^(2^(n+1)) :=
 calc ∥F.eval z'∥
     = ∥q∥ * ∥z1∥^2 : by simp [heq]
-... ≤ 1 * ∥z1∥^2 : mul_le_mul_of_nonneg_right (padic_int.norm_le_one _) (pow_nonneg (norm_nonneg _) _)
+... ≤ 1 * ∥z1∥^2 :
+  mul_le_mul_of_nonneg_right (padic_int.norm_le_one _) (pow_nonneg (norm_nonneg _) _)
 ... = ∥F.eval z∥^2 / ∥F.derivative.eval a∥^2 :
   by simp [hzeq, hz.1, div_pow]
 ... ≤ (∥F.derivative.eval a∥^2 * T^(2^n))^2 / ∥F.derivative.eval a∥^2 :
@@ -227,7 +230,8 @@ private lemma newton_seq_norm_le (n : ℕ) :
 (newton_seq_aux n).2.2
 
 private lemma newton_seq_norm_eq (n : ℕ) :
-  ∥newton_seq (n+1) - newton_seq n∥ = ∥F.eval (newton_seq n)∥ / ∥F.derivative.eval (newton_seq n)∥ :=
+  ∥newton_seq (n+1) - newton_seq n∥ =
+    ∥F.eval (newton_seq n)∥ / ∥F.derivative.eval (newton_seq n)∥ :=
 by simp [newton_seq, newton_seq_aux, ih_n, sub_eq_add_neg, add_comm]
 
 private lemma newton_seq_succ_dist (n : ℕ) :
@@ -253,11 +257,11 @@ have 2 ≤ 2^(n+1),
     by simpa using this,
 calc ∥newton_seq (n+2) - newton_seq (n+1)∥
     ≤ ∥F.derivative.eval a∥ * T^(2^(n+1)) : newton_seq_succ_dist _
-... ≤ ∥F.derivative.eval a∥ * T^2 : mul_le_mul_of_nonneg_left
-                                      (pow_le_pow_of_le_one (norm_nonneg _) (le_of_lt T_lt_one) this)
-                                      (norm_nonneg _)
-... < ∥F.derivative.eval a∥ * T^1 : mul_lt_mul_of_pos_left (pow_lt_pow_of_lt_one T_pos T_lt_one (by norm_num))
-                                                           deriv_norm_pos
+... ≤ ∥F.derivative.eval a∥ * T^2 :
+  mul_le_mul_of_nonneg_left (pow_le_pow_of_le_one (norm_nonneg _) (le_of_lt T_lt_one) this)
+    (norm_nonneg _)
+... < ∥F.derivative.eval a∥ * T^1 :
+  mul_lt_mul_of_pos_left (pow_lt_pow_of_lt_one T_pos T_lt_one (by norm_num)) deriv_norm_pos
 ... = ∥F.eval a∥ / ∥F.derivative.eval a∥ :
   begin
     rw [T, pow_two, pow_one, normed_field.norm_div, ←mul_div_assoc, padic_norm_e.mul],
@@ -274,30 +278,36 @@ private lemma newton_seq_dist_aux (n : ℕ) :
   calc
   ∥newton_seq (n + (k + 1)) - newton_seq n∥
     = ∥newton_seq ((n + k) + 1) - newton_seq n∥ : by rw add_assoc
-... = ∥(newton_seq ((n + k) + 1) - newton_seq (n+k)) + (newton_seq (n+k) - newton_seq n)∥ : by rw ←sub_add_sub_cancel
-... ≤ max (∥newton_seq ((n + k) + 1) - newton_seq (n+k)∥) (∥newton_seq (n+k) - newton_seq n∥) : padic_int.nonarchimedean _ _
+... = ∥(newton_seq ((n + k) + 1) - newton_seq (n+k)) + (newton_seq (n+k) - newton_seq n)∥ :
+  by rw ←sub_add_sub_cancel
+... ≤ max (∥newton_seq ((n + k) + 1) - newton_seq (n+k)∥) (∥newton_seq (n+k) - newton_seq n∥) :
+  padic_int.nonarchimedean _ _
 ... ≤ max (∥F.derivative.eval a∥ * T^(2^((n + k)))) (∥F.derivative.eval a∥ * T^(2^n)) :
   max_le_max (newton_seq_succ_dist _) (newton_seq_dist_aux _)
 ... = ∥F.derivative.eval a∥ * T^(2^n) :
-  max_eq_right $ mul_le_mul_of_nonneg_left (pow_le_pow_of_le_one (norm_nonneg _) (le_of_lt T_lt_one) this) (norm_nonneg _)
+  max_eq_right $ mul_le_mul_of_nonneg_left
+    (pow_le_pow_of_le_one (norm_nonneg _) (le_of_lt T_lt_one) this) (norm_nonneg _)
 
 private lemma newton_seq_dist {n k : ℕ} (hnk : n ≤ k) :
   ∥newton_seq k - newton_seq n∥ ≤ ∥F.derivative.eval a∥ * T^(2^n) :=
 have hex : ∃ m, k = n + m, from exists_eq_add_of_le hnk,
 let ⟨_, hex'⟩ := hex in
 by rw hex'; apply newton_seq_dist_aux; assumption
 
-private lemma newton_seq_dist_to_a : ∀ n : ℕ, 0 < n → ∥newton_seq n - a∥ = ∥F.eval a∥ / ∥F.derivative.eval a∥
-| 1 h := by simp [sub_eq_add_neg, add_assoc, newton_seq, newton_seq_aux, ih_n]; apply normed_field.norm_div
+private lemma newton_seq_dist_to_a :
+  ∀ n : ℕ, 0 < n → ∥newton_seq n - a∥ = ∥F.eval a∥ / ∥F.derivative.eval a∥
+| 1 h := by simp [sub_eq_add_neg, add_assoc, newton_seq, newton_seq_aux, ih_n]
 | (k+2) h :=
   have hlt : ∥newton_seq (k+2) - newton_seq (k+1)∥ < ∥newton_seq (k+1) - a∥,
     by rw newton_seq_dist_to_a (k+1) (succ_pos _); apply newton_seq_succ_dist_weak; assumption,
   have hne' : ∥newton_seq (k + 2) - newton_seq (k+1)∥ ≠ ∥newton_seq (k+1) - a∥, from ne_of_lt hlt,
   calc  ∥newton_seq (k + 2) - a∥
     = ∥(newton_seq (k + 2) - newton_seq (k+1)) + (newton_seq (k+1) - a)∥ : by rw ←sub_add_sub_cancel
-... = max (∥newton_seq (k + 2) - newton_seq (k+1)∥) (∥newton_seq (k+1) - a∥) : padic_int.norm_add_eq_max_of_ne hne'
+... = max (∥newton_seq (k + 2) - newton_seq (k+1)∥) (∥newton_seq (k+1) - a∥) :
+  padic_int.norm_add_eq_max_of_ne hne'
 ... = ∥newton_seq (k+1) - a∥ : max_eq_right_of_lt hlt
-... = ∥polynomial.eval a F∥ / ∥polynomial.eval a (polynomial.derivative F)∥ : newton_seq_dist_to_a (k+1) (succ_pos _)
+... = ∥polynomial.eval a F∥ / ∥polynomial.eval a (polynomial.derivative F)∥ :
+  newton_seq_dist_to_a (k+1) (succ_pos _)
 
 private lemma bound' : tendsto (λ n : ℕ, ∥F.derivative.eval a∥ * T^(2^n)) at_top (𝓝 0) :=
 begin
@@ -351,7 +361,8 @@ setoid.symm (cau_seq.equiv_lim newton_cau_seq) _ hε
 private lemma soln_deriv_norm : ∥F.derivative.eval soln∥ = ∥F.derivative.eval a∥ :=
 norm_deriv_eq newton_seq_deriv_norm
 
-private lemma newton_seq_norm_tendsto_zero : tendsto (λ i, ∥F.eval (newton_cau_seq i)∥) at_top (𝓝 0) :=
+private lemma newton_seq_norm_tendsto_zero :
+  tendsto (λ i, ∥F.eval (newton_cau_seq i)∥) at_top (𝓝 0) :=
 squeeze_zero (λ _, norm_nonneg _) newton_seq_norm_le bound'_sq
 
 private lemma newton_seq_dist_tendsto :
@@ -375,24 +386,28 @@ end
 private lemma eval_soln : F.eval soln = 0 :=
 limit_zero_of_norm_tendsto_zero newton_seq_norm_tendsto_zero
 
-private lemma soln_unique (z : ℤ_[p]) (hev : F.eval z = 0) (hnlt : ∥z - a∥ < ∥F.derivative.eval a∥) :
+private lemma soln_unique (z : ℤ_[p]) (hev : F.eval z = 0)
+  (hnlt : ∥z - a∥ < ∥F.derivative.eval a∥) :
   z = soln :=
 have soln_dist : ∥z - soln∥ < ∥F.derivative.eval a∥, from calc
   ∥z - soln∥ = ∥(z - a) + (a - soln)∥ : by rw sub_add_sub_cancel
         ... ≤ max (∥z - a∥) (∥a - soln∥) : padic_int.nonarchimedean _ _
-        ... < ∥F.derivative.eval a∥ : max_lt hnlt (by rw norm_sub_rev; apply soln_dist_to_a_lt_deriv),
+        ... < ∥F.derivative.eval a∥ : max_lt hnlt (norm_sub_rev soln a ▸ soln_dist_to_a_lt_deriv),
 let h := z - soln,
     ⟨q, hq⟩ := F.binom_expansion soln h in
 have (F.derivative.eval soln + q * h) * h = 0, from eq.symm (calc
   0 = F.eval (soln + h) : by simp [hev, h]
 ... = F.derivative.eval soln * h + q * h^2 : by rw [hq, eval_soln, zero_add]
 ... = (F.derivative.eval soln + q * h) * h : by rw [pow_two, right_distrib, mul_assoc]),
 have h = 0, from by_contradiction $ λ hne,
-  have F.derivative.eval soln + q * h = 0, from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right hne,
+  have F.derivative.eval soln + q * h = 0,
+    from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right hne,
   have F.derivative.eval soln = (-q) * h, by simpa using eq_neg_of_add_eq_zero this,
   lt_irrefl ∥F.derivative.eval soln∥ (calc
   ∥F.derivative.eval soln∥ = ∥(-q) * h∥ : by rw this
-... ≤ 1 * ∥h∥ : by rw [padic_int.norm_mul]; exact mul_le_mul_of_nonneg_right (padic_int.norm_le_one _) (norm_nonneg _)
+... ≤ 1 * ∥h∥ :
+  by { rw padic_int.norm_mul,
+       exact mul_le_mul_of_nonneg_right (padic_int.norm_le_one _) (norm_nonneg _) }
 ... = ∥z - soln∥ : by simp [h]
 ... < ∥F.derivative.eval soln∥ : by rw soln_deriv_norm; apply soln_dist),
 eq_of_sub_eq_zero (by rw ←this; refl)
@@ -410,7 +425,8 @@ have (F.derivative.eval a + q * h) * h = 0, from eq.symm (calc
 ... = F.derivative.eval a * h + q * h^2 : by rw [hq, ha, zero_add]
 ... = (F.derivative.eval a + q * h) * h : by rw [pow_two, right_distrib, mul_assoc]),
 have h = 0, from by_contradiction $ λ hne,
-  have F.derivative.eval a + q * h = 0, from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right hne,
+  have F.derivative.eval a + q * h = 0,
+    from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right hne,
   have F.derivative.eval a = (-q) * h, by simpa using eq_neg_of_add_eq_zero this,
   lt_irrefl ∥F.derivative.eval a∥ (calc
     ∥F.derivative.eval a∥ = ∥q∥*∥h∥ : by simp [this]
@@ -430,5 +446,5 @@ lemma hensels_lemma : ∃ z : ℤ_[p], F.eval z = 0 ∧ ∥z - a∥ < ∥F.deriv
   ∥F.derivative.eval z∥ = ∥F.derivative.eval a∥ ∧
   ∀ z', F.eval z' = 0 → ∥z' - a∥ < ∥F.derivative.eval a∥ → z' = z :=
 if ha : F.eval a = 0 then ⟨a, a_is_soln hnorm ha⟩ else
-by refine ⟨soln _ _, eval_soln _ _, soln_dist_to_a_lt_deriv _ _, soln_deriv_norm _ _, soln_unique _ _⟩;
-   assumption
+by refine ⟨soln _ _, eval_soln _ _, soln_dist_to_a_lt_deriv _ _, soln_deriv_norm _ _,
+  soln_unique _ _⟩; assumption

src/data/set/basic.lean

@@ -894,7 +894,7 @@ by finish [ext_iff]
 eq_empty_of_subset_empty $ assume x ⟨hx, _⟩, hx
 
 theorem diff_eq_empty {s t : set α} : s \ t = ∅ ↔ s ⊆ t :=
-⟨assume h x hx, classical.by_contradiction $ assume : x ∉ t, show x ∈ (∅ : set α), from h ▸ ⟨hx, this⟩,
+⟨assume h x hx, by_contradiction $ assume : x ∉ t, show x ∈ (∅ : set α), from h ▸ ⟨hx, this⟩,
   assume h, eq_empty_of_subset_empty $ assume x ⟨hx, hnx⟩, hnx $ h hx⟩
 
 @[simp] theorem diff_empty {s : set α} : s \ ∅ = s :=
@@ -2449,7 +2449,7 @@ iff.rfl
 @[congr] lemma image3_congr (h : ∀ (a ∈ s) (b ∈ t) (c ∈ u), g a b c = g' a b c) :
   image3 g s t u = image3 g' s t u :=
 by { ext x,
-     split; rintro ⟨a, b, c, ha, hb, hc, rfl⟩; refine ⟨a, b, c, ha, hb, hc, by rw h a ha b hb c hc⟩ }
+     split; rintro ⟨a, b, c, ha, hb, hc, rfl⟩; exact ⟨a, b, c, ha, hb, hc, by rw h a ha b hb c hc⟩ }
 
 /-- A common special case of `image3_congr` -/
 lemma image3_congr' (h : ∀ a b c, g a b c = g' a b c) : image3 g s t u = image3 g' s t u :=

src/geometry/euclidean/basic.lean

@@ -186,7 +186,8 @@ begin
                       (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).2,
       ←real.sqrt_mul_self (mul_nonneg (norm_nonneg x) (norm_nonneg y)),
       ←real.sqrt_mul' _ (mul_self_nonneg _), pow_two,
-      real.sqrt_mul_self (mul_nonneg (norm_nonneg x) (norm_nonneg y)), real_inner_self_eq_norm_square,
+      real.sqrt_mul_self (mul_nonneg (norm_nonneg x) (norm_nonneg y)),
+      real_inner_self_eq_norm_square,
       real_inner_self_eq_norm_square],
   by_cases h : (∥x∥ * ∥y∥) = 0,
   { rw [(show ∥x∥ * ∥x∥ * (∥y∥ * ∥y∥) = (∥x∥ * ∥y∥) * (∥x∥ * ∥y∥), by ring), h, mul_zero, mul_zero,
@@ -388,8 +389,8 @@ lemma dist_smul_vadd_square (r : ℝ) (v : V) (p₁ p₂ : P) :
   dist (r • v +ᵥ p₁) p₂ * dist (r • v +ᵥ p₁) p₂ =
     ⟪v, v⟫ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫ :=
 begin
-  rw [dist_eq_norm_vsub V _ p₂, ←real_inner_self_eq_norm_square, vadd_vsub_assoc, real_inner_add_add_self,
-      real_inner_smul_left, real_inner_smul_left, real_inner_smul_right],
+  rw [dist_eq_norm_vsub V _ p₂, ←real_inner_self_eq_norm_square, vadd_vsub_assoc,
+    real_inner_add_add_self, real_inner_smul_left, real_inner_smul_left, real_inner_smul_right],
   ring
 end
 
@@ -498,7 +499,8 @@ classical.some $ inter_eq_singleton_of_nonempty_of_is_compl
   (nonempty_subtype.mp ‹_›)
   (mk'_nonempty p s.directionᗮ)
   begin
-    convert submodule.is_compl_orthogonal_of_is_complete (complete_space_coe_iff_is_complete.mp ‹_›),
+    convert submodule.is_compl_orthogonal_of_is_complete
+      (complete_space_coe_iff_is_complete.mp ‹_›),
     exact direction_mk' p s.directionᗮ
   end
 
@@ -514,7 +516,8 @@ classical.some_spec $ inter_eq_singleton_of_nonempty_of_is_compl
   (nonempty_subtype.mp ‹_›)
   (mk'_nonempty p s.directionᗮ)
   begin
-    convert submodule.is_compl_orthogonal_of_is_complete (complete_space_coe_iff_is_complete.mp ‹_›),
+    convert submodule.is_compl_orthogonal_of_is_complete
+      (complete_space_coe_iff_is_complete.mp ‹_›),
     exact direction_mk' p s.directionᗮ
   end
 
@@ -862,7 +865,8 @@ end
 
 /-- The distance between `p₁` and the reflection of `p₂` equals that
 between the reflection of `p₁` and `p₂`. -/
-lemma dist_reflection (s : affine_subspace ℝ P) [nonempty s] [complete_space s.direction] (p₁ p₂ : P) :
+lemma dist_reflection (s : affine_subspace ℝ P) [nonempty s] [complete_space s.direction]
+  (p₁ p₂ : P) :
   dist p₁ (reflection s p₂) = dist (reflection s p₁) p₂ :=
 begin
   conv_lhs { rw ←reflection_reflection s p₁ },

src/geometry/manifold/algebra/monoid.lean

@@ -34,10 +34,9 @@ we formulate the definitions and lemmas for any model.
 
 3. While smoothness of an operation implies its continuity, lemmas like
 `has_continuous_mul_of_smooth` can't be instances becausen otherwise Lean would have to search for
-`has_smooth_mul I G` with unknown `𝕜`, `E`, `H`, and
-`I : model_with_corners 𝕜 E H`. If users needs `[has_continuous_mul G]` in a proof about a smooth
-monoid, then they need to either add `[has_continuous_mul G]` as an assumption (worse) or use `haveI`
-in the proof (better). -/
+`has_smooth_mul I G` with unknown `𝕜`, `E`, `H`, and `I : model_with_corners 𝕜 E H`. If users needs
+`[has_continuous_mul G]` in a proof about a smooth monoid, then they need to either add
+`[has_continuous_mul G]` as an assumption (worse) or use `haveI` in the proof (better). -/
 library_note "Design choices about smooth algebraic structures"
 
 /-- Basic hypothesis to talk about a smooth (Lie) additive monoid or a smooth additive