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

State before:
n : ℕ
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
⊢ iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
Tactic:
induction n with
| zero => simp
| succ n h =>
  simp [iteratedDeriv_succ, h]
  ext x
  apply deriv_add
  . apply Differentiable.differentiableAt
    exact ContDiff.differentiable_iteratedDeriv _ hf (WithTop.coe_lt_top _)
  . apply Differentiable.differentiableAt
    exact ContDiff.differentiable_iteratedDeriv _ hg (WithTop.coe_lt_top _)
State after:
no goals

State before:
case zero
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
⊢ iteratedDeriv Nat.zero (f + g) = iteratedDeriv Nat.zero f + iteratedDeriv Nat.zero g
Tactic:
simp
State after:
no goals

State before:
case succ
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
⊢ iteratedDeriv (Nat.succ n) (f + g) = iteratedDeriv (Nat.succ n) f + iteratedDeriv (Nat.succ n) g
Tactic:
simp [iteratedDeriv_succ, h]
State after:
case succ
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
⊢ deriv (iteratedDeriv n f + iteratedDeriv n g) = deriv (iteratedDeriv n f) + deriv (iteratedDeriv n g)

State before:
case succ
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
⊢ deriv (iteratedDeriv n f + iteratedDeriv n g) = deriv (iteratedDeriv n f) + deriv (iteratedDeriv n g)
Tactic:
ext x
State after:
case succ.h
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ deriv (iteratedDeriv n f + iteratedDeriv n g) x = (deriv (iteratedDeriv n f) + deriv (iteratedDeriv n g)) x

State before:
case succ.h
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ deriv (iteratedDeriv n f + iteratedDeriv n g) x = (deriv (iteratedDeriv n f) + deriv (iteratedDeriv n g)) x
Tactic:
apply deriv_add
State after:
case succ.h.hf
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ DifferentiableAt ℝ (fun y => iteratedDeriv n f y) x

case succ.h.hg
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ DifferentiableAt ℝ (fun y => iteratedDeriv n g y) x

State before:
case succ.h.hf
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ DifferentiableAt ℝ (fun y => iteratedDeriv n f y) x

case succ.h.hg
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ DifferentiableAt ℝ (fun y => iteratedDeriv n g y) x
Tactic:
. apply Differentiable.differentiableAt
  exact ContDiff.differentiable_iteratedDeriv _ hf (WithTop.coe_lt_top _)
State after:
case succ.h.hg
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ DifferentiableAt ℝ (fun y => iteratedDeriv n g y) x

State before:
case succ.h.hg
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ DifferentiableAt ℝ (fun y => iteratedDeriv n g y) x
Tactic:
. apply Differentiable.differentiableAt
  exact ContDiff.differentiable_iteratedDeriv _ hg (WithTop.coe_lt_top _)
State after:
no goals

State before:
case succ.h.hf
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ DifferentiableAt ℝ (fun y => iteratedDeriv n f y) x
Tactic:
apply Differentiable.differentiableAt
State after:
case succ.h.hf.h
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ Differentiable ℝ fun y => iteratedDeriv n f y

State before:
case succ.h.hf.h
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ Differentiable ℝ fun y => iteratedDeriv n f y
Tactic:
exact ContDiff.differentiable_iteratedDeriv _ hf (WithTop.coe_lt_top _)
State after:
no goals

State before:
case succ.h.hg
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ DifferentiableAt ℝ (fun y => iteratedDeriv n g y) x
Tactic:
apply Differentiable.differentiableAt
State after:
case succ.h.hg.h
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ Differentiable ℝ fun y => iteratedDeriv n g y

State before:
case succ.h.hg.h
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ Differentiable ℝ fun y => iteratedDeriv n g y
Tactic:
exact ContDiff.differentiable_iteratedDeriv _ hg (WithTop.coe_lt_top _)
State after:
no goals