awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
r : 𝕜
h : Tendsto.{0, u_4} (α := ℕ) (β := 𝕜) (abs ∘ fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
apply : Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ |r| ^ n) atTop atTop
apply₁ : Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ |r| ^ n) atTop (𝓝 0)
⊢ False

Tactic:
apply @not_tendsto_nhds_of_tendsto_atTop 𝕜 ℕ _ _ _ _ atTop _ (fun n ↦ |r| ^ n) _ 0 _

Premises used: not_tendsto_nhds_of_tendsto_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
r : 𝕜
h : Tendsto.{0, u_4} (α := ℕ) (β := 𝕜) (abs ∘ fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ |r| ^ n) atTop atTop

Tactic:
(pow_right_strictMono₀ <| lt_of_le_of_ne (le_of_not_gt hr_le)
          hr).monotone.tendsto_atTop_atTop (fun b ↦ ?_)

Premises used: StrictMono.monotone, le_of_not_gt, Monotone.tendsto_atTop_atTop, pow_right_strictMono₀, lt_of_le_of_ne
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
r : 𝕜
h : Tendsto.{0, u_4} (α := ℕ) (β := 𝕜) (abs ∘ fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
refine : ∀ (b : 𝕜), ∃ (a : ℕ), b ≤ |r| ^ a
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ |r| ^ n) atTop atTop

Tactic:
refine (pow_right_strictMono₀ <| lt_of_le_of_ne (le_of_not_gt hr_le)
          hr).monotone.tendsto_atTop_atTop (fun b ↦ ?_)

Premises used: StrictMono.monotone, le_of_not_gt, Monotone.tendsto_atTop_atTop, pow_right_strictMono₀, lt_of_le_of_ne
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
r : 𝕜
h : Tendsto.{0, u_4} (α := ℕ) (β := 𝕜) (abs ∘ fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
b : 𝕜
obtain : ∀ (n : ℕ) (hn : b < |r| ^ n), ∃ (a : ℕ), b ≤ |r| ^ a
⊢ ∃ (a : ℕ), b ≤ |r| ^ a

Tactic:
obtain ⟨n, hn⟩ := (pow_unbounded_of_one_lt b (lt_of_le_of_ne (le_of_not_gt hr_le) hr))

Premises used: le_of_not_gt, pow_unbounded_of_one_lt, lt_of_le_of_ne
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
r : 𝕜
h : Tendsto.{0, u_4} (α := ℕ) (β := 𝕜) (abs ∘ fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
b : 𝕜
n : ℕ
hn : b < |r| ^ n
⊢ ∃ (a : ℕ), b ≤ |r| ^ a

Tactic:
⟨n, le_of_lt hn⟩

Premises used: le_of_lt, Exists.intro
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
r : 𝕜
h : Tendsto.{0, u_4} (α := ℕ) (β := 𝕜) (abs ∘ fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
b : 𝕜
n : ℕ
hn : b < |r| ^ n
⊢ ∃ (a : ℕ), b ≤ |r| ^ a

Tactic:
exact ⟨n, le_of_lt hn⟩
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
r : 𝕜
h : Tendsto.{0, u_4} (α := ℕ) (β := 𝕜) (abs ∘ fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ |r| ^ n) atTop (𝓝 0)

Tactic:
simpa only [← abs_pow]

Premises used: abs_pow
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
r : 𝕜
h : |r| < 1
⊢ Tendsto.{0, u_4} (α := ℕ) (β := 𝕜) (abs ∘ fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)

Tactic:
simpa only [← abs_pow] using (tendsto_pow_atTop_nhds_zero_of_lt_one (abs_nonneg r)) h

Premises used: tendsto_pow_atTop_nhds_zero_of_lt_one, abs_nonneg, abs_pow
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
𝕜 : Type u_4
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : ExistsAddOfLE 𝕜
inst_4 : Archimedean 𝕜
inst_5 : TopologicalSpace 𝕜
inst_6 : OrderTopology 𝕜
r : 𝕜
h₁ : 0 < r
h₂ : r < 1
⊢ Tendsto.{0, u_4} (β := 𝕜) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝[>] 0)

Tactic:
tendsto_inf.2
    ⟨tendsto_pow_atTop_nhds_zero_of_lt_one h₁.le h₂,
      tendsto_principal.2 <| Eventually.of_forall fun _ ↦ pow_pos h₁ _⟩

Premises used: Iff.mpr, pow_pos, Filter.tendsto_inf, nhdsWithin, LT.lt.le, Filter.Eventually.of_forall, Filter.tendsto_principal, And.intro, tendsto_pow_atTop_nhds_zero_of_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_4
inst : PseudoMetricSpace α
r : ℝ
h₀ : 0 < r
h₁ : r < 1
⊢ (uniformity α).HasBasis (fun (x : ℕ) ↦ True) fun (k : ℕ) ↦ {p : α × α | dist p.1 p.2 < r ^ k}

Tactic:
Metric.mk_uniformity_basis (fun _ _ ↦ pow_pos h₀ _) fun _ ε0 ↦
    (exists_pow_lt_of_lt_one ε0 h₁).imp fun _ hk ↦ ⟨trivial, hk.le⟩

Premises used: pow_pos, trivial, exists_pow_lt_of_lt_one, Exists.imp, And.intro, Metric.mk_uniformity_basis
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, c * u k < u (k + 1)
apply : HPow.hPow (β := ℕ) c 0 * u 0 ≤ u 0
apply₁ : ∀ k < n, c ^ (k + 1) * u 0 ≤ c * (c ^ k * u 0)
⊢ c ^ n * u 0 < u n

Tactic:
apply (monotone_mul_left_of_nonneg hc).seq_pos_lt_seq_of_le_of_lt hn _ _ h

Premises used: Monotone.seq_pos_lt_seq_of_le_of_lt, monotone_mul_left_of_nonneg
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, c * u k < u (k + 1)
⊢ HPow.hPow (β := ℕ) c 0 * u 0 ≤ u 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, c * u k < u (k + 1)
⊢ ∀ k < n, c ^ (k + 1) * u 0 ≤ c * (c ^ k * u 0)

Tactic:
simp [_root_.pow_succ', mul_assoc]

Premises used: mul_assoc, pow_succ'
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, c * u k ≤ u (k + 1)
apply : HPow.hPow (β := ℕ) c 0 * u 0 ≤ u 0
apply₁ : ∀ k < n, c ^ (k + 1) * u 0 ≤ c * (c ^ k * u 0)
⊢ c ^ n * u 0 ≤ u n

Tactic:
apply (monotone_mul_left_of_nonneg hc).seq_le_seq n _ _ h

Premises used: Monotone.seq_le_seq, monotone_mul_left_of_nonneg
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, c * u k ≤ u (k + 1)
⊢ HPow.hPow (β := ℕ) c 0 * u 0 ≤ u 0

Tactic:
simp [_root_.pow_succ', mul_assoc]

Premises used: mul_assoc, pow_succ'
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, c * u k ≤ u (k + 1)
⊢ ∀ k < n, c ^ (k + 1) * u 0 ≤ c * (c ^ k * u 0)

Tactic:
simp [_root_.pow_succ', mul_assoc]

Premises used: mul_assoc, pow_succ'
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, u (k + 1) < c * u k
apply : u 0 ≤ HPow.hPow (β := ℕ) c 0 * u 0
apply₁ : ∀ k < n, c * (c ^ k * u 0) ≤ c ^ (k + 1) * u 0
⊢ u n < c ^ n * u 0

Tactic:
apply (monotone_mul_left_of_nonneg hc).seq_pos_lt_seq_of_lt_of_le hn _ h _

Premises used: monotone_mul_left_of_nonneg, Monotone.seq_pos_lt_seq_of_lt_of_le
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, u (k + 1) < c * u k
⊢ u 0 ≤ HPow.hPow (β := ℕ) c 0 * u 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, u (k + 1) < c * u k
⊢ ∀ k < n, c * (c ^ k * u 0) ≤ c ^ (k + 1) * u 0

Tactic:
simp [_root_.pow_succ', mul_assoc]

Premises used: mul_assoc, pow_succ'
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, u (k + 1) ≤ c * u k
apply : u 0 ≤ HPow.hPow (β := ℕ) c 0 * u 0
apply₁ : ∀ k < n, c * (c ^ k * u 0) ≤ c ^ (k + 1) * u 0
⊢ u n ≤ c ^ n * u 0

Tactic:
apply (monotone_mul_left_of_nonneg hc).seq_le_seq n _ h _

Premises used: Monotone.seq_le_seq, monotone_mul_left_of_nonneg
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, u (k + 1) ≤ c * u k
⊢ u 0 ≤ HPow.hPow (β := ℕ) c 0 * u 0

Tactic:
simp [_root_.pow_succ', mul_assoc]

Premises used: mul_assoc, pow_succ'
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, u (k + 1) ≤ c * u k
⊢ ∀ k < n, c * (c ^ k * u 0) ≤ c ^ (k + 1) * u 0

Tactic:
simp [_root_.pow_succ', mul_assoc]

Premises used: mul_assoc, pow_succ'
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
v : ℕ → ℝ
c : ℝ
h₀ : 0 < v 0
hc : 1 < c
hu : ∀ (n : ℕ), c * v n ≤ v (n + 1)
⊢ Tendsto v atTop atTop

Tactic:
(tendsto_atTop_mono fun n ↦ geom_le (zero_le_one.trans hc.le) n fun k _ ↦ hu k) <|
    (tendsto_pow_atTop_atTop_of_one_lt hc).atTop_mul_const h₀

Premises used: geom_le, Filter.Tendsto.atTop_mul_const, Filter.tendsto_atTop_mono, LT.lt.le, zero_le_one, tendsto_pow_atTop_atTop_of_one_lt, LE.le.trans
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0
hr : r < 1
⊢ Tendsto (fun (a : ℕ) ↦ (↑(r ^ a) : ℝ)) atTop (𝓝 (↑0 : ℝ))

Tactic:
simp only [NNReal.coe_pow, NNReal.coe_zero,
      _root_.tendsto_pow_atTop_nhds_zero_of_lt_one r.coe_nonneg hr]

Premises used: NNReal.coe_zero, NNReal.coe_pow, NNReal.coe_nonneg, tendsto_pow_atTop_nhds_zero_of_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0
h : Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)
⊢ r < 1

Tactic:
simpa [coe_pow, coe_zero, abs_eq, coe_lt_one, val_eq_coe] using
    tendsto_pow_atTop_nhds_zero_iff.mp <| tendsto_coe.mpr h

Premises used: Iff.mpr, NNReal.coe_zero, NNReal.val_eq_coe, NNReal.coe_lt_one, NNReal.abs_eq, NNReal.coe_pow, Iff.mp, NNReal.tendsto_coe, tendsto_pow_atTop_nhds_zero_iff
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
hr : r < 1
rcases : ∀ (r : ℝ≥0) (hr' hr : (↑r : ℝ≥0∞) < 1), Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑r : ℝ≥0∞) ^ n) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)

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' hr : (↑r : ℝ≥0∞) < 1
norm_cast : ∀ (hr' hr : r < 1), Tendsto (α := ℕ) (HPow.hPow r) atTop (𝓝 0)
⊢ Tendsto (fun (n : ℕ) ↦ (↑r : ℝ≥0∞) ^ n) atTop (𝓝 (↑0 : ℝ≥0∞))

Tactic:
norm_cast at *
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0
hr' hr : r < 1
⊢ Tendsto (α := ℕ) (HPow.hPow r) atTop (𝓝 0)

Tactic:
apply NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one hr

Premises used: NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0) ↔ r < 1

Tactic:
⟨fun h ↦ ?_, tendsto_pow_atTop_nhds_zero_of_lt_one⟩

Premises used: ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one, Iff.intro
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
refine : ∀ (h : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)), r < 1
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0) ↔ r < 1

Tactic:
refine ⟨fun h ↦ ?_, tendsto_pow_atTop_nhds_zero_of_lt_one⟩
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
h : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)
lift : r ≠ ∞
lift₁ : ∀ (r : ℝ≥0) (h : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑r : ℝ≥0∞) ^ n) atTop (𝓝 0)), (↑r : ℝ≥0∞) < 1
⊢ r < 1

Tactic:
lift r to NNReal

Premises used: NNReal
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
h : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)
⊢ r ≠ ∞

Tactic:
fun hr ↦ top_ne_zero (tendsto_nhds_unique (EventuallyEq.tendsto ?_) (hr ▸ h))

Premises used: Filter.EventuallyEq.tendsto, ENNReal.top_ne_zero, Not, tendsto_nhds_unique
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
h : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)
refine : ∀ (hr : r = ∞), EventuallyEq (β := ℝ≥0∞) atTop (fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) ∞ n) fun (x : ℕ) ↦ ∞
⊢ r ≠ ∞

Tactic:
refine fun hr ↦ top_ne_zero (tendsto_nhds_unique (EventuallyEq.tendsto ?_) (hr ▸ h))

Premises used: Filter.EventuallyEq.tendsto, ENNReal.top_ne_zero, tendsto_nhds_unique
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
h : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)
hr : r = ∞
⊢ EventuallyEq (β := ℝ≥0∞) atTop (fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) ∞ n) fun (x : ℕ) ↦ ∞

Tactic:
eventually_atTop.mpr ⟨1, fun _ hn ↦ pow_eq_top_iff.mpr ⟨rfl, Nat.pos_iff_ne_zero.mp hn⟩⟩

Premises used: Iff.mpr, Nat.pos_iff_ne_zero, Filter.EventuallyEq, And.intro, Exists.intro, Iff.mp, Filter.eventually_atTop, OfNat.ofNat, ENNReal.pow_eq_top_iff, rfl
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
h : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 0)
hr : r = ∞
⊢ EventuallyEq (β := ℝ≥0∞) atTop (fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) ∞ n) fun (x : ℕ) ↦ ∞

Tactic:
exact eventually_atTop.mpr ⟨1, fun _ hn ↦ pow_eq_top_iff.mpr ⟨rfl, Nat.pos_iff_ne_zero.mp hn⟩⟩

Premises used: Iff.mpr, Nat.pos_iff_ne_zero, And.intro, Exists.intro, Iff.mp, Filter.eventually_atTop, OfNat.ofNat, ENNReal.pow_eq_top_iff, rfl
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0
h : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑r : ℝ≥0∞) ^ n) atTop (𝓝 0)
⊢ Tendsto (fun (n : ℕ) ↦ (↑r : ℝ≥0∞) ^ n) atTop (𝓝 (↑0 : ℝ≥0∞))

Tactic:
rw [← coe_zero] at h

Premises used: ENNReal.coe_zero
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0
h : Tendsto (fun (n : ℕ) ↦ (↑r : ℝ≥0∞) ^ n) atTop (𝓝 (↑0 : ℝ≥0∞))
norm_cast : ∀ (h : Tendsto (α := ℕ) (HPow.hPow r) atTop (𝓝 0)), r < 1
⊢ (↑r : ℝ≥0∞) < 1

Tactic:
norm_cast at h ⊢
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0
h : Tendsto (α := ℕ) (HPow.hPow r) atTop (𝓝 0)
⊢ r < 1

Tactic:
NNReal.tendsto_pow_atTop_nhds_zero_iff.mp h

Premises used: Iff.mp, NNReal.tendsto_pow_atTop_nhds_zero_iff
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0
h : Tendsto (α := ℕ) (HPow.hPow r) atTop (𝓝 0)
⊢ r < 1

Tactic:
exact NNReal.tendsto_pow_atTop_nhds_zero_iff.mp h

Premises used: Iff.mp, NNReal.tendsto_pow_atTop_nhds_zero_iff
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 ∞) ↔ 1 < r

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
refine_1 : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 ∞) → 1 < r
refine_2 : 1 < r → Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 ∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 ∞) ↔ 1 < r

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
refine_1 : r ≤ 1 → ¬Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 ∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 ∞) → 1 < r

Tactic:
contrapose!
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
r_le_one : r ≤ 1
h_tends : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 ∞)
⊢ Membership.mem (γ := Filter ℝ≥0∞) (Filter.map (fun (n : ℕ) ↦ r ^ n) atTop) (Set.Ioi 1)

Tactic:
specialize h_tends (Ioi_mem_nhds one_lt_top)

Premises used: Ioi_mem_nhds, ENNReal.one_lt_top
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
r_le_one : r ≤ 1
h_tends : Membership.mem (γ := Filter ℝ≥0∞) (Filter.map (fun (n : ℕ) ↦ r ^ n) atTop) (Set.Ioi 1)
⊢ ∃ (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

Premises used: ge_iff_le, Filter.mem_atTop_sets, Set.mem_Ioi, Filter.mem_map, Set.mem_preimage
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
r_le_one : r ≤ 1
h_tends : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → 1 < r ^ b
refine_1 : ∀ (n : ℕ) (hn : ∀ (b : ℕ), n ≤ b → 1 < r ^ b), False
⊢ False

Tactic:
obtain ⟨n, hn⟩ := h_tends
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
r_le_one : r ≤ 1
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 1 < r ^ b
⊢ False

Tactic:
lt_irrefl _ <| lt_of_lt_of_le (hn n le_rfl) <| pow_le_one₀ zero_le r_le_one

Premises used: zero_le, lt_irrefl, le_rfl, lt_of_lt_of_le, pow_le_one₀
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
r_le_one : r ≤ 1
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 1 < r ^ b
⊢ False

Tactic:
exact lt_irrefl _ <| lt_of_lt_of_le (hn n le_rfl) <| pow_le_one₀ zero_le r_le_one

Premises used: zero_le, lt_irrefl, le_rfl, lt_of_lt_of_le, pow_le_one₀
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
r_gt_one : 1 < r
⊢ ∀ (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
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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⁻¹)
⊢ ∀ (h : r⁻¹ < 1), Tendsto (β := ℝ≥0∞) (fun (x : ℕ) ↦ (r⁻¹ ^ x)⁻¹) atTop (𝓝 ∞)

Tactic:
simp only [ENNReal.tendsto_pow_atTop_nhds_zero_iff, inv_zero] at obs

Premises used: ENNReal.tendsto_pow_atTop_nhds_zero_iff, ENNReal.inv_zero
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ≥0∞
r_gt_one : 1 < r
obs : ∀ (h : r⁻¹ < 1), Tendsto (β := ℝ≥0∞) (fun (x : ℕ) ↦ (r⁻¹ ^ x)⁻¹) atTop (𝓝 ∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ r ^ n) atTop (𝓝 ∞)

Tactic:
simpa [← ENNReal.inv_pow] using obs <| ENNReal.inv_lt_one.mpr r_gt_one

Premises used: Iff.mpr, ENNReal.inv_lt_one, ENNReal.inv_pow
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
x r : ℝ≥0∞
ε : ℝ≥0
hr : r < 1
h : ∀ (n : ℕ), x ≤ (↑ε : ℝ≥0∞) * r ^ n
rw : x ≤ 0
⊢ x = 0

Tactic:
rw [← nonpos_iff_eq_zero]

Premises used: nonpos_iff_eq_zero
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
x r : ℝ≥0∞
ε : ℝ≥0
hr : r < 1
h : ∀ (n : ℕ), x ≤ (↑ε : ℝ≥0∞) * r ^ n
⊢ x ≤ 0

Tactic:
ge_of_tendsto' (f := fun (n : ℕ) ↦ ε * r ^ n) (x := atTop) ?_ h

Premises used: ge_of_tendsto'
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
x r : ℝ≥0∞
ε : ℝ≥0
hr : r < 1
h : ∀ (n : ℕ), x ≤ (↑ε : ℝ≥0∞) * r ^ n
refine : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑ε : ℝ≥0∞) * r ^ n) atTop (𝓝 0)
⊢ x ≤ 0

Tactic:
refine ge_of_tendsto' (f := fun (n : ℕ) ↦ ε * r ^ n) (x := atTop) ?_ h

Premises used: ge_of_tendsto'
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
x r : ℝ≥0∞
ε : ℝ≥0
hr : r < 1
h : ∀ (n : ℕ), x ≤ (↑ε : ℝ≥0∞) * r ^ n
rw : Tendsto (fun (n : ℕ) ↦ (↑ε : ℝ≥0∞) * r ^ n) atTop (𝓝 ((↑ε : ℝ≥0∞) * 0))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑ε : ℝ≥0∞) * r ^ n) atTop (𝓝 0)

Tactic:
rw [← mul_zero (M₀ := ℝ≥0∞) (a := ε)]

Premises used: ENNReal.ofNNReal, MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
x r : ℝ≥0∞
ε : ℝ≥0
hr : r < 1
h : ∀ (n : ℕ), x ≤ (↑ε : ℝ≥0∞) * r ^ n
⊢ Tendsto (fun (n : ℕ) ↦ (↑ε : ℝ≥0∞) * r ^ n) atTop (𝓝 ((↑ε : ℝ≥0∞) * 0))

Tactic:
Tendsto.const_mul (tendsto_pow_atTop_nhds_zero_of_lt_one hr) (Or.inr coe_ne_top)

Premises used: ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one, ENNReal.Tendsto.const_mul, Or.inr, ENNReal.coe_ne_top
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
x r : ℝ≥0∞
ε : ℝ≥0
hr : r < 1
h : ∀ (n : ℕ), x ≤ (↑ε : ℝ≥0∞) * r ^ n
⊢ Tendsto (fun (n : ℕ) ↦ (↑ε : ℝ≥0∞) * r ^ n) atTop (𝓝 ((↑ε : ℝ≥0∞) * 0))

Tactic:
exact Tendsto.const_mul (tendsto_pow_atTop_nhds_zero_of_lt_one hr) (Or.inr coe_ne_top)

Premises used: ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one, ENNReal.Tendsto.const_mul, Or.inr, ENNReal.coe_ne_top
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ
h₁ : 0 ≤ r
h₂ : r < 1
this_1 : r ≠ 1
this : Tendsto (fun (n : ℕ) ↦ (r ^ n - 1) * (r - 1)⁻¹) atTop (𝓝 (HSub.hSub (α := ℝ) 0 1 * (r - 1)⁻¹))
⊢ Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, r ^ i) atTop (𝓝 (1 - r)⁻¹)

Tactic:
simp_all [neg_inv, geom_sum_eq, div_eq_mul_inv]

Premises used: geom_sum_eq, div_eq_mul_inv, neg_inv
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ
h₁ : 0 ≤ r
h₂ : r < 1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ r ^ n

Tactic:
⟨_, hasSum_geometric_of_lt_one h₁ h₂⟩

Premises used: Exists.intro, Summable, hasSum_geometric_of_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
r : ℝ
h₁ : 0 ≤ r
h₂ : r < 1
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹

Tactic:
(hasSum_geometric_of_lt_one h₁ h₂).tsum_eq

Premises used: HasSum.tsum_eq, hasSum_geometric_of_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
⊢ HasSum (fun (n : ℕ) ↦ (1 / 2) ^ n) (1 - 1 / 2)⁻¹

Tactic:
hasSum_geometric_of_lt_one _ _

Premises used: hasSum_geometric_of_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
h : 2 = (1 - 1 / 2)⁻¹
convert_2 : 0 ≤ 1 / 2
convert_3 : 1 / 2 < 1
⊢ HasSum (α := ℝ) (fun (n : ℕ) ↦ (1 / 2) ^ n) 2

Tactic:
convert! hasSum_geometric_of_lt_one _ _

Premises used: hasSum_geometric_of_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
⊢ 2 = (1 - 1 / 2)⁻¹

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
⊢ 0 ≤ 1 / 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
⊢ 1 / 2 < 1

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

Tactic:
⟨_, hasSum_geometric_two⟩

Premises used: hasSum_geometric_two, Exists.intro, Summable
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ι : Type u_4
inst : Encodable ι
⊢ Summable (α := ℝ) fun (i : ι) ↦ (1 / 2) ^ Encodable.encode i

Tactic:
summable_geometric_two.comp_injective Encodable.encode_injective

Premises used: Encodable.encode_injective, Summable.comp_injective, summable_geometric_two
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
⊢ Eq (α := ℝ) (∑' (n : ℕ), (1 / 2) ^ n) 2

Tactic:
hasSum_geometric_two.tsum_eq

Premises used: hasSum_geometric_two, HasSum.tsum_eq
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
n i : ℕ
ha : 0 ≤ 1 / 2
⊢ 0 ≤ (1 / 2) ^ i

Tactic:
apply pow_nonneg

Premises used: pow_nonneg
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
n i : ℕ
⊢ 0 ≤ 1 / 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
n : ℕ
⊢ ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i

Tactic:
have : ∀ i, 0 ≤ (1 / (2 : ℝ)) ^ i := by
    intro i
    apply pow_nonneg
    norm_num
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
n : ℕ
this : ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.range n, (1 / 2) ^ i) (∑' (i : ℕ), (1 / 2) ^ i)

Tactic:
summable_geometric_two.sum_le_tsum (range n) (fun i _ ↦ this i)

Premises used: Finset.range, Summable.sum_le_tsum, summable_geometric_two
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
n : ℕ
this : ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i
h : Eq (α := ℝ) 2 (∑' (i : ℕ), (1 / 2) ^ i)
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.range n, (1 / 2) ^ i) 2

Tactic:
convert! summable_geometric_two.sum_le_tsum (range n) (fun i _ ↦ this i)

Premises used: Finset.range, Summable.sum_le_tsum, summable_geometric_two
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
n : ℕ
this : ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i
⊢ Eq (α := ℝ) 2 (∑' (i : ℕ), (1 / 2) ^ i)

Tactic:
tsum_geometric_two.symm

Premises used: tsum_geometric_two, Eq.symm
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
n : ℕ
this : ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i
⊢ Eq (α := ℝ) 2 (∑' (i : ℕ), (1 / 2) ^ i)

Tactic:
exact tsum_geometric_two.symm

Premises used: tsum_geometric_two, Eq.symm
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
⊢ Eq (α := ℝ) (∑' (n : ℕ), HPow.hPow (α := ℝ) 2⁻¹ n) 2

Tactic:
(inv_eq_one_div (2 : ℝ)).symm ▸ tsum_geometric_two

Premises used: Eq.rec, tsum_geometric_two, inv_eq_one_div, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
n : ℕ
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ if n ≤ i then HPow.hPow (α := ℝ) 2⁻¹ i else 0

Tactic:
simpa only [← piecewise_eq_indicator, one_div]
      using summable_geometric_two.indicator {i | n ≤ i}

Premises used: setOf, LE.le, one_div, summable_geometric_two, Set.piecewise_eq_indicator, Summable.indicator