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

State before:
n : ℕ
r : ℝ
f : ℝ → ℝ
⊢ iteratedDeriv n (r • f) = r • 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_const_mul]
State after:
no goals

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

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

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

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

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

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

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