-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem tendsto_pow_atTop_nhds_zero_iff {𝕜 : Type*} [LinearOrderedField 𝕜] [Archimedean 𝕜]
    [TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} :
    Tendsto (fun n : ℕ ↦ r ^ n) atTop (𝓝 0) ↔ |r| < 1

Proof state:
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
b : 𝕜
⊢ ∃ a, b ≤ |r| ^ a

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

Result:
case intro
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
b : 𝕜
n : ℕ
hn : b < |r| ^ n
⊢ ∃ a, b ≤ |r| ^ a

Proof state:
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
⊢ Tendsto (fun n => |r| ^ n) atTop (𝓝 0)

Tactic:
simpa only [← abs_pow]

Result:
no goals

Proof state:
case pos
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
hr_le : ¬|r| < 1
hr : 1 = |r|
h : Tendsto (fun n => 1) atTop (𝓝 0)
⊢ False

Tactic:
exact zero_ne_one <| tendsto_nhds_unique h tendsto_const_nhds

Result:
no goals

Proof state:
case pos
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : 1 = |r|
⊢ False

Tactic:
replace h : Tendsto (fun n : ℕ ↦ |r|^n) atTop (𝓝 0) := by simpa only [← abs_pow, h]

Result:
case pos
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
hr_le : ¬|r| < 1
hr : 1 = |r|
h : Tendsto (fun n => |r| ^ n) atTop (𝓝 0)
⊢ False

Proof state:
case intro
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (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⟩

Result:
no goals

Proof state:
case pos
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
hr_le : ¬|r| < 1
hr : 1 = |r|
h : Tendsto (fun n => |r| ^ n) atTop (𝓝 0)
⊢ False

Tactic:
simp only [hr.symm, one_pow] at h

Result:
case pos
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
hr_le : ¬|r| < 1
hr : 1 = |r|
h : Tendsto (fun n => 1) atTop (𝓝 0)
⊢ False

Proof state:
case refine_1
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
⊢ False

Tactic:
by_cases hr : 1 = |r|

Result:
case pos
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : 1 = |r|
⊢ False

case neg
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
⊢ False

Proof state:
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
⊢ Tendsto (fun n => r ^ n) atTop (𝓝 0) ↔ |r| < 1

Tactic:
rw [tendsto_zero_iff_abs_tendsto_zero]

Result:
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
⊢ Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0) ↔ |r| < 1

Proof state:
case neg
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
⊢ False

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

Result:
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
⊢ Tendsto (fun n => |r| ^ n) atTop atTop

𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
⊢ Tendsto (fun n => |r| ^ n) atTop (𝓝 0)

Proof state:
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
⊢ Tendsto (fun n => |r| ^ n) atTop atTop

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

Result:
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
b : 𝕜
⊢ ∃ a, b ≤ |r| ^ a

Proof state:
case refine_2
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : |r| < 1
⊢ Tendsto (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

Result:
no goals

Proof state:
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
⊢ Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0) ↔ |r| < 1

Tactic:
refine ⟨fun h ↦ by_contra (fun hr_le ↦ ?_), fun h ↦ ?_⟩

Result:
case refine_1
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
⊢ False

case refine_2
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : |r| < 1
⊢ Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)

Proof state:
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : 1 = |r|
⊢ Tendsto (fun n => |r| ^ n) atTop (𝓝 0)

Tactic:
simpa only [← abs_pow, h]

Result:
no goals