Use more pipe operators to reduce nesting in Sum.lean

Changes

1 changed files (+4/-4)

• Sum.lean
  • @@ -74,10 +74,10 @@ theorem double_sum : Tendsto (fun n : ℕ => ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    have h₃ : 2 ≤ (b : ℝ) := by norm_num exact (List.left_le_of_mem_range' bico) - have h₄ : 1 / ((b : ℝ) - 1) ≤ 1 := (div_le_one₀ (by linarith)).mpr (by linarith) + have h₄ : 1 / ((b : ℝ) - 1) ≤ 1 := div_le_one₀ (by linarith) |>.mpr (by linarith) have h₅ : 1 / (b : ℝ) ^ (n - 1) ≤ 1 / 2 ^ (n - 1) := by simp only [one_div] - exact inv_anti₀ (by norm_num) (pow_le_pow_left₀ (by norm_num) h₃ (n - 1)) + exact inv_anti₀ (by norm_num) <| pow_le_pow_left₀ (by norm_num) h₃ (n - 1) grw [h₄, h₅] simp grw [sum_le_sum h₂]
  • @@ -89,7 +89,7 @@ theorem double_sum : Tendsto (fun n : ℕ => ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    suffices ((n : ℝ) - 2) / 2 ^ (n - 1) ≤ 1 / 2 by linarith have := exp_larger n h₁ rw [mul_comm, ← one_mul (2 ^ (n - 1))] at this - exact (div_le_div_iff₀ (by norm_num) (by norm_num)).mpr (by norm_cast) + exact div_le_div_iff₀ (by norm_num) (by norm_num) |>.mpr (by norm_cast) · have : 3 / n ≤ ε := (div_le_comm₀ (by positivity) εpos).mpr <| Nat.ceil_le.mp (le_of_max_le_left nlarge) grw [← this] have : 3 / (n : ℝ) - 1 / (n - 1) = (2 * n - 3) / (n * (n - 1)) := by
  • @@ -101,7 +101,7 @@ theorem double_sum : Tendsto (fun n : ℕ => ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    rify at this grind [Nat.cast_sub] have h₃ : 0 < (2 : ℝ) ^ (n - 1) := by norm_num - exact (div_lt_div_iff₀ h₃ (by nlinarith)).mpr h₂ + exact div_lt_div_iff₀ h₃ (by nlinarith) |>.mpr h₂ · -- Less than 1 have h₂ b (bico : b ∈ Ico 2 n) : 0 < (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := by rw [one_div_pos]