awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
ha : a ≠ 1
n : ℕ
zero : arithGeom a b u₀ 0 = HPow.hPow (β := ℕ) a 0 * (u₀ - b / (1 - a)) + b / (1 - a)
⊢ arithGeom a b u₀ n = a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)
have succ : ∀ (n : ℕ) (hn : arithGeom a b u₀ n = a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)),
  arithGeom a b u₀ (n + 1) = a ^ (n + 1) * (u₀ - b / (1 - a)) + b / (1 - a)
Tactic: induction n with
  | zero => simp
  | succ n hn => unfold arithGeom; grind
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
ha : a ≠ 1
⊢ arithGeom a b u₀ = fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)
have h : ∀ (x : ℕ), arithGeom a b u₀ x = a ^ x * (u₀ - b / (1 - a)) + b / (1 - a)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b : R
inst : Field R
ha : a ≠ 1
n : ℕ
⊢ arithGeom a b b n = b * (1 - a ^ (n + 1)) / (1 - a)
have rw : a ^ n * (b - b / (1 - a)) + b / (1 - a) = b * (1 - a ^ (n + 1)) / (1 - a)
Tactic: rw [arithGeom_eq ha n]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b : R
inst : Field R
ha : a ≠ 1
n : ℕ
⊢ arithGeom a b b n = b * (a ^ (n + 1) - 1) / (a - 1)
have rw : b * (1 - a ^ (n + 1)) / (1 - a) = b * (a ^ (n + 1) - 1) / (a - 1)
Tactic: rw [arithGeom_same_eq_mul_div' ha n, ← neg_sub _ a, div_neg,
    ← neg_sub _ (a ^ (n + 1)), mul_neg, neg_div, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b : R
inst : Field R
ha : a ≠ 1
n : ℕ
rw : b * (1 - a ^ (n + 1)) / (1 - a) = b * (a ^ (n + 1) - 1) / (a - 1)
⊢ arithGeom a b b n = b * (a ^ (n + 1) - 1) / (a - 1)
have rw₁ : b * (1 - a ^ (n + 1)) / (1 - a) = b * (a ^ (n + 1) - 1) / -(1 - a)
Tactic: rw [arithGeom_same_eq_mul_div' ha n, ← neg_sub _ a, div_neg,
    ← neg_sub _ (a ^ (n + 1)), mul_neg, neg_div, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b : R
inst : Field R
ha : a ≠ 1
n : ℕ
rw : b * (1 - a ^ (n + 1)) / (1 - a) = b * (a ^ (n + 1) - 1) / (a - 1)
rw₁ : b * (1 - a ^ (n + 1)) / (1 - a) = b * (a ^ (n + 1) - 1) / -(1 - a)
⊢ arithGeom a b b n = b * (a ^ (n + 1) - 1) / (a - 1)
have rw₂ : b * (1 - a ^ (n + 1)) / (1 - a) = -(b * (a ^ (n + 1) - 1) / (1 - a))
Tactic: rw [arithGeom_same_eq_mul_div' ha n, ← neg_sub _ a, div_neg,
    ← neg_sub _ (a ^ (n + 1)), mul_neg, neg_div, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b : R
inst : Field R
ha : a ≠ 1
n : ℕ
rw : b * (1 - a ^ (n + 1)) / (1 - a) = b * (a ^ (n + 1) - 1) / (a - 1)
rw₁ : b * (1 - a ^ (n + 1)) / (1 - a) = b * (a ^ (n + 1) - 1) / -(1 - a)
rw₂ : b * (1 - a ^ (n + 1)) / (1 - a) = -(b * (a ^ (n + 1) - 1) / (1 - a))
⊢ arithGeom a b b n = b * (a ^ (n + 1) - 1) / (a - 1)
have rw₃ : b * (1 - a ^ (n + 1)) / (1 - a) = -(b * -(1 - a ^ (n + 1)) / (1 - a))
Tactic: rw [arithGeom_same_eq_mul_div' ha n, ← neg_sub _ a, div_neg,
    ← neg_sub _ (a ^ (n + 1)), mul_neg, neg_div, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b : R
inst : Field R
ha : a ≠ 1
n : ℕ
rw : b * (1 - a ^ (n + 1)) / (1 - a) = b * (a ^ (n + 1) - 1) / (a - 1)
rw₁ : b * (1 - a ^ (n + 1)) / (1 - a) = b * (a ^ (n + 1) - 1) / -(1 - a)
rw₂ : b * (1 - a ^ (n + 1)) / (1 - a) = -(b * (a ^ (n + 1) - 1) / (1 - a))
rw₃ : b * (1 - a ^ (n + 1)) / (1 - a) = -(b * -(1 - a ^ (n + 1)) / (1 - a))
⊢ arithGeom a b b n = b * (a ^ (n + 1) - 1) / (a - 1)
have rw₄ : b * (1 - a ^ (n + 1)) / (1 - a) = -(-(b * (1 - a ^ (n + 1))) / (1 - a))
Tactic: rw [arithGeom_same_eq_mul_div' ha n, ← neg_sub _ a, div_neg,
    ← neg_sub _ (a ^ (n + 1)), mul_neg, neg_div, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b : R
inst : Field R
ha : a ≠ 1
n : ℕ
rw : b * (1 - a ^ (n + 1)) / (1 - a) = b * (a ^ (n + 1) - 1) / (a - 1)
rw₁ : b * (1 - a ^ (n + 1)) / (1 - a) = b * (a ^ (n + 1) - 1) / -(1 - a)
rw₂ : b * (1 - a ^ (n + 1)) / (1 - a) = -(b * (a ^ (n + 1) - 1) / (1 - a))
rw₃ : b * (1 - a ^ (n + 1)) / (1 - a) = -(b * -(1 - a ^ (n + 1)) / (1 - a))
rw₄ : b * (1 - a ^ (n + 1)) / (1 - a) = -(-(b * (1 - a ^ (n + 1))) / (1 - a))
⊢ arithGeom a b b n = b * (a ^ (n + 1) - 1) / (a - 1)
have rw₅ : b * (1 - a ^ (n + 1)) / (1 - a) = - -(b * (1 - a ^ (n + 1)) / (1 - a))
Tactic: rw [arithGeom_same_eq_mul_div' ha n, ← neg_sub _ a, div_neg,
    ← neg_sub _ (a ^ (n + 1)), mul_neg, neg_div, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b : R
inst : Field R
ha : a ≠ 1
n : ℕ
rw : b * (1 - a ^ (n + 1)) / (1 - a) = b * (a ^ (n + 1) - 1) / (a - 1)
rw₁ : b * (1 - a ^ (n + 1)) / (1 - a) = b * (a ^ (n + 1) - 1) / -(1 - a)
rw₂ : b * (1 - a ^ (n + 1)) / (1 - a) = -(b * (a ^ (n + 1) - 1) / (1 - a))
rw₃ : b * (1 - a ^ (n + 1)) / (1 - a) = -(b * -(1 - a ^ (n + 1)) / (1 - a))
rw₄ : b * (1 - a ^ (n + 1)) / (1 - a) = -(-(b * (1 - a ^ (n + 1))) / (1 - a))
rw₅ : b * (1 - a ^ (n + 1)) / (1 - a) = - -(b * (1 - a ^ (n + 1)) / (1 - a))
⊢ arithGeom a b b n = b * (a ^ (n + 1) - 1) / (a - 1)
have rw₆ : b * (1 - a ^ (n + 1)) / (1 - a) = b * (1 - a ^ (n + 1)) / (1 - a)
Tactic: rw [arithGeom_same_eq_mul_div' ha n, ← neg_sub _ a, div_neg,
    ← neg_sub _ (a ^ (n + 1)), mul_neg, neg_div, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b : R
inst : Field R
ha : a ≠ 1
n : ℕ
⊢ arithGeom a b 0 n = b * (1 - a ^ n) / (1 - a)
have rw : a ^ n * (0 - b / (1 - a)) + b / (1 - a) = b * (1 - a ^ n) / (1 - a)
Tactic: rw [arithGeom_eq ha n]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b : R
inst : Field R
ha : a ≠ 1
n : ℕ
⊢ arithGeom a b 0 n = b * (a ^ n - 1) / (a - 1)
have rw : b * (1 - a ^ n) / (1 - a) = b * (a ^ n - 1) / (a - 1)
Tactic: rw [arithGeom_zero_eq_mul_div' ha n, ← neg_sub _ a, div_neg, ← neg_sub _ (a ^ n), mul_neg,
    neg_div, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b : R
inst : Field R
ha : a ≠ 1
n : ℕ
rw : b * (1 - a ^ n) / (1 - a) = b * (a ^ n - 1) / (a - 1)
⊢ arithGeom a b 0 n = b * (a ^ n - 1) / (a - 1)
have rw₁ : b * (1 - a ^ n) / (1 - a) = b * (a ^ n - 1) / -(1 - a)
Tactic: rw [arithGeom_zero_eq_mul_div' ha n, ← neg_sub _ a, div_neg, ← neg_sub _ (a ^ n), mul_neg,
    neg_div, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b : R
inst : Field R
ha : a ≠ 1
n : ℕ
rw : b * (1 - a ^ n) / (1 - a) = b * (a ^ n - 1) / (a - 1)
rw₁ : b * (1 - a ^ n) / (1 - a) = b * (a ^ n - 1) / -(1 - a)
⊢ arithGeom a b 0 n = b * (a ^ n - 1) / (a - 1)
have rw₂ : b * (1 - a ^ n) / (1 - a) = -(b * (a ^ n - 1) / (1 - a))
Tactic: rw [arithGeom_zero_eq_mul_div' ha n, ← neg_sub _ a, div_neg, ← neg_sub _ (a ^ n), mul_neg,
    neg_div, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b : R
inst : Field R
ha : a ≠ 1
n : ℕ
rw : b * (1 - a ^ n) / (1 - a) = b * (a ^ n - 1) / (a - 1)
rw₁ : b * (1 - a ^ n) / (1 - a) = b * (a ^ n - 1) / -(1 - a)
rw₂ : b * (1 - a ^ n) / (1 - a) = -(b * (a ^ n - 1) / (1 - a))
⊢ arithGeom a b 0 n = b * (a ^ n - 1) / (a - 1)
have rw₃ : b * (1 - a ^ n) / (1 - a) = -(b * -(1 - a ^ n) / (1 - a))
Tactic: rw [arithGeom_zero_eq_mul_div' ha n, ← neg_sub _ a, div_neg, ← neg_sub _ (a ^ n), mul_neg,
    neg_div, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b : R
inst : Field R
ha : a ≠ 1
n : ℕ
rw : b * (1 - a ^ n) / (1 - a) = b * (a ^ n - 1) / (a - 1)
rw₁ : b * (1 - a ^ n) / (1 - a) = b * (a ^ n - 1) / -(1 - a)
rw₂ : b * (1 - a ^ n) / (1 - a) = -(b * (a ^ n - 1) / (1 - a))
rw₃ : b * (1 - a ^ n) / (1 - a) = -(b * -(1 - a ^ n) / (1 - a))
⊢ arithGeom a b 0 n = b * (a ^ n - 1) / (a - 1)
have rw₄ : b * (1 - a ^ n) / (1 - a) = -(-(b * (1 - a ^ n)) / (1 - a))
Tactic: rw [arithGeom_zero_eq_mul_div' ha n, ← neg_sub _ a, div_neg, ← neg_sub _ (a ^ n), mul_neg,
    neg_div, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b : R
inst : Field R
ha : a ≠ 1
n : ℕ
rw : b * (1 - a ^ n) / (1 - a) = b * (a ^ n - 1) / (a - 1)
rw₁ : b * (1 - a ^ n) / (1 - a) = b * (a ^ n - 1) / -(1 - a)
rw₂ : b * (1 - a ^ n) / (1 - a) = -(b * (a ^ n - 1) / (1 - a))
rw₃ : b * (1 - a ^ n) / (1 - a) = -(b * -(1 - a ^ n) / (1 - a))
rw₄ : b * (1 - a ^ n) / (1 - a) = -(-(b * (1 - a ^ n)) / (1 - a))
⊢ arithGeom a b 0 n = b * (a ^ n - 1) / (a - 1)
have rw₅ : b * (1 - a ^ n) / (1 - a) = - -(b * (1 - a ^ n) / (1 - a))
Tactic: rw [arithGeom_zero_eq_mul_div' ha n, ← neg_sub _ a, div_neg, ← neg_sub _ (a ^ n), mul_neg,
    neg_div, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b : R
inst : Field R
ha : a ≠ 1
n : ℕ
rw : b * (1 - a ^ n) / (1 - a) = b * (a ^ n - 1) / (a - 1)
rw₁ : b * (1 - a ^ n) / (1 - a) = b * (a ^ n - 1) / -(1 - a)
rw₂ : b * (1 - a ^ n) / (1 - a) = -(b * (a ^ n - 1) / (1 - a))
rw₃ : b * (1 - a ^ n) / (1 - a) = -(b * -(1 - a ^ n) / (1 - a))
rw₄ : b * (1 - a ^ n) / (1 - a) = -(-(b * (1 - a ^ n)) / (1 - a))
rw₅ : b * (1 - a ^ n) / (1 - a) = - -(b * (1 - a ^ n) / (1 - a))
⊢ arithGeom a b 0 n = b * (a ^ n - 1) / (a - 1)
have rw₆ : b * (1 - a ^ n) / (1 - a) = b * (1 - a ^ n) / (1 - a)
Tactic: rw [arithGeom_zero_eq_mul_div' ha n, ← neg_sub _ a, div_neg, ← neg_sub _ (a ^ n), mul_neg,
    neg_div, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha_pos : 0 < a
ha_ne : a ≠ 1
h0 : b / (1 - a) < u₀
n : ℕ
hn : b / (1 - a) < arithGeom a b u₀ n
⊢ b / (1 - a) < arithGeom a b u₀ (n + 1)
have calc : b / (1 - a) = a * (b / (1 - a)) + b
Tactic: calc b / (1 - a)
    _ = a * (b / (1 - a)) + b := by grind
    _ < a * arithGeom a b u₀ n + b := by gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha_pos : 0 < a
ha_ne : a ≠ 1
h0 : b / (1 - a) < u₀
n : ℕ
hn : b / (1 - a) < arithGeom a b u₀ n
calc : b / (1 - a) = a * (b / (1 - a)) + b
⊢ b / (1 - a) < arithGeom a b u₀ (n + 1)
have calc₁ : a * (b / (1 - a)) + b < a * arithGeom a b u₀ n + b
Tactic: calc b / (1 - a)
    _ = a * (b / (1 - a)) + b := by grind
    _ < a * arithGeom a b u₀ n + b := by gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha_pos : 0 < a
ha_ne : a ≠ 1
h0 : b / (1 - a) < u₀
n : ℕ
⊢ b / (1 - a) < arithGeom a b u₀ n
have zero : b / (1 - a) < arithGeom a b u₀ 0
Tactic: induction n with
  | zero => exact h0
  | succ n hn =>
    calc b / (1 - a)
    _ = a * (b / (1 - a)) + b := by grind
    _ < a * arithGeom a b u₀ n + b := by gcongr
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha_pos : 0 < a
ha_ne : a ≠ 1
h0 : b / (1 - a) < u₀
n : ℕ
zero : b / (1 - a) < arithGeom a b u₀ 0
⊢ b / (1 - a) < arithGeom a b u₀ n
have succ : ∀ (n : ℕ) (hn : b / (1 - a) < arithGeom a b u₀ n), b / (1 - a) < arithGeom a b u₀ (n + 1)
Tactic: induction n with
  | zero => exact h0
  | succ n hn =>
    calc b / (1 - a)
    _ = a * (b / (1 - a)) + b := by grind
    _ < a * arithGeom a b u₀ n + b := by gcongr
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha : 1 < a
h0 : b / (1 - a) < u₀
⊢ StrictMono (arithGeom a b u₀)
have refine : ∀ (n : ℕ), arithGeom a b u₀ n < arithGeom a b u₀ (n + 1)
Tactic: refine strictMono_nat_of_lt_succ fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (hypothesis)
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha : 1 < a
h0 : b / (1 - a) < u₀
n : ℕ
⊢ arithGeom a b u₀ n < arithGeom a b u₀ (n + 1)
have h_lt : b / (1 - a) < arithGeom a b u₀ n
Tactic: have h_lt : b / (1 - a) < arithGeom a b u₀ n := div_lt_arithGeom (by positivity) ha.ne' h0 n
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (hypothesis)
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha : 1 < a
h0 : b / (1 - a) < u₀
n : ℕ
h_lt : b / (1 - a) < arithGeom a b u₀ n
⊢ arithGeom a b u₀ n < arithGeom a b u₀ (n + 1)
have h_lt₁ : arithGeom a b u₀ n * (1 - a) < b
Tactic: rw [div_lt_iff_of_neg (sub_neg.mpr ha)] at h_lt
Cleared hypotheses: h_lt
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha : 1 < a
h0 : b / (1 - a) < u₀
n : ℕ
h_lt : arithGeom a b u₀ n * (1 - a) < b
⊢ arithGeom a b u₀ n < arithGeom a b u₀ (n + 1)
have rw : arithGeom a b u₀ n < a * arithGeom a b u₀ n + b
Tactic: rw [arithGeom_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha : 1 < a
h0 : b / (1 - a) < u₀
n : ℕ
h_lt : arithGeom a b u₀ n * (1 - a) < b
⊢ arithGeom a b u₀ n < a * arithGeom a b u₀ n + b
have linarith : a * arithGeom a b u₀ n + b ≤ arithGeom a b u₀ n →
  arithGeom a b u₀ n * (1 - a) - b + (a * arithGeom a b u₀ n + b - arithGeom a b u₀ n) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
ha : 1 < a
h0 : b / (1 - a) < u₀
⊢ Tendsto (arithGeom a b u₀) atTop atTop
have rw : Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)) atTop atTop
Tactic: rw [arithGeom_eq' ha.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
ha : 1 < a
h0 : b / (1 - a) < u₀
⊢ Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)) atTop atTop
have refine : Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a))) atTop atTop
Tactic: refine tendsto_atTop_add_const_right _ _ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
ha : 1 < a
h0 : b / (1 - a) < u₀
⊢ Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a))) atTop atTop
have refine : Tendsto (α := ℕ) (HPow.hPow a) atTop atTop
Tactic: refine Tendsto.atTop_mul_const (sub_pos.mpr h0) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : TopologicalSpace R
inst_5 : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
⊢ Tendsto (arithGeom a b u₀) atTop (𝓝 (b / (1 - a)))
have rw : Tendsto (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)) atTop (𝓝 (b / (1 - a)))
Tactic: rw [arithGeom_eq' ha.ne]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : TopologicalSpace R
inst_5 : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
| 𝓝 (b / (1 - a))
have rw : 𝓝 (0 + b / (1 - a))
Tactic: rw [← zero_add (b / (1 - a))]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : TopologicalSpace R
inst_5 : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
⊢ Tendsto (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)) atTop (𝓝 (b / (1 - a)))
have conv_rhs : Tendsto (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)) atTop (𝓝 (0 + b / (1 - a)))
Tactic: conv_rhs => rw [← zero_add (b / (1 - a))]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : TopologicalSpace R
inst_5 : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
⊢ Tendsto (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)) atTop (𝓝 (0 + b / (1 - a)))
have refine : Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a))) atTop (𝓝 0)
Tactic: refine Tendsto.add ?_ tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : TopologicalSpace R
inst_5 : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
| 𝓝 0
have rw : 𝓝 (0 * (u₀ - b / (1 - a)))
Tactic: rw [← zero_mul (u₀ - (b / (1 - a)))]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : TopologicalSpace R
inst_5 : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
⊢ Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a))) atTop (𝓝 0)
have conv_rhs : Tendsto (fun (n : ℕ) ↦ a ^ n * (u₀ - b / (1 - a))) atTop (𝓝 (0 * (u₀ - b / (1 - a))))
Tactic: conv_rhs => rw [← zero_mul (u₀ - (b / (1 - a)))]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
𝕜 : Type u_4
inst : Semiring 𝕜
inst_1 : Algebra ℚ≥0 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
⊢ Tendsto (α := ℕ) (β := 𝕜) (comp (β := ℚ≥0) (⇑(algebraMap ℚ≥0 𝕜) : (a : ℚ≥0) → 𝕜) fun (n : ℕ) ↦ (↑n : ℚ≥0)⁻¹) atTop
    (𝓝 0)
have h : Eq (α := 𝕜) (0 : 𝕜) ((algebraMap ℚ≥0 𝕜 : (a : ℚ≥0) → 𝕜) 0 : 𝕜)
Tactic: convert! (continuous_algebraMap ℚ≥0 𝕜).continuousAt.tendsto.comp tendsto_inv_atTop_nhds_zero_nat
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
𝕜 : Type u_4
inst : Semiring 𝕜
inst_1 : Algebra ℚ≥0 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
⊢ Eq (α := 𝕜) (0 : 𝕜) ((algebraMap ℚ≥0 𝕜 : (a : ℚ≥0) → 𝕜) 0 : 𝕜)
have h : Eq.{u_4 + 1} (α := 𝕜) 0 0
Tactic: rw [map_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
𝕜 : Type u_4
inst : DivisionSemiring 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ (↑n : 𝕜)⁻¹) atTop (𝓝 0)
have h : ∀ (x : ℕ), Eq (α := 𝕜) (↑x : 𝕜)⁻¹ (comp (β := ℚ≥0) (⇑(algebraMap ℚ≥0 𝕜) : (a : ℚ≥0) → 𝕜) (fun (n : ℕ) ↦ (↑n : ℚ≥0)⁻¹) x)
Tactic: convert! NNRat.tendsto_algebraMap_inv_atTop_nhds_zero_nat 𝕜
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
⊢ Eq (α := (n : ℕ) → EReal) (fun (n : ℕ) ↦ C / (↑n : EReal)) fun (n : ℕ) ↦ (↑(C.toReal / (↑n : ℝ)) : EReal)
have h₁ : ∀ (n : ℕ), C / (↑n : EReal) = (↑(C.toReal / (↑n : ℝ)) : EReal)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
n : ℕ
⊢ C / (↑n : EReal) = (↑(C.toReal / (↑n : ℝ)) : EReal)
have h₁ : (↑C.toReal : EReal) / (↑n : EReal) = (↑(C.toReal / (↑n : ℝ)) : EReal)
Tactic: nth_rw 1 [← coe_toReal h' h, ← coe_coe_eq_natCast n, ← coe_div C.toReal n]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
n : ℕ
h₁ : (↑C.toReal : EReal) / (↑n : EReal) = (↑(C.toReal / (↑n : ℝ)) : EReal)
⊢ C / (↑n : EReal) = (↑(C.toReal / (↑n : ℝ)) : EReal)
have h₂ : (↑C.toReal : EReal) / (↑(↑n : ℝ) : EReal) = (↑(C.toReal / (↑n : ℝ)) : EReal)
Tactic: nth_rw 1 [← coe_toReal h' h, ← coe_coe_eq_natCast n, ← coe_div C.toReal n]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
n : ℕ
h₁ : (↑C.toReal : EReal) / (↑n : EReal) = (↑(C.toReal / (↑n : ℝ)) : EReal)
h₂ : (↑C.toReal : EReal) / (↑(↑n : ℝ) : EReal) = (↑(C.toReal / (↑n : ℝ)) : EReal)
⊢ C / (↑n : EReal) = (↑(C.toReal / (↑n : ℝ)) : EReal)
have h₃ : (↑(C.toReal / (↑n : ℝ)) : EReal) = (↑(C.toReal / (↑n : ℝ)) : EReal)
Tactic: nth_rw 1 [← coe_toReal h' h, ← coe_coe_eq_natCast n, ← coe_div C.toReal n]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
⊢ Tendsto (β := EReal) (fun (n : ℕ) ↦ C / (↑n : EReal)) atTop (𝓝 0)
have this : Eq (α := (n : ℕ) → EReal) (fun (n : ℕ) ↦ C / (↑n : EReal)) fun (n : ℕ) ↦ (↑(C.toReal / (↑n : ℝ)) : EReal)
Tactic: have : (fun n : ℕ ↦ C / n) = fun n : ℕ ↦ ((C.toReal / n : ℝ) : EReal) := by
    ext n
    nth_rw 1 [← coe_toReal h' h, ← coe_coe_eq_natCast n, ← coe_div C.toReal n]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
this : Eq (α := (n : ℕ) → EReal) (fun (n : ℕ) ↦ C / (↑n : EReal)) fun (n : ℕ) ↦ (↑(C.toReal / (↑n : ℝ)) : EReal)
⊢ Tendsto (β := EReal) (fun (n : ℕ) ↦ C / (↑n : EReal)) atTop (𝓝 0)
have rw : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C.toReal / (↑n : ℝ)) atTop (𝓝 0)
Tactic: rw [this, ← coe_zero, tendsto_coe]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
𝕜 : Type u_4
A : Type u_5
inst : Semifield 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : Semiring A
inst_5 : Algebra 𝕜 A
inst_6 : TopologicalSpace A
inst_7 : ContinuousSMul 𝕜 A
⊢ Tendsto.{0, u_5} (α := ℕ) (β := A)
    (comp.{1, u_4 + 1, u_5 + 1} (β := 𝕜) (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) fun (n : ℕ) ↦ (↑n : 𝕜)⁻¹) atTop (𝓝 0)
have h : Eq.{u_5 + 1} (α := A) (0 : A) ((algebraMap 𝕜 A : (a : 𝕜) → A) 0 : A)
Tactic: convert! (continuous_algebraMap 𝕜 A).continuousAt.tendsto.comp tendsto_inv_atTop_nhds_zero_nat
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
𝕜 : Type u_4
A : Type u_5
inst : Semifield 𝕜
inst_1 : CharZero 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : Semiring A
inst_5 : Algebra 𝕜 A
inst_6 : TopologicalSpace A
inst_7 : ContinuousSMul 𝕜 A
⊢ Eq.{u_5 + 1} (α := A) (0 : A) ((algebraMap 𝕜 A : (a : 𝕜) → A) 0 : A)
have h : Eq.{u_5 + 1} (α := A) 0 0
Tactic: rw [map_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
𝕜 : Type u_4
inst : DivisionSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : CharZero 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
x : 𝕜
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ (↑n : 𝕜) / ((↑n : 𝕜) + x)) atTop (𝓝 1)
have convert_2 : ℕ → 𝕜
Tactic: convert! Tendsto.congr' ((eventually_ne_atTop 0).mp (Eventually.of_forall fun n hn ↦ _)) _
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
𝕜 : Type u_4
inst : DivisionSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : CharZero 𝕜
inst_3 : ContinuousSMul ℚ≥0 𝕜
inst_4 : IsTopologicalSemiring 𝕜
inst_5 : ContinuousInv₀ 𝕜
x : 𝕜
convert_2 : ℕ → 𝕜
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ (↑n : 𝕜) / ((↑n : 𝕜) + x)) atTop (𝓝 1)
have convert_5 : ∀ (n : ℕ) (hn : n ≠ 0), 1 / (1 + x / (↑n : 𝕜)) = (↑n : 𝕜) / ((↑n : 𝕜) + x)
Tactic: convert! Tendsto.congr' ((eventually_ne_atTop 0).mp (Eventually.of_forall fun n hn ↦ _)) _