Theorem: hasDerivAt_ene (Ray/Dynamics/Multibrot/Potential.lean)

State before:
c z : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
⊢ HasDerivAt ene (-dene x) x
Tactic:
have h : HasDerivAt (fun x ↦ exp (-exp x)) (exp (-exp x) * -exp x) x :=
  HasDerivAt.exp (Real.hasDerivAt_exp x).neg
State after:
c z : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
h : HasDerivAt (fun x => (-x.exp).exp) ((-x.exp).exp * -x.exp) x
⊢ HasDerivAt ene (-dene x) x

State before:
c z : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
h : HasDerivAt (fun x => (-x.exp).exp) ((-x.exp).exp * -x.exp) x
⊢ HasDerivAt ene (-dene x) x
Tactic:
simp only [mul_neg, ← Real.exp_add, neg_add_eq_sub] at h
State after:
c z : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
h : HasDerivAt (fun x => (-x.exp).exp) (-(x - x.exp).exp) x
⊢ HasDerivAt ene (-dene x) x

State before:
c z : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
h : HasDerivAt (fun x => (-x.exp).exp) (-(x - x.exp).exp) x
⊢ HasDerivAt ene (-dene x) x
Tactic:
exact h
State after:
no goals