[GOAL]
p : ℝ[X]
⊢ Tendsto (fun x => eval x p / exp x) atTop (𝓝 0)
[PROOFSTEP]
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
[GOAL]
p : ℝ[X]
⊢ Tendsto (fun x => eval x p / exp x) atTop (𝓝 0)
[PROOFSTEP]
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
[GOAL]
case h_monomial
n : ℕ
c : ℝ
⊢ Tendsto (fun x => eval x (↑(monomial n) c) / exp x) atTop (𝓝 0)
[PROOFSTEP]

| 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)
[GOAL]
case h_monomial
n : ℕ
c : ℝ
⊢ Tendsto (fun x => eval x (↑(monomial n) c) / exp x) atTop (𝓝 0)
[PROOFSTEP]
simpa [exp_neg, div_eq_mul_inv, mul_assoc] using tendsto_const_nhds.mul (tendsto_pow_mul_exp_neg_atTop_nhds_0 n)
[GOAL]
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)
[PROOFSTEP]

| h_add p q hp hq => simpa [add_div] using hp.add hq
[GOAL]
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)
[PROOFSTEP]
simpa [add_div] using hp.add hq
