awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0∞
h : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)
lift : r ≠ ∞
⊢ r < 1
have lift₁ : ∀ (r : ℝ≥0) (h : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑r : ℝ≥0∞) ^ n) atTop (𝓝 0)), (↑r : ℝ≥0∞) < 1
Tactic: lift r to NNReal
Cleared hypotheses: r, h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0∞
h : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)
⊢ r ≠ ∞
have refine : ∀ (hr : r = ∞), EventuallyEq (β := ℝ≥0∞) atTop (fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) ∞ n) fun (x : ℕ) ↦ ∞
Tactic: refine fun hr ↦ top_ne_zero (tendsto_nhds_unique (EventuallyEq.tendsto ?_) (hr ▸ h))
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
r : ℝ≥0
h : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑r : ℝ≥0∞) ^ n) atTop (𝓝 0)
⊢ (↑r : ℝ≥0∞) < 1
have h₁ : Tendsto (fun (n : ℕ) ↦ (↑r : ℝ≥0∞) ^ n) atTop (𝓝 (↑0 : ℝ≥0∞))
Tactic: rw [← coe_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0
h : Tendsto (fun (n : ℕ) ↦ (↑r : ℝ≥0∞) ^ n) atTop (𝓝 (↑0 : ℝ≥0∞))
⊢ (↑r : ℝ≥0∞) < 1
have norm_cast : ∀ (h : Tendsto (α := ℕ) (HPow.hPow r) atTop (𝓝 0)), r < 1
Tactic: norm_cast at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0∞
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 ∞) ↔ 1 < r
have refine_1 : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 ∞) → 1 < r
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0∞
refine_1 : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 ∞) → 1 < r
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 ∞) ↔ 1 < r
have refine_2 : 1 < r → Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 ∞)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0∞
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 ∞) → 1 < r
have refine_1 : r ≤ 1 → ¬Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 ∞)
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
r : ℝ≥0∞
r_le_one : r ≤ 1
h_tends : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 ∞)
⊢ False
have h_tends₁ : Membership.mem (γ := Filter ℝ≥0∞) (Filter.map (fun (n : ℕ) ↦ r ^ n) atTop) (Set.Ioi 1)
Tactic: specialize h_tends (Ioi_mem_nhds one_lt_top)
Cleared hypotheses: h_tends
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
r : ℝ≥0∞
r_le_one : r ≤ 1
h_tends : Membership.mem (γ := Filter ℝ≥0∞) (Filter.map (fun (n : ℕ) ↦ r ^ n) atTop) (Set.Ioi 1)
⊢ False
have h_tends₁ : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → 1 < r ^ b
Tactic: simp only [Filter.mem_map, mem_atTop_sets, ge_iff_le, Set.mem_preimage, Set.mem_Ioi] at h_tends
Cleared hypotheses: h_tends
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0∞
r_le_one : r ≤ 1
h_tends : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → 1 < r ^ b
⊢ False
have refine_1 : ∀ (n : ℕ) (hn : ∀ (b : ℕ), n ≤ b → 1 < r ^ b), False
Tactic: obtain ⟨n, hn⟩ := h_tends
Cleared hypotheses: h_tends
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
r : ℝ≥0∞
r_gt_one : 1 < r
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 ∞)
have obs : ∀ (h : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r⁻¹ ^ n) atTop (𝓝 0)),
  Tendsto (β := ℝ≥0∞) (fun (x : ℕ) ↦ (r⁻¹ ^ x)⁻¹) atTop (𝓝 0⁻¹)
Tactic: have obs := @Tendsto.inv ℝ≥0∞ ℕ _ _ _ (fun n ↦ (r⁻¹) ^ n) atTop 0
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
r : ℝ≥0∞
r_gt_one : 1 < r
obs :
  ∀ (h : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r⁻¹ ^ n) atTop (𝓝 0)),
    Tendsto (β := ℝ≥0∞) (fun (x : ℕ) ↦ (r⁻¹ ^ x)⁻¹) atTop (𝓝 0⁻¹)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 ∞)
have obs₁ : ∀ (h : r⁻¹ < 1), Tendsto (β := ℝ≥0∞) (fun (x : ℕ) ↦ (r⁻¹ ^ x)⁻¹) atTop (𝓝 ∞)
Tactic: simp only [ENNReal.tendsto_pow_atTop_nhds_zero_iff, inv_zero] at obs
Cleared hypotheses: obs
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
x r : ℝ≥0∞
ε : ℝ≥0
hr : r < 1
h : ∀ (n : ℕ), x ≤ (↑ε : ℝ≥0∞) * r ^ n
⊢ x = 0
have rw : x ≤ 0
Tactic: rw [← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
x r : ℝ≥0∞
ε : ℝ≥0
hr : r < 1
h : ∀ (n : ℕ), x ≤ (↑ε : ℝ≥0∞) * r ^ n
⊢ x ≤ 0
have refine : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑ε : ℝ≥0∞) * r ^ n) atTop (𝓝 0)
Tactic: refine ge_of_tendsto' (f := fun (n : ℕ) ↦ ε * r ^ n) (x := atTop) ?_ h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
x r : ℝ≥0∞
ε : ℝ≥0
hr : r < 1
h : ∀ (n : ℕ), x ≤ (↑ε : ℝ≥0∞) * r ^ n
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑ε : ℝ≥0∞) * r ^ n) atTop (𝓝 0)
have rw : Tendsto (fun (n : ℕ) ↦ (↑ε : ℝ≥0∞) * r ^ n) atTop (𝓝 ((↑ε : ℝ≥0∞) * 0))
Tactic: rw [← mul_zero (M₀ := ℝ≥0∞) (a := ε)]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
⊢ HasSum (α := ℝ) (fun (n : ℕ) ↦ (1 / 2) ^ n) 2
have h : 2 = (1 - 1 / 2)⁻¹
Tactic: convert! hasSum_geometric_of_lt_one _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
h : 2 = (1 - 1 / 2)⁻¹
⊢ HasSum (α := ℝ) (fun (n : ℕ) ↦ (1 / 2) ^ n) 2
have convert_2 : 0 ≤ 1 / 2
Tactic: convert! hasSum_geometric_of_lt_one _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
h : 2 = (1 - 1 / 2)⁻¹
convert_2 : 0 ≤ 1 / 2
⊢ HasSum (α := ℝ) (fun (n : ℕ) ↦ (1 / 2) ^ n) 2
have convert_3 : 1 / 2 < 1
Tactic: convert! hasSum_geometric_of_lt_one _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
n i : ℕ
⊢ 0 ≤ (1 / 2) ^ i
have ha : 0 ≤ 1 / 2
Tactic: apply pow_nonneg
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
n : ℕ
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.range n, (1 / 2) ^ i) 2
have this : ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i
Tactic: have : ∀ i, 0 ≤ (1 / (2 : ℝ)) ^ i := by
    intro i
    apply pow_nonneg
    norm_num
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
n : ℕ
this : ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.range n, (1 / 2) ^ i) 2
have h : Eq (α := ℝ) 2 (∑' (i : ℕ), (1 / 2) ^ i)
Tactic: convert! summable_geometric_two.sum_le_tsum (range n) (fun i _ ↦ this i)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
n : ℕ
⊢ (∑' (i : ℕ), if n ≤ i then HPow.hPow (α := ℝ) 2⁻¹ i else 0) = 2 * HPow.hPow (α := ℝ) 2⁻¹ n
have A : Summable (α := ℝ) fun (i : ℕ) ↦ if n ≤ i then HPow.hPow (α := ℝ) 2⁻¹ i else 0
Tactic: have A : Summable fun i : ℕ ↦ ite (n ≤ i) ((2⁻¹ : ℝ) ^ i) 0 := by
    simpa only [← piecewise_eq_indicator, one_div]
      using summable_geometric_two.indicator {i | n ≤ i}
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
n : ℕ
A : Summable (α := ℝ) fun (i : ℕ) ↦ if n ≤ i then HPow.hPow (α := ℝ) 2⁻¹ i else 0
⊢ (∑' (i : ℕ), if n ≤ i then HPow.hPow (α := ℝ) 2⁻¹ i else 0) = 2 * HPow.hPow (α := ℝ) 2⁻¹ n
have B : Eq (α := ℝ) (∑ i ∈ Finset.range n, if n ≤ i then HPow.hPow (α := ℝ) 2⁻¹ i else 0) 0
Tactic: have B : ((Finset.range n).sum fun i : ℕ ↦ ite (n ≤ i) ((2⁻¹ : ℝ) ^ i) 0) = 0 :=
    Finset.sum_eq_zero fun i hi ↦
      ite_eq_right_iff.2 fun h ↦ (lt_irrefl _ ((Finset.mem_range.1 hi).trans_le h)).elim
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
a : ℝ
⊢ HasSum (fun (n : ℕ) ↦ a / 2 / HPow.hPow (α := ℝ) 2 n) a
have h : Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ a / 2 / HPow.hPow (α := ℝ) 2 n) fun (i : ℕ) ↦ a / 2 * (1 / 2) ^ i
Tactic: convert!
    HasSum.mul_left (a / 2)
      (hasSum_geometric_of_lt_one (le_of_lt one_half_pos) one_half_lt_one) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
a : ℝ
h : Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ a / 2 / HPow.hPow (α := ℝ) 2 n) fun (i : ℕ) ↦ a / 2 * (1 / 2) ^ i
⊢ HasSum (fun (n : ℕ) ↦ a / 2 / HPow.hPow (α := ℝ) 2 n) a
have h₁ : a = a / 2 * (1 - 1 / 2)⁻¹
Tactic: convert!
    HasSum.mul_left (a / 2)
      (hasSum_geometric_of_lt_one (le_of_lt one_half_pos) one_half_lt_one) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
a : ℝ
⊢ Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ a / 2 / HPow.hPow (α := ℝ) 2 n) fun (i : ℕ) ↦ a / 2 * (1 / 2) ^ i
have h : ∀ (n : ℕ), a / 2 / HPow.hPow (α := ℝ) 2 n = a / 2 * (1 / 2) ^ n
Tactic: funext n
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
a : ℝ
n : ℕ
⊢ a / 2 / HPow.hPow (α := ℝ) 2 n = a / 2 * (1 / 2) ^ n
have h : a / 2 / HPow.hPow (α := ℝ) 2 n = a / 2 * (HPow.hPow (α := ℝ) 2 n)⁻¹
Tactic: simp only [one_div, inv_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun (n : ℕ) ↦ r ^ n) (1 - r)⁻¹
have apply : HasSum (fun (a : ℕ) ↦ (↑(r ^ a) : ℝ)) (↑(1 - r)⁻¹ : ℝ)
Tactic: apply NNReal.hasSum_coe.1
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun (a : ℕ) ↦ (↑r : ℝ) ^ a) (↑(1 - r) : ℝ)⁻¹
have rw : HasSum (fun (a : ℕ) ↦ (↑r : ℝ) ^ a) ((↑1 : ℝ) - (↑r : ℝ))⁻¹
Tactic: rw [NNReal.coe_sub (le_of_lt hr)]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0∞
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹
have inl : ∀ (hr : r < 1), ∑' (n : ℕ), r ^ n = (1 - r)⁻¹
Tactic: rcases lt_or_ge r 1 with hr | hr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0∞
inl : ∀ (hr : r < 1), ∑' (n : ℕ), r ^ n = (1 - r)⁻¹
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹
have inr : ∀ (hr : 1 ≤ r), ∑' (n : ℕ), r ^ n = (1 - r)⁻¹
Tactic: rcases lt_or_ge r 1 with hr | hr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0∞
hr : r < 1
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹
have inl : ∀ (r : ℝ≥0) (hr' : (↑r : ℝ≥0∞) < 1) (hr : (↑r : ℝ≥0∞) < 1), ∑' (n : ℕ), (↑r : ℝ≥0∞) ^ n = (1 - (↑r : ℝ≥0∞))⁻¹
Tactic: rcases ENNReal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
r : ℝ≥0
hr' : (↑r : ℝ≥0∞) < 1
hr : (↑r : ℝ≥0∞) < 1
⊢ ∑' (n : ℕ), (↑r : ℝ≥0∞) ^ n = (1 - (↑r : ℝ≥0∞))⁻¹
have hr'₁ : r < 1
Tactic: norm_cast at *
Cleared hypotheses: hr', hr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0
hr' hr : r < 1
⊢ ∑' (n : ℕ), (↑(r ^ n) : ℝ≥0∞) = (↑(1 - r) : ℝ≥0∞)⁻¹
have h : (↑(1 - r) : ℝ≥0∞)⁻¹ = (↑(1 - r)⁻¹ : ℝ≥0∞)
Tactic: convert! ENNReal.tsum_coe_eq (NNReal.hasSum_geometric hr)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0
hr' hr : r < 1
⊢ (↑(1 - r) : ℝ≥0∞)⁻¹ = (↑(1 - r)⁻¹ : ℝ≥0∞)
have h : (↑(1 - r) : ℝ≥0∞)⁻¹ = (↑(1 - r) : ℝ≥0∞)⁻¹
Tactic: rw [ENNReal.coe_inv <| ne_of_gt <| tsub_pos_iff_lt.2 hr, coe_sub, coe_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0
hr' hr : r < 1
h : (↑(1 - r) : ℝ≥0∞)⁻¹ = (↑(1 - r) : ℝ≥0∞)⁻¹
⊢ (↑(1 - r) : ℝ≥0∞)⁻¹ = (↑(1 - r)⁻¹ : ℝ≥0∞)
have h₁ : ((↑1 : ℝ≥0∞) - (↑r : ℝ≥0∞))⁻¹ = ((↑1 : ℝ≥0∞) - (↑r : ℝ≥0∞))⁻¹
Tactic: rw [ENNReal.coe_inv <| ne_of_gt <| tsub_pos_iff_lt.2 hr, coe_sub, coe_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0
hr' hr : r < 1
h : (↑(1 - r) : ℝ≥0∞)⁻¹ = (↑(1 - r) : ℝ≥0∞)⁻¹
h₁ : ((↑1 : ℝ≥0∞) - (↑r : ℝ≥0∞))⁻¹ = ((↑1 : ℝ≥0∞) - (↑r : ℝ≥0∞))⁻¹
⊢ (↑(1 - r) : ℝ≥0∞)⁻¹ = (↑(1 - r)⁻¹ : ℝ≥0∞)
have h₂ : (1 - (↑r : ℝ≥0∞))⁻¹ = (1 - (↑r : ℝ≥0∞))⁻¹
Tactic: rw [ENNReal.coe_inv <| ne_of_gt <| tsub_pos_iff_lt.2 hr, coe_sub, coe_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹
have inr : ∀ b < ∞, ∃ (i : ℕ), b < ∑ a ∈ Finset.range i, r ^ a
Tactic: rw [tsub_eq_zero_iff_le.mpr hr, ENNReal.inv_zero, ENNReal.tsum_eq_iSup_nat, iSup_eq_top]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ∀ b < ∞, ∃ (i : ℕ), b < ∑ a ∈ Finset.range i, r ^ a
have inr : ∀ (a : ℝ≥0∞) (ha : a < ∞) (n : ℕ) (hn : a < (↑n : ℝ≥0∞)), LE.le (α := ℝ≥0∞) (↑n : ℝ≥0∞) (∑ a ∈ Finset.range n, r ^ a)
Tactic: refine fun a ha ↦
      (ENNReal.exists_nat_gt (lt_top_iff_ne_top.1 ha)).imp fun n hn ↦ lt_of_lt_of_le hn ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ∞
n : ℕ
hn : a < (↑n : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (↑n : ℝ≥0∞) (∑ i ∈ Finset.range n, 1)
have rw : (↑n : ℝ≥0∞) = HSMul.hSMul (β := ℝ≥0∞) (#(Finset.range n)) 1
Tactic: rw [sum_const, nsmul_one, card_range]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ∞
n : ℕ
hn : a < (↑n : ℝ≥0∞)
rw : (↑n : ℝ≥0∞) = HSMul.hSMul (β := ℝ≥0∞) (#(Finset.range n)) 1
⊢ Eq (α := ℝ≥0∞) (↑n : ℝ≥0∞) (∑ i ∈ Finset.range n, 1)
have rw₁ : Eq (α := ℝ≥0∞) (↑n : ℝ≥0∞) (↑(#(Finset.range n)) : ℝ≥0∞)
Tactic: rw [sum_const, nsmul_one, card_range]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ∞
n : ℕ
hn : a < (↑n : ℝ≥0∞)
rw : (↑n : ℝ≥0∞) = HSMul.hSMul (β := ℝ≥0∞) (#(Finset.range n)) 1
rw₁ : Eq (α := ℝ≥0∞) (↑n : ℝ≥0∞) (↑(#(Finset.range n)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (↑n : ℝ≥0∞) (∑ i ∈ Finset.range n, 1)
have rw₂ : Eq (α := ℝ≥0∞) (↑n : ℝ≥0∞) (↑n : ℝ≥0∞)
Tactic: rw [sum_const, nsmul_one, card_range]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ∞
n : ℕ
hn : a < (↑n : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, 1) (∑ i ∈ Finset.range n, r ^ i)
have h : ∀ i ∈ Finset.range n, 1 ≤ r ^ i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ∞
n : ℕ
hn : a < (↑n : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (↑n : ℝ≥0∞) (∑ a ∈ Finset.range n, r ^ a)
have i : Eq (α := ℝ≥0∞) (↑n : ℝ≥0∞) (∑ i ∈ Finset.range n, 1)
Tactic: calc
      (n : ℝ≥0∞) = ∑ i ∈ range n, 1 := by rw [sum_const, nsmul_one, card_range]
      _ ≤ ∑ i ∈ range n, r ^ i := by gcongr; apply one_le_pow₀ hr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ∞
n : ℕ
hn : a < (↑n : ℝ≥0∞)
i : Eq (α := ℝ≥0∞) (↑n : ℝ≥0∞) (∑ i ∈ Finset.range n, 1)
⊢ LE.le (α := ℝ≥0∞) (↑n : ℝ≥0∞) (∑ a ∈ Finset.range n, r ^ a)
have i₁ : LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, 1) (∑ i ∈ Finset.range n, r ^ i)
Tactic: calc
      (n : ℝ≥0∞) = ∑ i ∈ range n, 1 := by rw [sum_const, nsmul_one, card_range]
      _ ≤ ∑ i ∈ range n, r ^ i := by gcongr; apply one_le_pow₀ hr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
⊢ Eq (α := ℝ≥0∞) (∑' (m : ℕ), HPow.hPow (α := ℝ≥0∞) 2 (HSub.hSub (α := ℤ) (-1) (↑m : ℤ))) 1
have simp_rw : HMul.hMul (α := ℝ≥0∞) 2⁻¹ 2 = 1
Tactic: simp_rw [neg_sub_left, ENNReal.zpow_neg, ← Nat.cast_one (R := ℤ), ← Nat.cast_add, zpow_natCast,
    ENNReal.inv_pow, ENNReal.tsum_geometric_add_one, one_sub_inv_two, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ CauchySeq f
have refine : Ne (α := ℝ≥0∞) (∑' (n : ℕ), C * r ^ n) ∞
Tactic: refine cauchySeq_of_edist_le_of_tsum_ne_top _ hu ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ Ne (α := ℝ≥0∞) (∑' (n : ℕ), C * r ^ n) ∞
have rw : C * (1 - r)⁻¹ ≠ ∞
Tactic: rw [ENNReal.tsum_mul_left, ENNReal.tsum_geometric]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ C * (1 - r)⁻¹ ≠ ∞
have finiteness : 1 - r ≠ 0 → C * (1 - r)⁻¹ ≠ ∞
Tactic: finiteness [(tsub_pos_iff_lt.2 hr).ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
r C : ℝ≥0∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ edist (f n) a ≤ C * r ^ n / (1 - r)
have h : C * r ^ n / (1 - r) = ∑' (m : ℕ), C * r ^ (n + m)
Tactic: convert! edist_le_tsum_of_edist_le_of_tendsto _ hu ha _
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / HPow.hPow (α := ℝ≥0∞) 2 n
⊢ CauchySeq f
have hu₁ : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
Tactic: simp only [div_eq_mul_inv, ENNReal.inv_pow] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
⊢ CauchySeq f
have refine : LT.lt (α := ℝ≥0∞) 2⁻¹ 1
Tactic: refine cauchySeq_of_edist_le_geometric 2⁻¹ C ?_ hC hu
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
C : ℝ≥0∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / HPow.hPow (α := ℝ≥0∞) 2 n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ edist (f n) a ≤ 2 * C / HPow.hPow (α := ℝ≥0∞) 2 n
have simp : ∀ (hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n),
  edist (f n) a ≤ 2 * C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
Tactic: simp only [div_eq_mul_inv, ENNReal.inv_pow] at *
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
C : ℝ≥0∞
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
⊢ edist (f n) a ≤ 2 * C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
have rw : edist (f n) a ≤ C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n * 2
Tactic: rw [mul_assoc, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
C : ℝ≥0∞
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
⊢ edist (f n) a ≤ C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n * 2
have h : C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n * 2 = C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n / HSub.hSub (α := ℝ≥0∞) 1 2⁻¹
Tactic: convert! edist_le_of_edist_le_geometric_of_tendsto 2⁻¹ C hu ha n using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
C : ℝ≥0∞
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
⊢ C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n * 2 = C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n / HSub.hSub (α := ℝ≥0∞) 1 2⁻¹
have h : C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n * 2 = C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n / 2⁻¹
Tactic: rw [ENNReal.one_sub_inv_two, div_eq_mul_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
C : ℝ≥0∞
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
h : C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n * 2 = C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n / 2⁻¹
⊢ C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n * 2 = C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n / HSub.hSub (α := ℝ≥0∞) 1 2⁻¹
have h₁ : C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n * 2 = C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n * 2⁻¹⁻¹
Tactic: rw [ENNReal.one_sub_inv_two, div_eq_mul_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
C : ℝ≥0∞
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
h : C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n * 2 = C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n / 2⁻¹
h₁ : C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n * 2 = C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n * 2⁻¹⁻¹
⊢ C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n * 2 = C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n / HSub.hSub (α := ℝ≥0∞) 1 2⁻¹
have h₂ : C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n * 2 = C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n * 2
Tactic: rw [ENNReal.one_sub_inv_two, div_eq_mul_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ HasSum (fun (n : ℕ) ↦ C * r ^ n) (C / (1 - r))
have inl : ∀ (hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ 0 * r ^ n), HasSum (fun (n : ℕ) ↦ 0 * r ^ n) (0 / (1 - r))
Tactic: rcases sign_cases_of_C_mul_pow_nonneg fun n ↦ dist_nonneg.trans (hu n) with (rfl | ⟨_, r₀⟩)
Cleared hypotheses: C, hu
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
inl : ∀ (hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ 0 * r ^ n), HasSum (fun (n : ℕ) ↦ 0 * r ^ n) (0 / (1 - r))
⊢ HasSum (fun (n : ℕ) ↦ C * r ^ n) (C / (1 - r))
have inr : 0 < C → ∀ (r₀ : 0 ≤ r), HasSum (fun (n : ℕ) ↦ C * r ^ n) (C / (1 - r))
Tactic: rcases sign_cases_of_C_mul_pow_nonneg fun n ↦ dist_nonneg.trans (hu n) with (rfl | ⟨_, r₀⟩)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
left : 0 < C
r₀ : 0 ≤ r
⊢ HasSum (fun (n : ℕ) ↦ C * r ^ n) (C / (1 - r))
have inr : HasSum (HPow.hPow r) (1 - r)⁻¹
Tactic: refine HasSum.mul_left C ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ dist (f n) a ≤ C * r ^ n / (1 - r)
have this : HasSum (fun (n : ℕ) ↦ C * r ^ n) (C / (1 - r))
Tactic: have := aux_hasSum_of_le_geometric hr hu
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun (n : ℕ) ↦ C * r ^ n) (C / (1 - r))
⊢ dist (f n) a ≤ C * r ^ n / (1 - r)
have h : C * r ^ n / (1 - r) = ∑' (m : ℕ), C * r ^ (n + m)
Tactic: convert! dist_le_tsum_of_dist_le_of_tendsto _ hu ⟨_, this⟩ ha n
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun (n : ℕ) ↦ C * r ^ n) (C / (1 - r))
⊢ C * r ^ n / (1 - r) = ∑' (m : ℕ), C * r ^ (n + m)
have h : C / (1 - r) * r ^ n = ∑' (m : ℕ), r ^ n * (C * r ^ m)
Tactic: simp only [pow_add, mul_left_comm C, mul_div_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun (n : ℕ) ↦ C * r ^ n) (C / (1 - r))
⊢ C / (1 - r) * r ^ n = ∑' (m : ℕ), r ^ n * (C * r ^ m)
have h : r ^ n * (C / (1 - r)) = ∑' (m : ℕ), r ^ n * (C * r ^ m)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
C : ℝ
f : ℕ → α
hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / HPow.hPow (α := ℝ) 2 n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ dist (f n) a ≤ C / HPow.hPow (α := ℝ) 2 n
have h : C / HPow.hPow (α := ℝ) 2 n = ∑' (m : ℕ), C / 2 / HPow.hPow (α := ℝ) 2 (n + m)
Tactic: convert! dist_le_tsum_of_dist_le_of_tendsto _ hu₂ (summable_geometric_two' C) ha n
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
C : ℝ
f : ℕ → α
hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / HPow.hPow (α := ℝ) 2 n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ C / HPow.hPow (α := ℝ) 2 n = ∑' (m : ℕ), C / 2 / HPow.hPow (α := ℝ) 2 (n + m)
have h : C / HPow.hPow (α := ℝ) 2 n = ∑' (m : ℕ), C / 2 / HPow.hPow (α := ℝ) 2 m / HPow.hPow (α := ℝ) 2 n
Tactic: simp only [add_comm n, pow_add, ← div_div]