case inl
p : ℝ[X]
x : ℝ
hx : x < 0
⊢ HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x)
    (Polynomial.eval x⁻¹ (X ^ 2 * (p - ↑derivative p)) * expNegInvGlue x) x

case inr.inl
p : ℝ[X]
⊢ HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x)
    (Polynomial.eval 0⁻¹ (X ^ 2 * (p - ↑derivative p)) * expNegInvGlue 0) 0

case inr.inr
p : ℝ[X]
x : ℝ
hx : 0 < x
⊢ HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x)
    (Polynomial.eval x⁻¹ (X ^ 2 * (p - ↑derivative p)) * expNegInvGlue x) x
p : ℝ[X]
x : ℝ
⊢ HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x)
    (Polynomial.eval x⁻¹ (X ^ 2 * (p - ↑derivative p)) * expNegInvGlue x) x
rcases lt_trichotomy x 0 with hx | rfl | hx
case inl
p : ℝ[X]
x : ℝ
hx : x < 0
⊢ HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) 0 x
case inl
p : ℝ[X]
x : ℝ
hx : x < 0
⊢ HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x)
    (Polynomial.eval x⁻¹ (X ^ 2 * (p - ↑derivative p)) * expNegInvGlue x) x
rw [zero_of_nonpos hx.le, mul_zero]
case inl
p : ℝ[X]
x : ℝ
hx : x < 0
⊢ (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) =ᶠ[𝓝 x] fun x => 0
case inl
p : ℝ[X]
x : ℝ
hx : x < 0
⊢ HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) 0 x
refine (hasDerivAt_const _ 0).congr_of_eventuallyEq ?_
case h
p : ℝ[X]
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
⊢ Polynomial.eval y⁻¹ p * expNegInvGlue y = 0
case inl
p : ℝ[X]
x : ℝ
hx : x < 0
⊢ (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) =ᶠ[𝓝 x] fun x => 0
filter_upwards [gt_mem_nhds hx] with y hy
no goals
case h
p : ℝ[X]
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
⊢ Polynomial.eval y⁻¹ p * expNegInvGlue y = 0
rw [zero_of_nonpos hy.le, mul_zero]
case inr.inl
p : ℝ[X]
⊢ Tendsto (slope (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) 0) (𝓝[{0}ᶜ] 0) (𝓝 0)
case inr.inl
p : ℝ[X]
⊢ HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x)
    (Polynomial.eval 0⁻¹ (X ^ 2 * (p - ↑derivative p)) * expNegInvGlue 0) 0
rw [expNegInvGlue.zero, mul_zero, hasDerivAt_iff_tendsto_slope]
case inr.inl
p : ℝ[X]
x : ℝ
⊢ Polynomial.eval x⁻¹ (p * X) * expNegInvGlue x = slope (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) 0 x
case inr.inl
p : ℝ[X]
⊢ Tendsto (slope (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) 0) (𝓝[{0}ᶜ] 0) (𝓝 0)
refine ((tendsto_polynomial_inv_mul_zero (p * X)).mono_left inf_le_left).congr fun x ↦ ?_
no goals
case inr.inl
p : ℝ[X]
x : ℝ
⊢ Polynomial.eval x⁻¹ (p * X) * expNegInvGlue x = slope (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) 0 x
simp [slope_def_field, div_eq_mul_inv, mul_right_comm]
case inr.inr
p : ℝ[X]
x : ℝ
hx : 0 < x
this :
  HasDerivAt ((fun y => Polynomial.eval y p * exp (-y)) ∘ Inv.inv)
    ((Polynomial.eval x⁻¹ (↑derivative p) * exp (-x⁻¹) + Polynomial.eval x⁻¹ p * (exp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹) x
⊢ HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x)
    (Polynomial.eval x⁻¹ (X ^ 2 * (p - ↑derivative p)) * expNegInvGlue x) x
case inr.inr
p : ℝ[X]
x : ℝ
hx : 0 < x
⊢ HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x)
    (Polynomial.eval x⁻¹ (X ^ 2 * (p - ↑derivative p)) * expNegInvGlue x) x
have := ((p.hasDerivAt x⁻¹).mul (hasDerivAt_neg _).exp).comp x (hasDerivAt_inv hx.ne')
case h.e'_7
p : ℝ[X]
x : ℝ
hx : 0 < x
this :
  HasDerivAt ((fun y => Polynomial.eval y p * exp (-y)) ∘ Inv.inv)
    ((Polynomial.eval x⁻¹ (↑derivative p) * exp (-x⁻¹) + Polynomial.eval x⁻¹ p * (exp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹) x
⊢ Polynomial.eval x⁻¹ (X ^ 2 * (p - ↑derivative p)) * expNegInvGlue x =
    (Polynomial.eval x⁻¹ (↑derivative p) * exp (-x⁻¹) + Polynomial.eval x⁻¹ p * (exp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹

case inr.inr.convert_2
p : ℝ[X]
x : ℝ
hx : 0 < x
this :
  HasDerivAt ((fun y => Polynomial.eval y p * exp (-y)) ∘ Inv.inv)
    ((Polynomial.eval x⁻¹ (↑derivative p) * exp (-x⁻¹) + Polynomial.eval x⁻¹ p * (exp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹) x
⊢ (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) =ᶠ[𝓝 x] (fun y => Polynomial.eval y p * exp (-y)) ∘ Inv.inv
case inr.inr
p : ℝ[X]
x : ℝ
hx : 0 < x
this :
  HasDerivAt ((fun y => Polynomial.eval y p * exp (-y)) ∘ Inv.inv)
    ((Polynomial.eval x⁻¹ (↑derivative p) * exp (-x⁻¹) + Polynomial.eval x⁻¹ p * (exp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹) x
⊢ HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x)
    (Polynomial.eval x⁻¹ (X ^ 2 * (p - ↑derivative p)) * expNegInvGlue x) x
convert this.congr_of_eventuallyEq _ using 1
case h.e'_7
p : ℝ[X]
x : ℝ
hx : 0 < x
this :
  HasDerivAt ((fun y => Polynomial.eval y p * exp (-y)) ∘ Inv.inv)
    ((Polynomial.eval x⁻¹ (↑derivative p) * exp (-x⁻¹) + Polynomial.eval x⁻¹ p * (exp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹) x
⊢ (x ^ 2)⁻¹ * (Polynomial.eval x⁻¹ p - Polynomial.eval x⁻¹ (↑derivative p)) * exp (-x⁻¹) =
    -((Polynomial.eval x⁻¹ (↑derivative p) * exp (-x⁻¹) + -(Polynomial.eval x⁻¹ p * exp (-x⁻¹))) * (x ^ 2)⁻¹)
case h.e'_7
p : ℝ[X]
x : ℝ
hx : 0 < x
this :
  HasDerivAt ((fun y => Polynomial.eval y p * exp (-y)) ∘ Inv.inv)
    ((Polynomial.eval x⁻¹ (↑derivative p) * exp (-x⁻¹) + Polynomial.eval x⁻¹ p * (exp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹) x
⊢ Polynomial.eval x⁻¹ (X ^ 2 * (p - ↑derivative p)) * expNegInvGlue x =
    (Polynomial.eval x⁻¹ (↑derivative p) * exp (-x⁻¹) + Polynomial.eval x⁻¹ p * (exp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹
simp [expNegInvGlue, hx.not_le]
no goals
case h.e'_7
p : ℝ[X]
x : ℝ
hx : 0 < x
this :
  HasDerivAt ((fun y => Polynomial.eval y p * exp (-y)) ∘ Inv.inv)
    ((Polynomial.eval x⁻¹ (↑derivative p) * exp (-x⁻¹) + Polynomial.eval x⁻¹ p * (exp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹) x
⊢ (x ^ 2)⁻¹ * (Polynomial.eval x⁻¹ p - Polynomial.eval x⁻¹ (↑derivative p)) * exp (-x⁻¹) =
    -((Polynomial.eval x⁻¹ (↑derivative p) * exp (-x⁻¹) + -(Polynomial.eval x⁻¹ p * exp (-x⁻¹))) * (x ^ 2)⁻¹)
ring
case h
p : ℝ[X]
x : ℝ
hx : 0 < x
this :
  HasDerivAt ((fun y => Polynomial.eval y p * exp (-y)) ∘ Inv.inv)
    ((Polynomial.eval x⁻¹ (↑derivative p) * exp (-x⁻¹) + Polynomial.eval x⁻¹ p * (exp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹) x
y : ℝ
hy : 0 < y
⊢ Polynomial.eval y⁻¹ p * expNegInvGlue y = ((fun y => Polynomial.eval y p * exp (-y)) ∘ Inv.inv) y
case inr.inr.convert_2
p : ℝ[X]
x : ℝ
hx : 0 < x
this :
  HasDerivAt ((fun y => Polynomial.eval y p * exp (-y)) ∘ Inv.inv)
    ((Polynomial.eval x⁻¹ (↑derivative p) * exp (-x⁻¹) + Polynomial.eval x⁻¹ p * (exp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹) x
⊢ (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) =ᶠ[𝓝 x] (fun y => Polynomial.eval y p * exp (-y)) ∘ Inv.inv
filter_upwards [lt_mem_nhds hx] with y hy
no goals
case h
p : ℝ[X]
x : ℝ
hx : 0 < x
this :
  HasDerivAt ((fun y => Polynomial.eval y p * exp (-y)) ∘ Inv.inv)
    ((Polynomial.eval x⁻¹ (↑derivative p) * exp (-x⁻¹) + Polynomial.eval x⁻¹ p * (exp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹) x
y : ℝ
hy : 0 < y
⊢ Polynomial.eval y⁻¹ p * expNegInvGlue y = ((fun y => Polynomial.eval y p * exp (-y)) ∘ Inv.inv) y
simp [expNegInvGlue, hy.not_le]