case refine'_1
𝕜 : Type u_1
α : Type ?u.43044
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : Tendsto (fun x => c * x ^ n) atTop (𝓝 d)
⊢ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0

case refine'_2
𝕜 : Type u_1
α : Type ?u.43044
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n = 0 ∧ c = d ∨ n < 0 ∧ d = 0
⊢ Tendsto (fun x => c * x ^ n) atTop (𝓝 d)
𝕜 : Type u_1
α : Type ?u.43044
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
⊢ Tendsto (fun x => c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0
refine' ⟨fun h => _, fun h => _⟩
no goals
case refine'_1
𝕜 : Type u_1
α : Type ?u.43044
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : Tendsto (fun x => c * x ^ n) atTop (𝓝 d)
⊢ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0
cases n with | ofNat n =>
  left
  simpa [tendsto_const_mul_pow_nhds_iff hc] using h
| negSucc n =>
  have hn := Int.negSucc_lt_zero n
  exact Or.inr ⟨hn, tendsto_nhds_unique h (tendsto_const_mul_zpow_atTop_zero hn)⟩
case refine'_1.ofNat.h
𝕜 : Type u_1
α : Type ?u.43044
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
c d : 𝕜
hc : c ≠ 0
n : ℕ
h : Tendsto (fun x => c * x ^ Int.ofNat n) atTop (𝓝 d)
⊢ Int.ofNat n = 0 ∧ c = d
case refine'_1.ofNat
𝕜 : Type u_1
α : Type ?u.43044
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
c d : 𝕜
hc : c ≠ 0
n : ℕ
h : Tendsto (fun x => c * x ^ Int.ofNat n) atTop (𝓝 d)
⊢ Int.ofNat n = 0 ∧ c = d ∨ Int.ofNat n < 0 ∧ d = 0
left
no goals
case refine'_1.ofNat.h
𝕜 : Type u_1
α : Type ?u.43044
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
c d : 𝕜
hc : c ≠ 0
n : ℕ
h : Tendsto (fun x => c * x ^ Int.ofNat n) atTop (𝓝 d)
⊢ Int.ofNat n = 0 ∧ c = d
simpa [tendsto_const_mul_pow_nhds_iff hc] using h
case refine'_1.negSucc
𝕜 : Type u_1
α : Type ?u.43044
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
c d : 𝕜
hc : c ≠ 0
n : ℕ
h : Tendsto (fun x => c * x ^ Int.negSucc n) atTop (𝓝 d)
hn : Int.negSucc n < 0
⊢ Int.negSucc n = 0 ∧ c = d ∨ Int.negSucc n < 0 ∧ d = 0
case refine'_1.negSucc
𝕜 : Type u_1
α : Type ?u.43044
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
c d : 𝕜
hc : c ≠ 0
n : ℕ
h : Tendsto (fun x => c * x ^ Int.negSucc n) atTop (𝓝 d)
⊢ Int.negSucc n = 0 ∧ c = d ∨ Int.negSucc n < 0 ∧ d = 0
have hn := Int.negSucc_lt_zero n
no goals
case refine'_1.negSucc
𝕜 : Type u_1
α : Type ?u.43044
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
c d : 𝕜
hc : c ≠ 0
n : ℕ
h : Tendsto (fun x => c * x ^ Int.negSucc n) atTop (𝓝 d)
hn : Int.negSucc n < 0
⊢ Int.negSucc n = 0 ∧ c = d ∨ Int.negSucc n < 0 ∧ d = 0
exact Or.inr ⟨hn, tendsto_nhds_unique h (tendsto_const_mul_zpow_atTop_zero hn)⟩
case refine'_2.inl
𝕜 : Type u_1
α : Type ?u.43044
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n = 0 ∧ c = d
⊢ Tendsto (fun x => c * x ^ n) atTop (𝓝 d)

case refine'_2.inr
𝕜 : Type u_1
α : Type ?u.43044
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n < 0 ∧ d = 0
⊢ Tendsto (fun x => c * x ^ n) atTop (𝓝 d)
case refine'_2
𝕜 : Type u_1
α : Type ?u.43044
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n = 0 ∧ c = d ∨ n < 0 ∧ d = 0
⊢ Tendsto (fun x => c * x ^ n) atTop (𝓝 d)
cases' h with h h
case refine'_2.inl
𝕜 : Type u_1
α : Type ?u.43044
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n = 0 ∧ c = d
⊢ Tendsto (fun x => d) atTop (𝓝 d)
case refine'_2.inl
𝕜 : Type u_1
α : Type ?u.43044
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n = 0 ∧ c = d
⊢ Tendsto (fun x => c * x ^ n) atTop (𝓝 d)
simp only [h.left, h.right, zpow_zero, mul_one]
no goals
case refine'_2.inl
𝕜 : Type u_1
α : Type ?u.43044
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n = 0 ∧ c = d
⊢ Tendsto (fun x => d) atTop (𝓝 d)
exact tendsto_const_nhds
no goals
case refine'_2.inr
𝕜 : Type u_1
α : Type ?u.43044
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n < 0 ∧ d = 0
⊢ Tendsto (fun x => c * x ^ n) atTop (𝓝 d)
exact h.2.symm ▸ tendsto_const_mul_zpow_atTop_zero h.1