p : ℝ[X]
⊢ Tendsto (fun x => if x ≤ 0 then 0 else Polynomial.eval x⁻¹ p * exp (-x⁻¹)) (𝓝 0) (𝓝 0)
p : ℝ[X]
⊢ Tendsto (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) (𝓝 0) (𝓝 0)
simp only [expNegInvGlue, mul_ite, mul_zero]
p : ℝ[X]
⊢ Tendsto (fun x => Polynomial.eval x⁻¹ p * exp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x | ¬x ≤ 0}) (𝓝 0)
p : ℝ[X]
⊢ Tendsto (fun x => if x ≤ 0 then 0 else Polynomial.eval x⁻¹ p * exp (-x⁻¹)) (𝓝 0) (𝓝 0)
refine tendsto_const_nhds.if ?_
p : ℝ[X]
⊢ Tendsto (fun x => Polynomial.eval x⁻¹ p * exp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x | 0 < x}) (𝓝 0)
p : ℝ[X]
⊢ Tendsto (fun x => Polynomial.eval x⁻¹ p * exp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x | ¬x ≤ 0}) (𝓝 0)
simp only [not_le]
p : ℝ[X]
this : Tendsto (fun x => Polynomial.eval x⁻¹ p / exp x⁻¹) (𝓝[Ioi 0] 0) (𝓝 0)
⊢ Tendsto (fun x => Polynomial.eval x⁻¹ p * exp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x | 0 < x}) (𝓝 0)
p : ℝ[X]
⊢ Tendsto (fun x => Polynomial.eval x⁻¹ p * exp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x | 0 < x}) (𝓝 0)
have : Tendsto (fun x ↦ p.eval x⁻¹ / exp x⁻¹) (𝓝[>] 0) (𝓝 0) :=
  p.tendsto_div_exp_atTop.comp tendsto_inv_zero_atTop
p : ℝ[X]
this : Tendsto (fun x => Polynomial.eval x⁻¹ p / exp x⁻¹) (𝓝[Ioi 0] 0) (𝓝 0)
x : ℝ
hx : x ∈ {x | 0 < x}
⊢ x ∈ {x | (fun x => Polynomial.eval x⁻¹ p / exp x⁻¹ = (fun x => Polynomial.eval x⁻¹ p * exp (-x⁻¹)) x) x}
p : ℝ[X]
this : Tendsto (fun x => Polynomial.eval x⁻¹ p / exp x⁻¹) (𝓝[Ioi 0] 0) (𝓝 0)
⊢ Tendsto (fun x => Polynomial.eval x⁻¹ p * exp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x | 0 < x}) (𝓝 0)
refine this.congr' <| mem_of_superset self_mem_nhdsWithin fun x hx ↦ ?_
no goals
p : ℝ[X]
this : Tendsto (fun x => Polynomial.eval x⁻¹ p / exp x⁻¹) (𝓝[Ioi 0] 0) (𝓝 0)
x : ℝ
hx : x ∈ {x | 0 < x}
⊢ x ∈ {x | (fun x => Polynomial.eval x⁻¹ p / exp x⁻¹ = (fun x => Polynomial.eval x⁻¹ p * exp (-x⁻¹)) x) x}
simp [expNegInvGlue, hx.out.not_le, exp_neg, div_eq_mul_inv]