awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
n : ℕ
⊢ 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}
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
n : ℕ
A : Summable (α := ℝ) fun (i : ℕ) ↦ if n ≤ i then HPow.hPow (α := ℝ) 2⁻¹ i else 0
⊢ 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
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
n : ℕ
A : Summable (α := ℝ) fun (i : ℕ) ↦ if n ≤ i then HPow.hPow (α := ℝ) 2⁻¹ i else 0
B : Eq (α := ℝ) (∑ i ∈ Finset.range n, if n ≤ i then HPow.hPow (α := ℝ) 2⁻¹ i else 0) 0
⊢ (∑' (i : ℕ), if n ≤ i then HPow.hPow (α := ℝ) 2⁻¹ i else 0) = 2 * HPow.hPow (α := ℝ) 2⁻¹ n

Tactic:
simp only [← Summable.sum_add_tsum_nat_add n A, B, if_true, zero_add, zero_le',
    le_add_iff_nonneg_left, pow_add, _root_.tsum_mul_right, tsum_geometric_inv_two]

Premises used: if_true, pow_add, zero_add, tsum_mul_right, tsum_geometric_inv_two, zero_le', Summable.sum_add_tsum_nat_add, le_add_iff_nonneg_left
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
a : ℝ
⊢ HasSum (fun (i : ℕ) ↦ a / 2 * (1 / 2) ^ i) (a / 2 * (1 - 1 / 2)⁻¹)

Tactic:
HasSum.mul_left (a / 2)
      (hasSum_geometric_of_lt_one (le_of_lt one_half_pos) one_half_lt_one)

Premises used: le_of_lt, one_half_lt_one, HDiv.hDiv, HasSum.mul_left, one_half_pos, OfNat.ofNat, hasSum_geometric_of_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
a : ℝ
h : Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ a / 2 / HPow.hPow (α := ℝ) 2 n) fun (i : ℕ) ↦ a / 2 * (1 / 2) ^ i
h₁ : a = a / 2 * (1 - 1 / 2)⁻¹
⊢ HasSum (fun (n : ℕ) ↦ a / 2 / HPow.hPow (α := ℝ) 2 n) a

Tactic:
convert!
    HasSum.mul_left (a / 2)
      (hasSum_geometric_of_lt_one (le_of_lt one_half_pos) one_half_lt_one) using 1

Premises used: le_of_lt, one_half_lt_one, HDiv.hDiv, HasSum.mul_left, one_half_pos, OfNat.ofNat, hasSum_geometric_of_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
a : ℝ
h : ∀ (n : ℕ), a / 2 / HPow.hPow (α := ℝ) 2 n = a / 2 * (1 / 2) ^ n
⊢ Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ a / 2 / HPow.hPow (α := ℝ) 2 n) fun (i : ℕ) ↦ a / 2 * (1 / 2) ^ i

Tactic:
funext n
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
a : ℝ
n : ℕ
h : a / 2 / HPow.hPow (α := ℝ) 2 n = a / 2 * (HPow.hPow (α := ℝ) 2 n)⁻¹
⊢ a / 2 / HPow.hPow (α := ℝ) 2 n = a / 2 * (1 / 2) ^ n

Tactic:
simp only [one_div, inv_pow]

Premises used: inv_pow, one_div
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
a : ℝ
n : ℕ
⊢ a / 2 / HPow.hPow (α := ℝ) 2 n = a / 2 * (HPow.hPow (α := ℝ) 2 n)⁻¹

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
a : ℝ
⊢ a = a / 2 * (1 - 1 / 2)⁻¹

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
a : ℝ
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ a / 2 / HPow.hPow (α := ℝ) 2 n

Tactic:
⟨a, hasSum_geometric_two' a⟩

Premises used: hasSum_geometric_two', Exists.intro, Summable
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
a : ℝ
⊢ ∑' (n : ℕ), a / 2 / HPow.hPow (α := ℝ) 2 n = a

Tactic:
(hasSum_geometric_two' a).tsum_eq

Premises used: hasSum_geometric_two', HasSum.tsum_eq
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0
hr : r < 1
apply : HasSum (fun (a : ℕ) ↦ (↑(r ^ a) : ℝ)) (↑(1 - r)⁻¹ : ℝ)
⊢ HasSum (fun (n : ℕ) ↦ r ^ n) (1 - r)⁻¹

Tactic:
apply NNReal.hasSum_coe.1

Premises used: Iff.mp, NNReal.hasSum_coe
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0
hr : r < 1
rw : HasSum (fun (a : ℕ) ↦ (↑r : ℝ) ^ a) ((↑1 : ℝ) - (↑r : ℝ))⁻¹
⊢ HasSum (fun (a : ℕ) ↦ (↑r : ℝ) ^ a) (↑(1 - r) : ℝ)⁻¹

Tactic:
rw [NNReal.coe_sub (le_of_lt hr)]

Premises used: le_of_lt, NNReal.coe_sub
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun (a : ℕ) ↦ (↑r : ℝ) ^ a) ((↑1 : ℝ) - (↑r : ℝ))⁻¹

Tactic:
hasSum_geometric_of_lt_one r.coe_nonneg hr

Premises used: NNReal.coe_nonneg, NNReal.toReal, hasSum_geometric_of_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun (a : ℕ) ↦ (↑r : ℝ) ^ a) ((↑1 : ℝ) - (↑r : ℝ))⁻¹

Tactic:
exact hasSum_geometric_of_lt_one r.coe_nonneg hr

Premises used: NNReal.coe_nonneg, hasSum_geometric_of_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0
hr : r < 1
⊢ Summable (α := ℝ≥0) fun (n : ℕ) ↦ r ^ n

Tactic:
⟨_, NNReal.hasSum_geometric hr⟩

Premises used: NNReal.hasSum_geometric, Exists.intro, Summable
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0
hr : r < 1
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹

Tactic:
(NNReal.hasSum_geometric hr).tsum_eq

Premises used: NNReal.hasSum_geometric, HasSum.tsum_eq
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
inl : ∀ (hr : r < 1), ∑' (n : ℕ), r ^ n = (1 - r)⁻¹
inr : ∀ (hr : 1 ≤ r), ∑' (n : ℕ), r ^ n = (1 - r)⁻¹
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹

Tactic:
rcases lt_or_ge r 1 with hr | hr

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
hr : r < 1
inl : ∀ (r : ℝ≥0) (hr' : (↑r : ℝ≥0∞) < 1) (hr : (↑r : ℝ≥0∞) < 1), ∑' (n : ℕ), (↑r : ℝ≥0∞) ^ n = (1 - (↑r : ℝ≥0∞))⁻¹
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹

Tactic:
rcases ENNReal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩

Premises used: ENNReal.lt_iff_exists_coe, Iff.mp, rfl
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0
hr' : (↑r : ℝ≥0∞) < 1
hr : (↑r : ℝ≥0∞) < 1
⊢ r < 1

Tactic:
norm_cast at *
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0
hr' : (↑r : ℝ≥0∞) < 1
hr : (↑r : ℝ≥0∞) < 1
hr'₁ : r < 1
⊢ r < 1

Tactic:
norm_cast at *
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0
hr' hr : r < 1
⊢ ∑' (a : ℕ), (↑(r ^ a) : ℝ≥0∞) = (↑(1 - r)⁻¹ : ℝ≥0∞)

Tactic:
ENNReal.tsum_coe_eq (NNReal.hasSum_geometric hr)

Premises used: NNReal.hasSum_geometric, ENNReal.tsum_coe_eq
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0
hr' hr : r < 1
h : (↑(1 - r) : ℝ≥0∞)⁻¹ = (↑(1 - r)⁻¹ : ℝ≥0∞)
⊢ ∑' (n : ℕ), (↑(r ^ n) : ℝ≥0∞) = (↑(1 - r) : ℝ≥0∞)⁻¹

Tactic:
convert! ENNReal.tsum_coe_eq (NNReal.hasSum_geometric hr)

Premises used: NNReal.hasSum_geometric, ENNReal.tsum_coe_eq
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0
hr' hr : r < 1
h : (↑(1 - r) : ℝ≥0∞)⁻¹ = (↑(1 - r) : ℝ≥0∞)⁻¹
h₁ : ((↑1 : ℝ≥0∞) - (↑r : ℝ≥0∞))⁻¹ = ((↑1 : ℝ≥0∞) - (↑r : ℝ≥0∞))⁻¹
h₂ h₃ : (1 - (↑r : ℝ≥0∞))⁻¹ = (1 - (↑r : ℝ≥0∞))⁻¹
⊢ (↑(1 - r) : ℝ≥0∞)⁻¹ = (↑(1 - r)⁻¹ : ℝ≥0∞)

Tactic:
rw [ENNReal.coe_inv <| ne_of_gt <| tsub_pos_iff_lt.2 hr, coe_sub, coe_one]

Premises used: Iff.mpr, ENNReal.coe_inv, tsub_pos_iff_lt, ENNReal.coe_one, ENNReal.coe_sub, Nat.ne_of_gt
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
hr : 1 ≤ r
inr : ∀ b < ∞, ∃ (i : ℕ), b < ∑ a ∈ Finset.range i, r ^ a
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹

Tactic:
rw [tsub_eq_zero_iff_le.mpr hr, ENNReal.inv_zero, ENNReal.tsum_eq_iSup_nat, iSup_eq_top]

Premises used: Iff.mpr, iSup_eq_top, ENNReal.inv_zero, tsub_eq_zero_iff_le, ENNReal.tsum_eq_iSup_nat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ∀ b < ∞, ∃ (i : ℕ), b < ∑ a ∈ Finset.range i, r ^ a

Tactic:
fun a ha ↦
      (ENNReal.exists_nat_gt (lt_top_iff_ne_top.1 ha)).imp fun n hn ↦ lt_of_lt_of_le hn ?_

Premises used: ENNReal.exists_nat_gt, Exists.imp, lt_top_iff_ne_top, Iff.mp, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
hr : 1 ≤ r
inr :
  ∀ (a : ℝ≥0∞) (ha : a < ∞) (n : ℕ) (hn : a < (↑n : ℝ≥0∞)), LE.le (α := ℝ≥0∞) (↑n : ℝ≥0∞) (∑ a ∈ Finset.range n, r ^ a)
⊢ ∀ b < ∞, ∃ (i : ℕ), b < ∑ a ∈ Finset.range i, 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 ?_

Premises used: ENNReal.exists_nat_gt, Exists.imp, lt_top_iff_ne_top, Iff.mp, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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∞)
rw₂ rw₃ : Eq (α := ℝ≥0∞) (↑n : ℝ≥0∞) (↑n : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (↑n : ℝ≥0∞) (∑ i ∈ Finset.range n, 1)

Tactic:
rw [sum_const, nsmul_one, card_range]

Premises used: Finset.card_range, nsmul_one, Finset.sum_const
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ∞
n : ℕ
hn : a < (↑n : ℝ≥0∞)
h : ∀ i ∈ Finset.range n, 1 ≤ r ^ i
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, 1) (∑ i ∈ Finset.range n, r ^ i)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ∞
n : ℕ
hn : a < (↑n : ℝ≥0∞)
i : ℕ
h : i ∈ Finset.range n
⊢ 1 ≤ r ^ i

Tactic:
apply one_le_pow₀ hr

Premises used: one_le_pow₀
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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)
i₁ : LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, 1) (∑ i ∈ Finset.range n, r ^ i)
⊢ LE.le (α := ℝ≥0∞) (↑n : ℝ≥0∞) (∑ a ∈ Finset.range n, r ^ a)

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

Premises used: Nat.cast, Finset.range
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
⊢ ∑' (n : ℕ), r ^ (n + 1) = r * (1 - r)⁻¹

Tactic:
simp only [_root_.pow_succ', ENNReal.tsum_mul_left, ENNReal.tsum_geometric]

Premises used: ENNReal.tsum_mul_left, ENNReal.tsum_geometric, pow_succ'
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
simp_rw : HMul.hMul (α := ℝ≥0∞) 2⁻¹ 2 = 1
⊢ Eq (α := ℝ≥0∞) (∑' (m : ℕ), HPow.hPow (α := ℝ≥0∞) 2 (HSub.hSub (α := ℤ) (-1) (↑m : ℤ))) 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]

Premises used: zpow_natCast, neg_sub_left, ENNReal.tsum_geometric_add_one, ENNReal.one_sub_inv_two, Nat.cast_add, inv_inv, ENNReal.zpow_neg, Nat.cast_one, ENNReal.inv_pow
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
⊢ HMul.hMul (α := ℝ≥0∞) 2⁻¹ 2 = 1

Tactic:
ENNReal.inv_mul_cancel (Ne.symm (NeZero.ne' 2)) (Ne.symm top_ne_ofNat)

Premises used: NeZero.ne', ENNReal.top_ne_ofNat, Ne.symm, ENNReal.inv_mul_cancel, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
⊢ HMul.hMul (α := ℝ≥0∞) 2⁻¹ 2 = 1

Tactic:
exact ENNReal.inv_mul_cancel (Ne.symm (NeZero.ne' 2)) (Ne.symm top_ne_ofNat)

Premises used: NeZero.ne', ENNReal.top_ne_ofNat, Ne.symm, ENNReal.inv_mul_cancel, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ι : Type u_4
inst : Encodable ι
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ι), HPow.hPow (α := ℝ≥0∞) 2⁻¹ (encode i)) 2

Tactic:
(ENNReal.tsum_comp_le_tsum_of_injective encode_injective _).trans_eq ENNReal.tsum_geometric_two

Premises used: LE.le.trans_eq, Encodable.encode_injective, ENNReal.tsum_geometric_two, ENNReal.tsum_comp_le_tsum_of_injective
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
⊢ LT.lt (α := ℝ≥0∞) (∑' (n : ℕ), r ^ n) ∞ ↔ r < 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
hr : r < 1
ι : Type u_4
inst : Encodable ι
⊢ LT.lt (α := ℝ≥0∞) (∑' (y : ℕ), r ^ y) ∞

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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

Tactic:
cauchySeq_of_edist_le_of_tsum_ne_top _ hu ?_

Premises used: cauchySeq_of_edist_le_of_tsum_ne_top
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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
refine : Ne (α := ℝ≥0∞) (∑' (n : ℕ), C * r ^ n) ∞
⊢ CauchySeq f

Tactic:
refine cauchySeq_of_edist_le_of_tsum_ne_top _ hu ?_

Premises used: cauchySeq_of_edist_le_of_tsum_ne_top
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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
rw : C * (1 - r)⁻¹ ≠ ∞
⊢ Ne (α := ℝ≥0∞) (∑' (n : ℕ), C * r ^ n) ∞

Tactic:
rw [ENNReal.tsum_mul_left, ENNReal.tsum_geometric]

Premises used: ENNReal.tsum_mul_left, ENNReal.tsum_geometric
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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
finiteness finiteness₁ finiteness₂ finiteness₃ : 1 - r ≠ 0 → C * (1 - r)⁻¹ ≠ ∞
⊢ C * (1 - r)⁻¹ ≠ ∞

Tactic:
finiteness [(tsub_pos_iff_lt.2 hr).ne']

Premises used: Iff.mpr, tsub_pos_iff_lt, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 ≤ ∑' (m : ℕ), C * r ^ (n + m)

Tactic:
edist_le_tsum_of_edist_le_of_tendsto _ hu ha _

Premises used: edist_le_tsum_of_edist_le_of_tendsto
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 : ℕ
h : C * r ^ n / (1 - r) = ∑' (m : ℕ), C * r ^ (n + m)
⊢ edist (f n) a ≤ C * r ^ n / (1 - r)

Tactic:
convert! edist_le_tsum_of_edist_le_of_tendsto _ hu ha _

Premises used: edist_le_tsum_of_edist_le_of_tendsto
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 : ℕ
⊢ C * r ^ n / (1 - r) = ∑' (m : ℕ), C * r ^ (n + m)

Tactic:
simp only [pow_add, ENNReal.tsum_mul_left, ENNReal.tsum_geometric, div_eq_mul_inv, mul_assoc]

Premises used: ENNReal.tsum_mul_left, mul_assoc, pow_add, div_eq_mul_inv, ENNReal.tsum_geometric
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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)
⊢ edist (f 0) a ≤ C / (1 - r)

Tactic:
simpa only [_root_.pow_zero, mul_one] using edist_le_of_edist_le_geometric_of_tendsto r C hu ha 0

Premises used: edist_le_of_edist_le_geometric_of_tendsto, pow_zero, mul_one, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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
⊢ ∀ (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

Premises used: div_eq_mul_inv, ENNReal.inv_pow
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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

Tactic:
cauchySeq_of_edist_le_geometric 2⁻¹ C ?_ hC hu

Premises used: cauchySeq_of_edist_le_geometric, Inv.inv, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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
refine : LT.lt (α := ℝ≥0∞) 2⁻¹ 1
⊢ CauchySeq f

Tactic:
refine cauchySeq_of_edist_le_geometric 2⁻¹ C ?_ hC hu

Premises used: cauchySeq_of_edist_le_geometric, Inv.inv, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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
⊢ LT.lt (α := ℝ≥0∞) 2⁻¹ 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 : ℕ
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
⊢ edist (f n) a ≤ 2 * C / HPow.hPow (α := ℝ≥0∞) 2 n

Tactic:
simp only [div_eq_mul_inv, ENNReal.inv_pow] at *

Premises used: div_eq_mul_inv, ENNReal.inv_pow
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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
rw : edist (f n) a ≤ C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n * 2
⊢ edist (f n) a ≤ 2 * C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n

Tactic:
rw [mul_assoc, mul_comm]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 / HSub.hSub (α := ℝ≥0∞) 1 2⁻¹

Tactic:
edist_le_of_edist_le_geometric_of_tendsto 2⁻¹ C hu ha n

Premises used: edist_le_of_edist_le_geometric_of_tendsto, Inv.inv, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 / HSub.hSub (α := ℝ≥0∞) 1 2⁻¹
⊢ edist (f n) a ≤ C * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n * 2

Tactic:
convert! edist_le_of_edist_le_geometric_of_tendsto 2⁻¹ C hu ha n using 1

Premises used: edist_le_of_edist_le_geometric_of_tendsto, Inv.inv, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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⁻¹⁻¹
h₂ 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⁻¹

Tactic:
rw [ENNReal.one_sub_inv_two, div_eq_mul_inv, inv_inv]

Premises used: div_eq_mul_inv, ENNReal.one_sub_inv_two, inv_inv
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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)
⊢ edist (f 0) a ≤ 2 * C

Tactic:
simpa only [_root_.pow_zero, div_eq_mul_inv, inv_one, mul_one] using
    edist_le_of_edist_le_geometric_two_of_tendsto C hu ha 0

Premises used: inv_one, edist_le_of_edist_le_geometric_two_of_tendsto, div_eq_mul_inv, pow_zero, mul_one, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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))
inr : 0 < C → ∀ (r₀ : 0 ≤ r), HasSum (fun (n : ℕ) ↦ C * r ^ n) (C / (1 - 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₀⟩)

Premises used: dist_nonneg, LE.le.trans, sign_cases_of_C_mul_pow_nonneg, rfl
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_1
inst : PseudoMetricSpace α
r : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ 0 * r ^ n
⊢ HasSum (fun (n : ℕ) ↦ 0 * r ^ n) (0 / (1 - r))

Tactic:
simp [hasSum_zero]

Premises used: hasSum_zero
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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))

Tactic:
HasSum.mul_left C ?_

Premises used: HasSum.mul_left, DivInvMonoid.div'
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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
inr : HasSum (HPow.hPow r) (1 - r)⁻¹
⊢ HasSum (fun (n : ℕ) ↦ C * r ^ n) (C / (1 - r))

Tactic:
refine HasSum.mul_left C ?_

Premises used: HasSum.mul_left
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 (HPow.hPow r) (1 - r)⁻¹

Tactic:
simpa using hasSum_geometric_of_lt_one r₀ hr

Premises used: hasSum_geometric_of_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_1
inst : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ CauchySeq f

Tactic:
cauchySeq_of_dist_le_of_summable _ hu ⟨_, aux_hasSum_of_le_geometric hr hu⟩

Premises used: aux_hasSum_of_le_geometric, cauchySeq_of_dist_le_of_summable, Exists.intro
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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)
⊢ dist (f 0) a ≤ C / (1 - r)

Tactic:
(aux_hasSum_of_le_geometric hr hu).tsum_eq ▸
    dist_le_tsum_of_dist_le_of_tendsto₀ _ hu ⟨_, aux_hasSum_of_le_geometric hr hu⟩ ha

Premises used: aux_hasSum_of_le_geometric, Eq.rec, dist_le_tsum_of_dist_le_of_tendsto₀, HasSum.tsum_eq, Exists.intro
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 : ℕ
⊢ HasSum (fun (n : ℕ) ↦ C * r ^ n) (C / (1 - r))

Tactic:
have := aux_hasSum_of_le_geometric hr hu
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 ≤ ∑' (m : ℕ), C * r ^ (n + m)

Tactic:
dist_le_tsum_of_dist_le_of_tendsto _ hu ⟨_, this⟩ ha n

Premises used: dist_le_tsum_of_dist_le_of_tendsto, Exists.intro
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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))
h : C * r ^ n / (1 - r) = ∑' (m : ℕ), C * r ^ (n + m)
⊢ dist (f n) a ≤ C * r ^ n / (1 - r)

Tactic:
convert! dist_le_tsum_of_dist_le_of_tendsto _ hu ⟨_, this⟩ ha n

Premises used: dist_le_tsum_of_dist_le_of_tendsto, Exists.intro
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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))
h : C / (1 - r) * r ^ n = ∑' (m : ℕ), r ^ n * (C * r ^ m)
⊢ C * r ^ n / (1 - r) = ∑' (m : ℕ), C * r ^ (n + m)

Tactic:
simp only [pow_add, mul_left_comm C, mul_div_right_comm]

Premises used: pow_add, mul_left_comm, mul_div_right_comm
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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))
h : r ^ n * (C / (1 - r)) = ∑' (m : ℕ), r ^ n * (C * r ^ m)
⊢ C / (1 - r) * r ^ n = ∑' (m : ℕ), r ^ n * (C * r ^ m)

Tactic:
rw [mul_comm]

Premises used: mul_comm