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

State before:
n : ℕ
⊢ iteratedDeriv n 0 = 0
Tactic:
induction n with
| zero => simp
| succ n h =>
  simp [iteratedDeriv_succ, h]
  ext x
  apply deriv_const
State after:
no goals

State before:
case zero

⊢ iteratedDeriv Nat.zero 0 = 0
Tactic:
simp
State after:
no goals

State before:
case succ
n : ℕ
h : iteratedDeriv n 0 = 0
⊢ iteratedDeriv (Nat.succ n) 0 = 0
Tactic:
simp [iteratedDeriv_succ, h]
State after:
case succ
n : ℕ
h : iteratedDeriv n 0 = 0
⊢ deriv 0 = 0

State before:
case succ
n : ℕ
h : iteratedDeriv n 0 = 0
⊢ deriv 0 = 0
Tactic:
ext x
State after:
case succ.h
n : ℕ
h : iteratedDeriv n 0 = 0
x : ℝ
⊢ deriv 0 x = 0 x

State before:
case succ.h
n : ℕ
h : iteratedDeriv n 0 = 0
x : ℝ
⊢ deriv 0 x = 0 x
Tactic:
apply deriv_const
State after:
no goals