n : ℕ∞
p : ℝ[X]
m : ℕ
⊢ ContDiff ℝ ↑m fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
n : ℕ∞
p : ℝ[X]
⊢ ContDiff ℝ n fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
apply contDiff_all_iff_nat.2 (fun m => ?_) n
no goals
n : ℕ∞
p : ℝ[X]
m : ℕ
⊢ ContDiff ℝ ↑m fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
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
no goals
case zero
n : ℕ∞
p : ℝ[X]
⊢ ContDiff ℝ ↑Nat.zero fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
exact contDiff_zero.2 <| continuous_polynomial_eval_inv_mul _
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)
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
refine contDiff_succ_iff_deriv.2 ⟨differentiable_polynomial_eval_inv_mul _, ?_⟩
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✝
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)
convert ihm (X ^ 2 * (p - derivative (R := ℝ) p)) using 2
no goals
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✝
exact (hasDerivAt_polynomial_eval_inv_mul p _).deriv