-- Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
theorem iteratedDerivWithin_neg :
    iteratedDerivWithin n (-f) s x = -iteratedDerivWithin n f s x

Proof state:
case succ.e_f.h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f : 𝕜 → F
n : ℕ
IH : ∀ {x : 𝕜}, iteratedDerivWithin n (-f) s x = -iteratedDerivWithin n f s x
x y : 𝕜
⊢ iteratedDerivWithin n (-f) s y = -iteratedDerivWithin n f s y

Tactic:
exact IH

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f : 𝕜 → F
n : ℕ
IH : ∀ {x : 𝕜}, iteratedDerivWithin n (-f) s x = -iteratedDerivWithin n f s x
x : 𝕜
⊢ derivWithin (iteratedDerivWithin n (-f) s) s x = -derivWithin (iteratedDerivWithin n f s) s x

Tactic:
rw [← derivWithin.neg]

Result:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f : 𝕜 → F
n : ℕ
IH : ∀ {x : 𝕜}, iteratedDerivWithin n (-f) s x = -iteratedDerivWithin n f s x
x : 𝕜
⊢ derivWithin (iteratedDerivWithin n (-f) s) s x = derivWithin (fun y => -iteratedDerivWithin n f s y) s x

Proof state:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f : 𝕜 → F
n : ℕ
IH : ∀ {x : 𝕜}, iteratedDerivWithin n (-f) s x = -iteratedDerivWithin n f s x
x : 𝕜
⊢ derivWithin (iteratedDerivWithin n (-f) s) s x = derivWithin (fun y => -iteratedDerivWithin n f s y) s x

Tactic:
congr with y

Result:
case succ.e_f.h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f : 𝕜 → F
n : ℕ
IH : ∀ {x : 𝕜}, iteratedDerivWithin n (-f) s x = -iteratedDerivWithin n f s x
x y : 𝕜
⊢ iteratedDerivWithin n (-f) s y = -iteratedDerivWithin n f s y

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
⊢ iteratedDerivWithin n (-f) s x = -iteratedDerivWithin n f s x

Tactic:
induction n generalizing x with
| zero => simp
| succ n IH =>
  simp only [iteratedDerivWithin_succ, derivWithin_neg]
  rw [← derivWithin.neg]
  congr with y
  exact IH

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f : 𝕜 → F
n : ℕ
IH : ∀ {x : 𝕜}, iteratedDerivWithin n (-f) s x = -iteratedDerivWithin n f s x
x : 𝕜
⊢ iteratedDerivWithin (n + 1) (-f) s x = -iteratedDerivWithin (n + 1) f s x

Tactic:
simp only [iteratedDerivWithin_succ, derivWithin_neg]

Result:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f : 𝕜 → F
n : ℕ
IH : ∀ {x : 𝕜}, iteratedDerivWithin n (-f) s x = -iteratedDerivWithin n f s x
x : 𝕜
⊢ derivWithin (iteratedDerivWithin n (-f) s) s x = -derivWithin (iteratedDerivWithin n f s) s x

Proof state:
case zero
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f : 𝕜 → F
x : 𝕜
⊢ iteratedDerivWithin 0 (-f) s x = -iteratedDerivWithin 0 f s x

Tactic:
simp

Result:
no goals