-- Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean
theorem contDiff_polynomial_eval_inv_mul {n : ℕ∞} (p : ℝ[X]) :
    ContDiff ℝ n (fun x ↦ p.eval x⁻¹ * expNegInvGlue x)

Proof state:
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ ↑m fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
⊢ ↑m = ⊤ → AnalyticOn ℝ (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) univ

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ∞
p : ℝ[X]
⊢ ContDiff ℝ ↑n fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x

Tactic:
apply contDiff_all_iff_nat.2 (fun m => ?_) n

Result:
n : ℕ∞
p : ℝ[X]
m : ℕ
⊢ ContDiff ℝ ↑m fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x

Proof state:
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✝

Tactic:
exact (hasDerivAt_polynomial_eval_inv_mul p _).deriv

Result:
no goals

Proof state:
case succ
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ ↑m fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
⊢ ContDiff ℝ (↑m + 1) fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x

Tactic:
refine contDiff_succ_iff_deriv.2 ⟨differentiable_polynomial_eval_inv_mul _, by simp, ?_⟩

Result:
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)

Proof state:
case zero
n : ℕ∞
p : ℝ[X]
⊢ ContDiff ℝ ↑0 fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x

Tactic:
exact contDiff_zero.2 <| continuous_polynomial_eval_inv_mul _

Result:
no goals

Proof state:
case succ
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ ↑m fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
⊢ ContDiff ℝ ↑(m + 1) fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x

Tactic:
rw [show ((m + 1 : ℕ) : WithTop ℕ∞) = m + 1 from rfl]

Result:
case succ
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ ↑m fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
⊢ ContDiff ℝ (↑m + 1) fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x

Proof state:
n : ℕ∞
p : ℝ[X]
m : ℕ
⊢ ContDiff ℝ ↑m fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x

Tactic:
induction m generalizing p with
| zero => exact contDiff_zero.2 <| continuous_polynomial_eval_inv_mul _
| succ m ihm =>
  rw [show ((m + 1 : ℕ) : WithTop ℕ∞) = m + 1 from rfl]
  refine contDiff_succ_iff_deriv.2 ⟨differentiable_polynomial_eval_inv_mul _, by simp, ?_⟩
  convert ihm (X ^ 2 * (p - derivative (R := ℝ) p)) using 2
  exact (hasDerivAt_polynomial_eval_inv_mul p _).deriv

Result:
no goals

Proof state:
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)

Tactic:
convert ihm (X ^ 2 * (p - derivative (R := ℝ) p)) using 2

Result:
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✝