case hgf
a : ℝ
ha : 0 < a
b : ℝ
⊢ ∀ᶠ (x : ℝ) in atTop, x ^ b = 0 → exp (-a * x) = 0

case a
a : ℝ
ha : 0 < a
b : ℝ
⊢ Tendsto (fun x => exp (-a * x) / x ^ b) atTop (𝓝 0)
a : ℝ
ha : 0 < a
b : ℝ
⊢ (fun x => exp (-a * x)) =o[atTop] fun x => x ^ b
apply isLittleO_of_tendsto'
case hgf
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 < t
h : t ^ b = 0
⊢ exp (-a * t) = 0
case hgf
a : ℝ
ha : 0 < a
b : ℝ
⊢ ∀ᶠ (x : ℝ) in atTop, x ^ b = 0 → exp (-a * x) = 0
refine' (eventually_gt_atTop 0).mp (eventually_of_forall fun t ht h => _)
case hgf
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 < t
h : t = 0 ∧ b ≠ 0
⊢ exp (-a * t) = 0
case hgf
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 < t
h : t ^ b = 0
⊢ exp (-a * t) = 0
rw [rpow_eq_zero_iff_of_nonneg ht.le] at h
no goals
case hgf
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 < t
h : t = 0 ∧ b ≠ 0
⊢ exp (-a * t) = 0
exact (ht.ne' h.1).elim
case a
a : ℝ
ha : 0 < a
b : ℝ
⊢ (fun x => exp (a * x) / x ^ (-b))⁻¹ =ᶠ[atTop] fun x => exp (-a * x) / x ^ b
case a
a : ℝ
ha : 0 < a
b : ℝ
⊢ Tendsto (fun x => exp (-a * x) / x ^ b) atTop (𝓝 0)
refine' (tendsto_exp_mul_div_rpow_atTop (-b) a ha).inv_tendsto_atTop.congr' _
case a
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 ≤ t
⊢ (fun x => exp (a * x) / x ^ (-b))⁻¹ t = (fun x => exp (-a * x) / x ^ b) t
case a
a : ℝ
ha : 0 < a
b : ℝ
⊢ (fun x => exp (a * x) / x ^ (-b))⁻¹ =ᶠ[atTop] fun x => exp (-a * x) / x ^ b
refine' (eventually_ge_atTop 0).mp (eventually_of_forall fun t ht => _)
case a
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 ≤ t
⊢ (fun x => exp (a * x) / x ^ (-b))⁻¹ t = exp (-a * t) / t ^ b
case a
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 ≤ t
⊢ (fun x => exp (a * x) / x ^ (-b))⁻¹ t = (fun x => exp (-a * x) / x ^ b) t
dsimp only
no goals
case a
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 ≤ t
⊢ (fun x => exp (a * x) / x ^ (-b))⁻¹ t = exp (-a * t) / t ^ b
rw [Pi.inv_apply, inv_div, ← inv_div_inv, neg_mul, Real.exp_neg, rpow_neg ht, inv_inv]