awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
k : ℕ
r : ℝ
hr : |r| < 1
h0 : ¬r = 0
⊢ 1 < |r|⁻¹

Tactic:
have hr' : 1 < |r|⁻¹ := (one_lt_inv₀ (abs_pos.2 h0)).2 hr
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
k : ℕ
r : ℝ
hr : |r| < 1
h0 : ¬r = 0
hr' : 1 < |r|⁻¹
neg : Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖HPow.hPow (α := ℝ) (↑x : ℝ) k * r ^ x‖) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * r ^ n) atTop (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]

Premises used: tendsto_zero_iff_norm_tendsto_zero
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
k : ℕ
r : ℝ
hr : |r| < 1
h0 : ¬r = 0
hr' : 1 < |r|⁻¹
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖HPow.hPow (α := ℝ) (↑x : ℝ) k * r ^ x‖) atTop (𝓝 0)

Tactic:
simpa [div_eq_mul_inv] using tendsto_pow_const_div_const_pow_of_one_lt k hr'

Premises used: div_eq_mul_inv, tendsto_pow_const_div_const_pow_of_one_lt
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
r : ℝ
k : ℕ
hk : k ≠ 0
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ r / HPow.hPow (α := ℝ) (↑n : ℝ) k) atTop (𝓝 0)

Tactic:
simpa using Filter.Tendsto.const_div_atTop (tendsto_natCast_atTop_atTop (R := ℝ).comp
    (tendsto_pow_atTop hk)) r

Premises used: tendsto_natCast_atTop_atTop, Filter.Tendsto.const_div_atTop, Filter.Tendsto.comp, Filter.tendsto_pow_atTop
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
k : ℕ
r : ℝ
hr : 0 ≤ r
h'r : r < 1
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * r ^ n) atTop (𝓝 0)

Tactic:
tendsto_pow_const_mul_const_pow_of_abs_lt_one k (abs_lt.2 ⟨neg_one_lt_zero.trans_le hr, h'r⟩)

Premises used: Iff.mpr, tendsto_pow_const_mul_const_pow_of_abs_lt_one, LT.lt.trans_le, And.intro, abs_lt, neg_one_lt_zero
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
r : ℝ
hr : |r| < 1
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑n : ℝ) * r ^ n) atTop (𝓝 0)

Tactic:
simpa only [pow_one] using tendsto_pow_const_mul_const_pow_of_abs_lt_one 1 hr

Premises used: tendsto_pow_const_mul_const_pow_of_abs_lt_one, pow_one, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
r : ℝ
hr : 0 ≤ r
h'r : r < 1
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑n : ℝ) * r ^ n) atTop (𝓝 0)

Tactic:
simpa only [pow_one] using tendsto_pow_const_mul_const_pow_of_lt_one 1 hr h'r

Premises used: pow_one, tendsto_pow_const_mul_const_pow_of_lt_one, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : SeminormedRing R
x : R
h : ‖x‖ < 1
apply : Tendsto (α := ℕ) (HPow.hPow ‖x‖) atTop (𝓝 0)
⊢ Tendsto.{0, u_2} (β := R) (fun (n : ℕ) ↦ x ^ n) atTop (𝓝 0)

Tactic:
apply squeeze_zero_norm' (eventually_norm_pow_le x)

Premises used: eventually_norm_pow_le, squeeze_zero_norm'
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : SeminormedRing R
x : R
h : ‖x‖ < 1
⊢ Tendsto (α := ℕ) (HPow.hPow ‖x‖) atTop (𝓝 0)

Tactic:
tendsto_pow_atTop_nhds_zero_of_lt_one (norm_nonneg _) h

Premises used: tendsto_pow_atTop_nhds_zero_of_lt_one, norm_nonneg
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : SeminormedRing R
x : R
h : ‖x‖ < 1
⊢ Tendsto (α := ℕ) (HPow.hPow ‖x‖) atTop (𝓝 0)

Tactic:
exact tendsto_pow_atTop_nhds_zero_of_lt_one (norm_nonneg _) h

Premises used: tendsto_pow_atTop_nhds_zero_of_lt_one, norm_nonneg
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
r : ℝ
h : |r| < 1
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)

Tactic:
tendsto_pow_atTop_nhds_zero_of_norm_lt_one h

Premises used: tendsto_pow_atTop_nhds_zero_of_norm_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : SeminormedRing R
inst_1 : NormMulClass R
x : R
⊢ Tendsto.{0, u_2} (β := R) (fun (n : ℕ) ↦ x ^ n) atTop (𝓝 0) ↔ ‖x‖ < 1

Tactic:
⟨?_, tendsto_pow_atTop_nhds_zero_of_norm_lt_one⟩

Premises used: Iff.intro, tendsto_pow_atTop_nhds_zero_of_norm_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : SeminormedRing R
inst_1 : NormMulClass R
x : R
refine : Tendsto.{0, u_2} (β := R) (fun (n : ℕ) ↦ x ^ n) atTop (𝓝 0) → ‖x‖ < 1
⊢ Tendsto.{0, u_2} (β := R) (fun (n : ℕ) ↦ x ^ n) atTop (𝓝 0) ↔ ‖x‖ < 1

Tactic:
refine ⟨?_, tendsto_pow_atTop_nhds_zero_of_norm_lt_one⟩
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : SeminormedRing R
inst_1 : NormMulClass R
x : R
rw : Tendsto (β := ℝ) (fun (x_1 : ℕ) ↦ ‖x ^ x_1‖) atTop (𝓝 0) → Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖x‖ ^ n) atTop (𝓝 0)
⊢ Tendsto.{0, u_2} (β := R) (fun (n : ℕ) ↦ x ^ n) atTop (𝓝 0) → ‖x‖ < 1

Tactic:
rw [← abs_of_nonneg (norm_nonneg _), ← tendsto_pow_atTop_nhds_zero_iff,
    tendsto_zero_iff_norm_tendsto_zero]

Premises used: tendsto_zero_iff_norm_tendsto_zero, abs_of_nonneg, tendsto_pow_atTop_nhds_zero_iff, norm_nonneg
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : SeminormedRing R
inst_1 : NormMulClass R
x : R
hl : EventuallyEq (β := ℝ) atTop (fun (x_1 : ℕ) ↦ ‖x ^ x_1‖) fun (n : ℕ) ↦ ‖x‖ ^ n
⊢ Tendsto (β := ℝ) (fun (x_1 : ℕ) ↦ ‖x ^ x_1‖) atTop (𝓝 0) → Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖x‖ ^ n) atTop (𝓝 0)

Tactic:
apply Tendsto.congr'

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : SeminormedRing R
inst_1 : NormMulClass R
x : R
h : ∀ (n : ℕ) (hn : 1 ≤ n), ‖x ^ n‖ = ‖x‖ ^ n
⊢ EventuallyEq (β := ℝ) atTop (fun (x_1 : ℕ) ↦ ‖x ^ x_1‖) fun (n : ℕ) ↦ ‖x‖ ^ n

Tactic:
filter_upwards [eventually_ge_atTop 1] with n hn

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : SeminormedRing R
inst_1 : NormMulClass R
x : R
n : ℕ
⊢ ‖HPow.hPow (β := ℕ) x 1‖ = HPow.hPow (β := ℕ) ‖x‖ 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : SeminormedRing R
inst_1 : NormMulClass R
x : R
n_1 n : ℕ
hn : 1 ≤ n
IH : ‖x ^ n‖ = ‖x‖ ^ n
⊢ ‖x ^ (n + 1)‖ = ‖x‖ ^ (n + 1)

Tactic:
simp [pow_succ, IH]

Premises used: pow_succ
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : SeminormedRing R
inst_1 : NormMulClass R
x : R
n : ℕ
hn : 1 ≤ n
h : ‖HPow.hPow (β := ℕ) x 1‖ = HPow.hPow (β := ℕ) ‖x‖ 1
h₁ : ∀ (n : ℕ) (hn : 1 ≤ n) (IH : ‖x ^ n‖ = ‖x‖ ^ n), ‖x ^ (n + 1)‖ = ‖x‖ ^ (n + 1)
⊢ ‖x ^ n‖ = ‖x‖ ^ n

Tactic:
induction n, hn using Nat.le_induction with
  | base => simp
  | succ n hn IH => simp [pow_succ, IH]

Premises used: pow_succ, Nat.succ
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
S : Type u_3
inst : Field R
inst_1 : Field S
inst_2 : LinearOrder S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : LT.lt.{u_3} (α := S) ((v : (a : R) → S) a : S) (1 : S)
simp_rw :
  Tendsto.{0, u_3} (β := S) (fun (n : ℕ) ↦ HDiv.hDiv (α := S) (β := S) (1 : S) ((v : (a : R) → S) (1 + a ^ n) : S))
    atTop (𝓝 1)
⊢ Tendsto.{0, u_3} (β := S) (fun (n : ℕ) ↦ (v : (a : R) → S) (1 / (1 + a ^ n))) atTop (𝓝 1)

Tactic:
simp_rw [map_div₀ v, v.map_one]

Premises used: map_div₀, AbsoluteValue.map_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
S : Type u_3
inst : Field R
inst_1 : Field S
inst_2 : LinearOrder S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : LT.lt.{u_3} (α := S) ((v : (a : R) → S) a : S) (1 : S)
apply : Tendsto.{0, u_3} (β := S) (fun (n : ℕ) ↦ (v : (a : R) → S) (1 + a ^ n)) atTop (𝓝 1)
⊢ Tendsto.{0, u_3} (β := S) (fun (n : ℕ) ↦ HDiv.hDiv (α := S) (β := S) (1 : S) ((v : (a : R) → S) (1 + a ^ n) : S))
    atTop (𝓝 1)

Tactic:
apply one_div_one (G := S) ▸ Tendsto.div tendsto_const_nhds _ one_ne_zero
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
S : Type u_3
inst : Field R
inst_1 : Field S
inst_2 : LinearOrder S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : LT.lt.{u_3} (α := S) ((v : (a : R) → S) a : S) (1 : S)
⊢ Tendsto (fun (x : ℕ) ↦ 1 + HPow.hPow (α := S) ((v : (a : R) → S) a : S) x) atTop (𝓝 (HAdd.hAdd (α := S) 1 0))

Tactic:
have h_add := (tendsto_pow_atTop_nhds_zero_of_lt_one (v.nonneg _) ha).const_add 1
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
S : Type u_3
inst : Field R
inst_1 : Field S
inst_2 : LinearOrder S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : LT.lt.{u_3} (α := S) ((v : (a : R) → S) a : S) (1 : S)
h_add : Tendsto (fun (x : ℕ) ↦ 1 + HPow.hPow (α := S) ((v : (a : R) → S) a : S) x) atTop (𝓝 (HAdd.hAdd (α := S) 1 0))
⊢ Tendsto (fun (x : ℕ) ↦ 1 - HPow.hPow (α := S) ((v : (a : R) → S) a : S) x) atTop (𝓝 (HSub.hSub (α := S) 1 0))

Tactic:
have h_sub := (tendsto_pow_atTop_nhds_zero_of_lt_one (v.nonneg _) ha).const_sub 1
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
S : Type u_3
inst : Field R
inst_1 : Field S
inst_2 : LinearOrder S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : LT.lt.{u_3} (α := S) ((v : (a : R) → S) a : S) (1 : S)
h_add : Tendsto (fun (x : ℕ) ↦ 1 + HPow.hPow (α := S) ((v : (a : R) → S) a : S) x) atTop (𝓝 (HAdd.hAdd (α := S) 1 0))
h_sub : Tendsto (fun (x : ℕ) ↦ 1 - HPow.hPow (α := S) ((v : (a : R) → S) a : S) x) atTop (𝓝 (HSub.hSub (α := S) 1 0))
⊢ Tendsto.{0, u_3} (β := S) (fun (x : ℕ) ↦ 1 - HPow.hPow (α := S) ((v : (a : R) → S) a : S) x) atTop (𝓝 1)

Tactic:
simpa using h_sub
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
S : Type u_3
inst : Field R
inst_1 : Field S
inst_2 : LinearOrder S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : LT.lt.{u_3} (α := S) ((v : (a : R) → S) a : S) (1 : S)
h_add : Tendsto (fun (x : ℕ) ↦ 1 + HPow.hPow (α := S) ((v : (a : R) → S) a : S) x) atTop (𝓝 (HAdd.hAdd (α := S) 1 0))
h_sub : Tendsto (fun (x : ℕ) ↦ 1 - HPow.hPow (α := S) ((v : (a : R) → S) a : S) x) atTop (𝓝 (HSub.hSub (α := S) 1 0))
⊢ Tendsto.{0, u_3} (β := S) (fun (x : ℕ) ↦ 1 + HPow.hPow (α := S) ((v : (a : R) → S) a : S) x) atTop (𝓝 1)

Tactic:
simpa using h_add
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
S : Type u_3
inst : Field R
inst_1 : Field S
inst_2 : LinearOrder S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : LT.lt.{u_3} (α := S) ((v : (a : R) → S) a : S) (1 : S)
h_add : Tendsto (fun (x : ℕ) ↦ 1 + HPow.hPow (α := S) ((v : (a : R) → S) a : S) x) atTop (𝓝 (HAdd.hAdd (α := S) 1 0))
h_sub : Tendsto (fun (x : ℕ) ↦ 1 - HPow.hPow (α := S) ((v : (a : R) → S) a : S) x) atTop (𝓝 (HSub.hSub (α := S) 1 0))
n : ℕ
⊢ 1 - HPow.hPow (α := S) ((v : (a : R) → S) a : S) n ≤
    HSub.hSub (α := S) (β := S) ((v : (a : R) → S) 1 : S) ((v : (a : R) → S) (a ^ n) : S)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
S : Type u_3
inst : Field R
inst_1 : Field S
inst_2 : LinearOrder S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : LT.lt.{u_3} (α := S) ((v : (a : R) → S) a : S) (1 : S)
h_add : Tendsto (fun (x : ℕ) ↦ 1 + HPow.hPow (α := S) ((v : (a : R) → S) a : S) x) atTop (𝓝 (HAdd.hAdd (α := S) 1 0))
h_sub : Tendsto (fun (x : ℕ) ↦ 1 - HPow.hPow (α := S) ((v : (a : R) → S) a : S) x) atTop (𝓝 (HSub.hSub (α := S) 1 0))
n : ℕ
⊢ HAdd.hAdd (α := S) (β := S) ((v : (a : R) → S) 1 : S) ((v : (a : R) → S) (a ^ n) : S) ≤
    1 + HPow.hPow (α := S) ((v : (a : R) → S) a : S) n

Tactic:
simp
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
S : Type u_3
inst : Field R
inst_1 : Field S
inst_2 : LinearOrder S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : LT.lt.{u_3} (α := S) ((v : (a : R) → S) a : S) (1 : S)
h_add : Tendsto (fun (x : ℕ) ↦ 1 + HPow.hPow (α := S) ((v : (a : R) → S) a : S) x) atTop (𝓝 (HAdd.hAdd (α := S) 1 0))
h_sub : Tendsto (fun (x : ℕ) ↦ 1 - HPow.hPow (α := S) ((v : (a : R) → S) a : S) x) atTop (𝓝 (HSub.hSub (α := S) 1 0))
⊢ Tendsto.{0, u_3} (β := S) (fun (n : ℕ) ↦ (v : (a : R) → S) (1 + a ^ n)) atTop (𝓝 1)

Tactic:
exact tendsto_of_tendsto_of_tendsto_of_le_of_le (by simpa using h_sub) (by simpa using h_add)
    (fun n ↦ le_trans (by simp) (v.le_add _ _))
    (fun n ↦ le_trans (v.add_le _ _) (by simp))

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le, AbsoluteValue.le_add, AbsoluteValue.add_le, le_trans
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
S : Type u_3
inst : Field R
inst_1 : Field S
inst_2 : LinearOrder S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : LT.lt.{u_3} (α := S) (1 : S) ((v : (a : R) → S) a : S)
simp_rw : Tendsto.{0, u_3} (β := S) (fun (n : ℕ) ↦ ((v : (a : R) → S) (a ^ n + 1))⁻¹) atTop (𝓝 0)
⊢ Tendsto.{0, u_3} (β := S) (fun (n : ℕ) ↦ (v : (a : R) → S) (1 / (1 + a ^ n))) atTop (𝓝 0)

Tactic:
simp_rw [div_eq_mul_inv, one_mul, map_inv₀, fun n ↦ add_comm 1 (a ^ n)]

Premises used: map_inv₀, div_eq_mul_inv, add_comm, HPow.hPow, OfNat.ofNat, one_mul
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
S : Type u_3
inst : Field R
inst_1 : Field S
inst_2 : LinearOrder S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : LT.lt.{u_3} (α := S) (1 : S) ((v : (a : R) → S) a : S)
⊢ Tendsto.{0, u_3} (β := S) (fun (n : ℕ) ↦ ((v : (a : R) → S) (a ^ n + 1))⁻¹) atTop (𝓝 0)

Tactic:
(tendsto_atTop_mono (fun n ↦ v.le_add _ _) ?_).inv_tendsto_atTop

Premises used: Filter.tendsto_atTop_mono, AbsoluteValue.le_add, Filter.Tendsto.inv_tendsto_atTop
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
S : Type u_3
inst : Field R
inst_1 : Field S
inst_2 : LinearOrder S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : LT.lt.{u_3} (α := S) (1 : S) ((v : (a : R) → S) a : S)
refine :
  Tendsto.{0, u_3} (β := S)
    (fun (n : ℕ) ↦ HSub.hSub (α := S) (β := S) ((v : (a : R) → S) (a ^ n) : S) ((v : (a : R) → S) 1 : S)) atTop atTop
⊢ Tendsto.{0, u_3} (β := S) (fun (n : ℕ) ↦ ((v : (a : R) → S) (a ^ n + 1))⁻¹) atTop (𝓝 0)

Tactic:
refine (tendsto_atTop_mono (fun n ↦ v.le_add _ _) ?_).inv_tendsto_atTop

Premises used: Filter.tendsto_atTop_mono, AbsoluteValue.le_add, Filter.Tendsto.inv_tendsto_atTop
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
S : Type u_3
inst : Field R
inst_1 : Field S
inst_2 : LinearOrder S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : LT.lt.{u_3} (α := S) (1 : S) ((v : (a : R) → S) a : S)
⊢ Tendsto.{0, u_3} (β := S)
    (fun (n : ℕ) ↦ HSub.hSub (α := S) (β := S) ((v : (a : R) → S) (a ^ n) : S) ((v : (a : R) → S) 1 : S)) atTop atTop

Tactic:
simpa using (tendsto_atTop_add_right_of_le _ _ (tendsto_pow_atTop_atTop_of_one_lt ha)
    (fun _ ↦ le_rfl)).congr fun n ↦ (sub_eq_add_neg (v a ^ n) 1).symm

Premises used: le_rfl, Filter.tendsto_atTop_add_right_of_le, sub_eq_add_neg, tendsto_pow_atTop_atTop_of_one_lt, HPow.hPow, Filter.Tendsto.congr, OfNat.ofNat, Eq.symm, DFunLike.coe
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
K : Type u_4
inst : NormedRing K
inst_1 : HasSummableGeomSeries K
x : K
h : ‖x‖ < 1
⊢ Summable.{u_4, 0} (α := K) fun (n : ℕ) ↦ x ^ n

Tactic:
HasSummableGeomSeries.summable_geometric_of_norm_lt_one x h

Premises used: HasSummableGeomSeries.summable_geometric_of_norm_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
R_1 : Type u_2
S : Type u_3
inst : Field R_1
inst_1 : Field S
inst_2 : LinearOrder S
v w : AbsoluteValue R_1 S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
R : Type u_4
inst_6 : NormedRing R
inst_7 : CompleteSpace R
summable_geometric_of_norm_lt_one : ∀ (ξ : R), ‖ξ‖ < 1 → Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ ξ ^ n
⊢ HasSummableGeomSeries R

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
R_1 : Type u_2
S : Type u_3
inst : Field R_1
inst_1 : Field S
inst_2 : LinearOrder S
v w : AbsoluteValue R_1 S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
R : Type u_4
inst_6 : NormedRing R
inst_7 : CompleteSpace R
x : R
hx : ‖x‖ < 1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖x‖ ^ n

Tactic:
have h1 : Summable fun n : ℕ ↦ ‖x‖ ^ n := summable_geometric_of_lt_one (norm_nonneg _) hx
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
R_1 : Type u_2
S : Type u_3
inst : Field R_1
inst_1 : Field S
inst_2 : LinearOrder S
v w : AbsoluteValue R_1 S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
R : Type u_4
inst_6 : NormedRing R
inst_7 : CompleteSpace R
x : R
hx : ‖x‖ < 1
h1 : Summable (α := ℝ) fun (n : ℕ) ↦ ‖x‖ ^ n
⊢ Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n

Tactic:
h1.of_norm_bounded_eventually_nat (eventually_norm_pow_le x)

Premises used: eventually_norm_pow_le, Summable.of_norm_bounded_eventually_nat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
R_1 : Type u_2
S : Type u_3
inst : Field R_1
inst_1 : Field S
inst_2 : LinearOrder S
v w : AbsoluteValue R_1 S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
R : Type u_4
inst_6 : NormedRing R
inst_7 : CompleteSpace R
x : R
hx : ‖x‖ < 1
h1 : Summable (α := ℝ) fun (n : ℕ) ↦ ‖x‖ ^ n
⊢ Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n

Tactic:
exact h1.of_norm_bounded_eventually_nat (eventually_norm_pow_le x)

Premises used: eventually_norm_pow_le, Summable.of_norm_bounded_eventually_nat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
pos :
  ∀ (hx : Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n),
    norm.{u_4} (E := R) (∑' (n : ℕ), x ^ n) ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
neg :
  ∀ (hx : ¬Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n),
    norm.{u_4} (E := R) (∑' (n : ℕ), x ^ n) ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
⊢ norm.{u_4} (E := R) (∑' (n : ℕ), x ^ n) ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹

Tactic:
by_cases hx : Summable (fun n ↦ x ^ n)

Premises used: HPow.hPow, Summable, SummationFilter.unconditional
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
pos : ‖HPow.hPow (β := ℕ) x 0 + ∑' (b : ℕ), x ^ (b + 1)‖ ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
⊢ norm.{u_4} (E := R) (∑' (n : ℕ), x ^ n) ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹

Tactic:
rw [hx.tsum_eq_zero_add]

Premises used: Summable.tsum_eq_zero_add
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
pos : ‖HAdd.hAdd (α := R) 1 (∑' (b : ℕ), x ^ (b + 1))‖ ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
⊢ ‖HPow.hPow (β := ℕ) x 0 + ∑' (b : ℕ), x ^ (b + 1)‖ ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹

Tactic:
simp only [_root_.pow_zero]

Premises used: pow_zero
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
⊢ ‖HAdd.hAdd (α := R) 1 (∑' (b : ℕ), x ^ (b + 1))‖ ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹

Tactic:
le_trans (norm_add_le _ _) ?_

Premises used: norm_add_le, le_trans
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
pos : norm.{u_4} (E := R) 1 + norm.{u_4} (E := R) (∑' (b : ℕ), x ^ (b + 1)) ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
⊢ ‖HAdd.hAdd (α := R) 1 (∑' (b : ℕ), x ^ (b + 1))‖ ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹

Tactic:
refine le_trans (norm_add_le _ _) ?_

Premises used: norm_add_le, le_trans
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
⊢ norm.{u_4} (E := R) (∑' (b : ℕ), (fun (n : ℕ) ↦ x ^ (n + 1)) b) ≤ (1 - ‖x‖)⁻¹ - 1

Tactic:
tsum_of_norm_bounded ?_ fun b ↦ norm_pow_le' _ (Nat.succ_pos b)

Premises used: Nat.succ_pos, norm_pow_le', tsum_of_norm_bounded
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
refine : HasSum (fun (b : ℕ) ↦ ‖x‖ ^ (b + 1)) ((1 - ‖x‖)⁻¹ - 1)
⊢ norm.{u_4} (E := R) (∑' (b : ℕ), (fun (n : ℕ) ↦ x ^ (n + 1)) b) ≤ (1 - ‖x‖)⁻¹ - 1

Tactic:
refine tsum_of_norm_bounded ?_ fun b ↦ norm_pow_le' _ (Nat.succ_pos b)

Premises used: tsum_of_norm_bounded
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
⊢ HasSum (fun (n : ℕ) ↦ ‖x‖ ^ (n + 1)) ((1 - ‖x‖)⁻¹ - ∑ i ∈ Finset.range 1, ‖x‖ ^ i)

Tactic:
(hasSum_nat_add_iff' 1).mpr (hasSum_geometric_of_lt_one (norm_nonneg x) h)

Premises used: Iff.mpr, hasSum_nat_add_iff', OfNat.ofNat, norm_nonneg, hasSum_geometric_of_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
h₁ : Eq (α := ℝ) 1 (∑ i ∈ Finset.range 1, ‖x‖ ^ i)
⊢ HasSum (fun (b : ℕ) ↦ ‖x‖ ^ (b + 1)) ((1 - ‖x‖)⁻¹ - 1)

Tactic:
convert! (hasSum_nat_add_iff' 1).mpr (hasSum_geometric_of_lt_one (norm_nonneg x) h)

Premises used: Iff.mpr, hasSum_nat_add_iff', OfNat.ofNat, norm_nonneg, hasSum_geometric_of_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
⊢ Eq (α := ℝ) 1 (∑ i ∈ Finset.range 1, ‖x‖ ^ i)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
⊢ norm.{u_4} (E := R) (∑' (b : ℕ), (fun (n : ℕ) ↦ x ^ (n + 1)) b) ≤ (1 - ‖x‖)⁻¹ - 1

Tactic:
have : ‖∑' b : ℕ, (fun n ↦ x ^ (n + 1)) b‖ ≤ (1 - ‖x‖)⁻¹ - 1 := by
      refine tsum_of_norm_bounded ?_ fun b ↦ norm_pow_le' _ (Nat.succ_pos b)
      convert! (hasSum_nat_add_iff' 1).mpr (hasSum_geometric_of_lt_one (norm_nonneg x) h)
      simp
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
this : norm.{u_4} (E := R) (∑' (b : ℕ), (fun (n : ℕ) ↦ x ^ (n + 1)) b) ≤ (1 - ‖x‖)⁻¹ - 1
linarith :
  norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹ < norm.{u_4} (E := R) 1 + norm.{u_4} (E := R) (∑' (b : ℕ), x ^ (b + 1)) →
    1 * norm.{u_4} (E := R) (∑' (b : ℕ), x ^ (b + 1)) - (1 * (1 - ‖x‖)⁻¹ - HMul.hMul (α := ℝ) 1 1) +
        (1 * norm.{u_4} (E := R) 1 - HMul.hMul (α := ℝ) 1 1 + 1 * (1 - ‖x‖)⁻¹ -
          (1 * norm.{u_4} (E := R) 1 + 1 * norm.{u_4} (E := R) (∑' (b : ℕ), x ^ (b + 1)))) =
      0
⊢ norm.{u_4} (E := R) 1 + norm.{u_4} (E := R) (∑' (b : ℕ), x ^ (b + 1)) ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
neg : 0 ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹
⊢ norm.{u_4} (E := R) (∑' (n : ℕ), x ^ n) ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹

Tactic:
simp only [tsum_eq_zero_of_not_summable hx, norm_zero]

Premises used: norm_zero, tsum_eq_zero_of_not_summable
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
h_1 : Nontrivial R
⊢ 1 ≤ norm.{u_4} (E := R) 1

Tactic:
have : 1 ≤ ‖(1 : R)‖ := one_le_norm_one R