Theorem: Bump₁.iteratedDeriv_neg (ForML/BumpTopology.lean)

State before:
n : ℕ
f : ℝ → ℝ
⊢ iteratedDeriv n (-f) = -iteratedDeriv n f
Tactic:
induction n with
| zero => simp
| succ n h =>
  conv => rhs; rw [iteratedDeriv_succ]
  rw [iteratedDeriv_succ]
  rw [h]
  ext x
  conv => lhs; arg 1; intro x
  simp [deriv.neg']
State after:
no goals

State before:
case zero
f : ℝ → ℝ
⊢ iteratedDeriv Nat.zero (-f) = -iteratedDeriv Nat.zero f
Tactic:
simp
State after:
no goals

State before:
case succ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
⊢ iteratedDeriv (Nat.succ n) (-f) = -iteratedDeriv (Nat.succ n) f
Tactic:
conv => rhs; rw [iteratedDeriv_succ]
State after:
case succ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
⊢ iteratedDeriv (Nat.succ n) (-f) = -deriv (iteratedDeriv n f)

State before:
case succ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
⊢ iteratedDeriv (Nat.succ n) (-f) = -deriv (iteratedDeriv n f)
Tactic:
rw [iteratedDeriv_succ]
State after:
case succ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
⊢ deriv (iteratedDeriv n (-f)) = -deriv (iteratedDeriv n f)

State before:
case succ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
⊢ deriv (iteratedDeriv n (-f)) = -deriv (iteratedDeriv n f)
Tactic:
rw [h]
State after:
case succ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
⊢ deriv (-iteratedDeriv n f) = -deriv (iteratedDeriv n f)

State before:
case succ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
⊢ deriv (-iteratedDeriv n f) = -deriv (iteratedDeriv n f)
Tactic:
ext x
State after:
case succ.h
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
x : ℝ
⊢ deriv (-iteratedDeriv n f) x = (-deriv (iteratedDeriv n f)) x

State before:
case succ.h
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
x : ℝ
⊢ deriv (-iteratedDeriv n f) x = (-deriv (iteratedDeriv n f)) x
Tactic:
conv => lhs; arg 1; intro x
State after:
case succ.h
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
x : ℝ
⊢ deriv (fun x => (-iteratedDeriv n f) x) x = (-deriv (iteratedDeriv n f)) x

State before:
case succ.h
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
x : ℝ
⊢ deriv (fun x => (-iteratedDeriv n f) x) x = (-deriv (iteratedDeriv n f)) x
Tactic:
simp [deriv.neg']
State after:
no goals