no goals
p : ℝ[X]
⊢ Tendsto (fun x => eval x p / exp x) atTop (𝓝 0)
induction p using Polynomial.induction_on' with
| h_monomial n c => simpa [exp_neg, div_eq_mul_inv, mul_assoc]
  using tendsto_const_nhds.mul (tendsto_pow_mul_exp_neg_atTop_nhds_0 n)
| h_add p q hp hq => simpa [add_div] using hp.add hq
no goals
case h_monomial
n : ℕ
c : ℝ
⊢ Tendsto (fun x => eval x (↑(monomial n) c) / exp x) atTop (𝓝 0)
simpa [exp_neg, div_eq_mul_inv, mul_assoc]
using tendsto_const_nhds.mul (tendsto_pow_mul_exp_neg_atTop_nhds_0 n)
no goals
case h_add
p q : ℝ[X]
hp : Tendsto (fun x => eval x p / exp x) atTop (𝓝 0)
hq : Tendsto (fun x => eval x q / exp x) atTop (𝓝 0)
⊢ Tendsto (fun x => eval x (p + q) / exp x) atTop (𝓝 0)
simpa [add_div] using hp.add hq