[GOAL]
x : ℝ
hx : x ≤ 0
⊢ expNegInvGlue x = 0
[PROOFSTEP]
simp [expNegInvGlue, hx]
[GOAL]
x : ℝ
hx : 0 < x
⊢ 0 < expNegInvGlue x
[PROOFSTEP]
simp [expNegInvGlue, not_le.2 hx, exp_pos]
[GOAL]
x : ℝ
⊢ 0 ≤ expNegInvGlue x
[PROOFSTEP]
cases le_or_gt x 0 with
| inl h => exact ge_of_eq (zero_of_nonpos h)
| inr h => exact le_of_lt (pos_of_pos h)
[GOAL]
x : ℝ
x✝ : x ≤ 0 ∨ x > 0
⊢ 0 ≤ expNegInvGlue x
[PROOFSTEP]
cases le_or_gt x 0 with
| inl h => exact ge_of_eq (zero_of_nonpos h)
| inr h => exact le_of_lt (pos_of_pos h)
[GOAL]
case inl
x : ℝ
h : x ≤ 0
⊢ 0 ≤ expNegInvGlue x
[PROOFSTEP]

| inl h => exact ge_of_eq (zero_of_nonpos h)
[GOAL]
case inl
x : ℝ
h : x ≤ 0
⊢ 0 ≤ expNegInvGlue x
[PROOFSTEP]
exact ge_of_eq (zero_of_nonpos h)
[GOAL]
case inr
x : ℝ
h : x > 0
⊢ 0 ≤ expNegInvGlue x
[PROOFSTEP]

| inr h => exact le_of_lt (pos_of_pos h)
[GOAL]
case inr
x : ℝ
h : x > 0
⊢ 0 ≤ expNegInvGlue x
[PROOFSTEP]
exact le_of_lt (pos_of_pos h)
[GOAL]
p : ℝ[X]
⊢ Tendsto (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) (𝓝 0) (𝓝 0)
[PROOFSTEP]
simp only [expNegInvGlue, mul_ite, mul_zero]
[GOAL]
p : ℝ[X]
⊢ Tendsto (fun x => if x ≤ 0 then 0 else Polynomial.eval x⁻¹ p * exp (-x⁻¹)) (𝓝 0) (𝓝 0)
[PROOFSTEP]
refine tendsto_const_nhds.if ?_
[GOAL]
p : ℝ[X]
⊢ Tendsto (fun x => Polynomial.eval x⁻¹ p * exp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x | ¬x ≤ 0}) (𝓝 0)
[PROOFSTEP]
simp only [not_le]
[GOAL]
p : ℝ[X]
⊢ Tendsto (fun x => Polynomial.eval x⁻¹ p * exp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x | 0 < x}) (𝓝 0)
[PROOFSTEP]
have : Tendsto (fun x ↦ p.eval x⁻¹ / exp x⁻¹) (𝓝[>] 0) (𝓝 0) := p.tendsto_div_exp_atTop.comp tendsto_inv_zero_atTop
[GOAL]
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)
[PROOFSTEP]
refine this.congr' <| mem_of_superset self_mem_nhdsWithin fun x hx ↦ ?_
[GOAL]
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}
[PROOFSTEP]
simp [expNegInvGlue, hx.out.not_le, exp_neg, div_eq_mul_inv]
[GOAL]
p : ℝ[X]
x : ℝ
⊢ HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x)
    (Polynomial.eval x⁻¹ (X ^ 2 * (p - ↑derivative p)) * expNegInvGlue x) x
[PROOFSTEP]
rcases lt_trichotomy x 0 with hx | rfl | hx
[GOAL]
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
[PROOFSTEP]
rw [zero_of_nonpos hx.le, mul_zero]
[GOAL]
case inl
p : ℝ[X]
x : ℝ
hx : x < 0
⊢ HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) 0 x
[PROOFSTEP]
refine (hasDerivAt_const _ 0).congr_of_eventuallyEq ?_
[GOAL]
case inl
p : ℝ[X]
x : ℝ
hx : x < 0
⊢ (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) =ᶠ[𝓝 x] fun x => 0
[PROOFSTEP]
filter_upwards [gt_mem_nhds hx] with y hy
[GOAL]
case h
p : ℝ[X]
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
⊢ Polynomial.eval y⁻¹ p * expNegInvGlue y = 0
[PROOFSTEP]
rw [zero_of_nonpos hy.le, mul_zero]
[GOAL]
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
[PROOFSTEP]
rw [expNegInvGlue.zero, mul_zero, hasDerivAt_iff_tendsto_slope]
[GOAL]
case inr.inl
p : ℝ[X]
⊢ Tendsto (slope (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) 0) (𝓝[{0}ᶜ] 0) (𝓝 0)
[PROOFSTEP]
refine ((tendsto_polynomial_inv_mul_zero (p * X)).mono_left inf_le_left).congr fun x ↦ ?_
[GOAL]
case inr.inl
p : ℝ[X]
x : ℝ
⊢ Polynomial.eval x⁻¹ (p * X) * expNegInvGlue x = slope (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) 0 x
[PROOFSTEP]
simp [slope_def_field, div_eq_mul_inv, mul_right_comm]
[GOAL]
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
[PROOFSTEP]
have := ((p.hasDerivAt x⁻¹).mul (hasDerivAt_neg _).exp).comp x (hasDerivAt_inv hx.ne')
[GOAL]
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
[PROOFSTEP]
convert this.congr_of_eventuallyEq _ using 1
[GOAL]
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)⁻¹
[PROOFSTEP]
simp [expNegInvGlue, hx.not_le]
[GOAL]
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)⁻¹)
[PROOFSTEP]
ring
[GOAL]
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
[PROOFSTEP]
filter_upwards [lt_mem_nhds hx] with y hy
[GOAL]
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
[PROOFSTEP]
simp [expNegInvGlue, hy.not_le]
[GOAL]
n : ℕ∞
p : ℝ[X]
⊢ ContDiff ℝ n fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
[PROOFSTEP]
apply contDiff_all_iff_nat.2 (fun m => ?_) n
[GOAL]
n : ℕ∞
p : ℝ[X]
m : ℕ
⊢ ContDiff ℝ ↑m fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
[PROOFSTEP]
induction m generalizing p with
| zero => exact contDiff_zero.2 <| continuous_polynomial_eval_inv_mul _
| succ m ihm =>
  refine contDiff_succ_iff_deriv.2 ⟨differentiable_polynomial_eval_inv_mul _, ?_⟩
  convert ihm (X ^ 2 * (p - derivative (R := ℝ) p)) using 2
  exact (hasDerivAt_polynomial_eval_inv_mul p _).deriv
[GOAL]
n : ℕ∞
p : ℝ[X]
m : ℕ
⊢ ContDiff ℝ ↑m fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
[PROOFSTEP]
induction m generalizing p with
| zero => exact contDiff_zero.2 <| continuous_polynomial_eval_inv_mul _
| succ m ihm =>
  refine contDiff_succ_iff_deriv.2 ⟨differentiable_polynomial_eval_inv_mul _, ?_⟩
  convert ihm (X ^ 2 * (p - derivative (R := ℝ) p)) using 2
  exact (hasDerivAt_polynomial_eval_inv_mul p _).deriv
[GOAL]
case zero
n : ℕ∞
p : ℝ[X]
⊢ ContDiff ℝ ↑Nat.zero fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
[PROOFSTEP]

| zero => exact contDiff_zero.2 <| continuous_polynomial_eval_inv_mul _
[GOAL]
case zero
n : ℕ∞
p : ℝ[X]
⊢ ContDiff ℝ ↑Nat.zero fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
[PROOFSTEP]
exact contDiff_zero.2 <| continuous_polynomial_eval_inv_mul _
[GOAL]
case succ
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ ↑m fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
⊢ ContDiff ℝ ↑(Nat.succ m) fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
[PROOFSTEP]

| succ m ihm =>
  refine contDiff_succ_iff_deriv.2 ⟨differentiable_polynomial_eval_inv_mul _, ?_⟩
  convert ihm (X ^ 2 * (p - derivative (R := ℝ) p)) using 2
  exact (hasDerivAt_polynomial_eval_inv_mul p _).deriv
[GOAL]
case succ
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ ↑m fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
⊢ ContDiff ℝ ↑(Nat.succ m) fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
[PROOFSTEP]
refine contDiff_succ_iff_deriv.2 ⟨differentiable_polynomial_eval_inv_mul _, ?_⟩
[GOAL]
case succ
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ ↑m fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
⊢ ContDiff ℝ (↑m) (deriv fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x)
[PROOFSTEP]
convert ihm (X ^ 2 * (p - derivative (R := ℝ) p)) using 2
[GOAL]
case h.e'_10.h
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ ↑m fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
x✝ : ℝ
⊢ deriv (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) x✝ =
    Polynomial.eval x✝⁻¹ (X ^ 2 * (p - ↑derivative p)) * expNegInvGlue x✝
[PROOFSTEP]
exact (hasDerivAt_polynomial_eval_inv_mul p _).deriv
[GOAL]
n : ℕ∞
⊢ ContDiff ℝ n expNegInvGlue
[PROOFSTEP]
simpa using contDiff_polynomial_eval_inv_mul 1
[GOAL]
x : ℝ
h : 1 ≤ x
⊢ expNegInvGlue x = expNegInvGlue x + expNegInvGlue (1 - x)
[PROOFSTEP]
rw [zero_of_nonpos (sub_nonpos.2 h), add_zero]
[GOAL]
x : ℝ
⊢ smoothTransition x = 0 ↔ x ≤ 0
[PROOFSTEP]
simp only [smoothTransition, _root_.div_eq_zero_iff, (pos_denom x).ne', zero_iff_nonpos, or_false]
[GOAL]
x : ℝ
⊢ smoothTransition ↑(projIcc 0 1 (_ : 0 ≤ 1) x) = smoothTransition x
[PROOFSTEP]
refine' congr_fun (IccExtend_eq_self zero_le_one smoothTransition (fun x hx => _) fun x hx => _) x
[GOAL]
case refine'_1
x✝ x : ℝ
hx : x < 0
⊢ smoothTransition x = smoothTransition 0
[PROOFSTEP]
rw [smoothTransition.zero, zero_of_nonpos hx.le]
[GOAL]
case refine'_2
x✝ x : ℝ
hx : 1 < x
⊢ smoothTransition x = smoothTransition 1
[PROOFSTEP]
rw [smoothTransition.one, one_of_one_le hx.le]
