case refine'_1
ι : Type ?u.223673
ι' : Type ?u.223676
α : Type u_1
β : Type ?u.223682
γ : Type ?u.223685
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
h : Tendsto (fun x => c * x ^ n) atTop atTop
⊢ n ≠ 0

case refine'_2
ι : Type ?u.223673
ι' : Type ?u.223676
α : Type u_1
β : Type ?u.223682
γ : Type ?u.223685
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
h : Tendsto (fun x => c * x ^ n) atTop atTop
⊢ 0 < c
ι : Type ?u.223673
ι' : Type ?u.223676
α : Type u_1
β : Type ?u.223682
γ : Type ?u.223685
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
⊢ Tendsto (fun x => c * x ^ n) atTop atTop ↔ n ≠ 0 ∧ 0 < c
refine' ⟨fun h => ⟨_, _⟩, fun h => tendsto_const_mul_pow_atTop h.1 h.2⟩
case refine'_1
ι : Type ?u.223673
ι' : Type ?u.223676
α : Type u_1
β : Type ?u.223682
γ : Type ?u.223685
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
h : Tendsto (fun x => c * x ^ 0) atTop atTop
⊢ False
case refine'_1
ι : Type ?u.223673
ι' : Type ?u.223676
α : Type u_1
β : Type ?u.223682
γ : Type ?u.223685
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
h : Tendsto (fun x => c * x ^ n) atTop atTop
⊢ n ≠ 0
rintro rfl
no goals
case refine'_1
ι : Type ?u.223673
ι' : Type ?u.223676
α : Type u_1
β : Type ?u.223682
γ : Type ?u.223685
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
h : Tendsto (fun x => c * x ^ 0) atTop atTop
⊢ False
simp only [pow_zero, not_tendsto_const_atTop] at h
case refine'_2.intro.intro
ι : Type ?u.223673
ι' : Type ?u.223676
α : Type u_1
β : Type ?u.223682
γ : Type ?u.223685
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
h : Tendsto (fun x => c * x ^ n) atTop atTop
k : α
hck : 0 < c * k ^ n
hk : 0 ≤ k
⊢ 0 < c
case refine'_2
ι : Type ?u.223673
ι' : Type ?u.223676
α : Type u_1
β : Type ?u.223682
γ : Type ?u.223685
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
h : Tendsto (fun x => c * x ^ n) atTop atTop
⊢ 0 < c
rcases((h.eventually_gt_atTop 0).and (eventually_ge_atTop 0)).exists with ⟨k, hck, hk⟩
no goals
case refine'_2.intro.intro
ι : Type ?u.223673
ι' : Type ?u.223676
α : Type u_1
β : Type ?u.223682
γ : Type ?u.223685
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
h : Tendsto (fun x => c * x ^ n) atTop atTop
k : α
hck : 0 < c * k ^ n
hk : 0 ≤ k
⊢ 0 < c
exact pos_of_mul_pos_left hck (pow_nonneg hk _)