Don't name hypotheses that don't need names

Changes

1 changed files (+13/-15)

• Sum.lean
  • @@ -15,7 +15,7 @@ lemma geom_sum (b : ℝ) (N : ℕ) (h₁ : 2 ≤ N) (h₂ : 2 ≤ b) : ∑ a ∈
    grind exact h₁ _ = 1 / (b - 1) - 1 / b - b / (b ^ N * (b - 1)) := by - have h₃ : b - 1 ≠ 0 := by + have : b - 1 ≠ 0 := by linarith field_simp ring
  • @@ -127,17 +127,17 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
    have h₃ : 1 < 1 + ε - 1 / (n - 1) - (n - 2) / 2 ^ (n - 1) := by suffices 1 / (n - 1) + (n - 2) / 2 ^ (n - 1) < ε by linarith if hε : 3 / 2 < ε then - have h₄ : 2 ≤ (n : ℝ) := Nat.ofNat_le_cast.mpr h₁ - have h₅ : 1 / ((n : ℝ) - 1) ≤ 1 := by + have : 2 ≤ (n : ℝ) := Nat.ofNat_le_cast.mpr h₁ + have : 1 / ((n : ℝ) - 1) ≤ 1 := by refine (div_le_one₀ ?_).mpr (by linarith) linarith suffices ((n : ℝ) - 2) / 2 ^ (n - 1) ≤ 1 / 2 by linarith - have h₆ : 2 * (n - 2) ≤ 2 ^ (n - 1) := by - if h₇ : n = 2 then - simp [h₇] + have h₄ : 2 * (n - 2) ≤ 2 ^ (n - 1) := by + if h₅ : n = 2 then + simp [h₅] else exact exp_larger n (by omega) - rw [mul_comm, ←one_mul (2 ^ (n - 1))] at h₆ + rw [mul_comm, ←one_mul (2 ^ (n - 1))] at h₄ exact (div_le_div_iff₀ (by norm_num) (by norm_num)).mpr (by norm_cast) else simp at hε
  • @@ -158,10 +158,10 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
    exact exp_larger' n (by omega) apply lt_sub_iff_add_lt'.mp have h₅ : 3 / (n : ℝ) - 1 / (n - 1) = (2 * n - 3) / (n * (n - 1)) := by - have h₆ : (n : ℝ) ≠ 0 := by + have : (n : ℝ) ≠ 0 := by rw [Nat.cast_ne_zero] omega - have h₇ : (n : ℝ) - 1 ≠ 0 := by + have : (n : ℝ) - 1 ≠ 0 := by grind field_simp ring
  • @@ -177,8 +177,7 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
    simp have h₉ : ↑(n - 2) = (n : ℝ) - 2 := by norm_cast - rw [h₇, h₈, h₉] at h₄ - exact h₄ + rwa [h₇, h₈, h₉] at h₄ have h₇ : 0 < (2 : ℝ) ^ (n - 1) := by norm_num exact (div_lt_div_iff₀ h₇ (by nlinarith)).mpr h₆
  • @@ -195,11 +194,10 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
    have h₃ : ∀ b ∈ Ico 2 n, 0 < (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := by intro b bico field_simp - have h₄ : 2 ≤ b := List.left_le_of_mem_range' bico - have h₅ : 1 < (b : ℝ) := Nat.one_lt_cast.mpr h₄ - have h₆ : 0 < (b : ℝ) ^ (n - 1) := by + have : 1 < (b : ℝ) := Nat.one_lt_cast.mpr (List.left_le_of_mem_range' bico) + have h₄ : 0 < (b : ℝ) ^ (n - 1) := by apply pow_pos (by linarith) - exact mul_pos h₆ (by linarith) + exact mul_pos h₄ (by linarith) have h₄ : 0 ≤ ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := sum_nonneg (fun b a => le_of_lt (h₃ b a)) ring_nf at h₄ field_simp at h₄