-- Mathlib/NumberTheory/Transcendental/Lindemann/Init/AnalyticalPart.lean
theorem hasDerivAt_cexp_mul_sumIDeriv (p : ℂ[X]) (s : ℂ) (x : ℝ) :
    HasDerivAt (fun x : ℝ ↦ -(cexp (-(x • s)) * p.sumIDeriv.eval (x • s)))
      (s * (cexp (-(x • s)) * p.eval (x • s))) x

Proof state:
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun y => y • s) (1 • s) x
h₁ : HasDerivAt (fun x => cexp (-(x • s))) (cexp (-(x • s)) * -(1 • s)) x
⊢ HasDerivAt (fun x => -(cexp (-(x • s)) * eval (x • s) (sumIDeriv p))) (s * (cexp (-(x • s)) * eval (x • s) p)) x

Tactic:
have h₂ := ((sumIDeriv p).hasDerivAt (x • s)).comp x h₀

Result:
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun y => y • s) (1 • s) x
h₁ : HasDerivAt (fun x => cexp (-(x • s))) (cexp (-(x • s)) * -(1 • s)) x
h₂ : HasDerivAt ((fun x => eval x (sumIDeriv p)) ∘ fun y => y • s) (eval (x • s) (derivative (sumIDeriv p)) * 1 • s) x
⊢ HasDerivAt (fun x => -(cexp (-(x • s)) * eval (x • s) (sumIDeriv p))) (s * (cexp (-(x • s)) * eval (x • s) p)) x

Proof state:
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun y => y • s) (1 • s) x
⊢ HasDerivAt (fun x => -(cexp (-(x • s)) * eval (x • s) (sumIDeriv p))) (s * (cexp (-(x • s)) * eval (x • s) p)) x

Tactic:
have h₁ := h₀.neg.cexp

Result:
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun y => y • s) (1 • s) x
h₁ : HasDerivAt (fun x => cexp (-(x • s))) (cexp (-(x • s)) * -(1 • s)) x
⊢ HasDerivAt (fun x => -(cexp (-(x • s)) * eval (x • s) (sumIDeriv p))) (s * (cexp (-(x • s)) * eval (x • s) p)) x

Proof state:
case h.e'_9
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun y => y • s) (1 • s) x
h₁ : HasDerivAt (fun x => cexp (-(x • s))) (cexp (-(x • s)) * -(1 • s)) x
h₂ : HasDerivAt ((fun x => eval x (sumIDeriv p)) ∘ fun y => y • s) (eval (x • s) (derivative (sumIDeriv p)) * 1 • s) x
⊢ s * (cexp (-(x • s)) * eval (x • s) p) =
    -(cexp (-(x • s)) * -(1 • s) * ((fun x => eval x (sumIDeriv p)) ∘ fun y => y • s) x +
        cexp (-(x • s)) * (eval (x • s) (derivative (sumIDeriv p)) * 1 • s))

Tactic:
nth_rw 1 [sumIDeriv_eq_self_add p]

Result:
case h.e'_9
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun y => y • s) (1 • s) x
h₁ : HasDerivAt (fun x => cexp (-(x • s))) (cexp (-(x • s)) * -(1 • s)) x
h₂ : HasDerivAt ((fun x => eval x (sumIDeriv p)) ∘ fun y => y • s) (eval (x • s) (derivative (sumIDeriv p)) * 1 • s) x
⊢ s * (cexp (-(x • s)) * eval (x • s) p) =
    -(cexp (-(x • s)) * -(1 • s) * ((fun x => eval x (p + derivative (sumIDeriv p))) ∘ fun y => y • s) x +
        cexp (-(x • s)) * (eval (x • s) (derivative (sumIDeriv p)) * 1 • s))

Proof state:
case h.e'_9
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun y => y • s) (1 • s) x
h₁ : HasDerivAt (fun x => cexp (-(x • s))) (cexp (-(x • s)) * -(1 • s)) x
h₂ : HasDerivAt ((fun x => eval x (sumIDeriv p)) ∘ fun y => y • s) (eval (x • s) (derivative (sumIDeriv p)) * 1 • s) x
⊢ s * (cexp (-(x • s)) * eval (x • s) p) =
    -(cexp (-(x • s)) * -s * (eval (x • s) p + eval (x • s) (derivative (sumIDeriv p))) +
        cexp (-(x • s)) * (eval (x • s) (derivative (sumIDeriv p)) * s))

Tactic:
ring

Result:
no goals

Proof state:
case h.e'_9
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun y => y • s) (1 • s) x
h₁ : HasDerivAt (fun x => cexp (-(x • s))) (cexp (-(x • s)) * -(1 • s)) x
h₂ : HasDerivAt ((fun x => eval x (sumIDeriv p)) ∘ fun y => y • s) (eval (x • s) (derivative (sumIDeriv p)) * 1 • s) x
⊢ s * (cexp (-(x • s)) * eval (x • s) p) =
    -(cexp (-(x • s)) * -(1 • s) * ((fun x => eval x (p + derivative (sumIDeriv p))) ∘ fun y => y • s) x +
        cexp (-(x • s)) * (eval (x • s) (derivative (sumIDeriv p)) * 1 • s))

Tactic:
simp only [one_smul, eval_add, Function.comp_apply]

Result:
case h.e'_9
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun y => y • s) (1 • s) x
h₁ : HasDerivAt (fun x => cexp (-(x • s))) (cexp (-(x • s)) * -(1 • s)) x
h₂ : HasDerivAt ((fun x => eval x (sumIDeriv p)) ∘ fun y => y • s) (eval (x • s) (derivative (sumIDeriv p)) * 1 • s) x
⊢ s * (cexp (-(x • s)) * eval (x • s) p) =
    -(cexp (-(x • s)) * -s * (eval (x • s) p + eval (x • s) (derivative (sumIDeriv p))) +
        cexp (-(x • s)) * (eval (x • s) (derivative (sumIDeriv p)) * s))

Proof state:
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun y => y • s) (1 • s) x
h₁ : HasDerivAt (fun x => cexp (-(x • s))) (cexp (-(x • s)) * -(1 • s)) x
h₂ : HasDerivAt ((fun x => eval x (sumIDeriv p)) ∘ fun y => y • s) (eval (x • s) (derivative (sumIDeriv p)) * 1 • s) x
⊢ HasDerivAt (fun x => -(cexp (-(x • s)) * eval (x • s) (sumIDeriv p))) (s * (cexp (-(x • s)) * eval (x • s) p)) x

Tactic:
convert (h₁.mul h₂).neg using 1

Result:
case h.e'_9
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun y => y • s) (1 • s) x
h₁ : HasDerivAt (fun x => cexp (-(x • s))) (cexp (-(x • s)) * -(1 • s)) x
h₂ : HasDerivAt ((fun x => eval x (sumIDeriv p)) ∘ fun y => y • s) (eval (x • s) (derivative (sumIDeriv p)) * 1 • s) x
⊢ s * (cexp (-(x • s)) * eval (x • s) p) =
    -(cexp (-(x • s)) * -(1 • s) * ((fun x => eval x (sumIDeriv p)) ∘ fun y => y • s) x +
        cexp (-(x • s)) * (eval (x • s) (derivative (sumIDeriv p)) * 1 • s))

Proof state:
p : ℂ[X]
s : ℂ
x : ℝ
⊢ HasDerivAt (fun x => -(cexp (-(x • s)) * eval (x • s) (sumIDeriv p))) (s * (cexp (-(x • s)) * eval (x • s) p)) x

Tactic:
have h₀ := (hasDerivAt_id' x).smul_const s

Result:
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun y => y • s) (1 • s) x
⊢ HasDerivAt (fun x => -(cexp (-(x • s)) * eval (x • s) (sumIDeriv p))) (s * (cexp (-(x • s)) * eval (x • s) p)) x