-- Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
theorem iteratedDerivWithin_const_add (hn : 0 < n) (c : F) :
    iteratedDerivWithin n (fun z => c + f z) s x = iteratedDerivWithin n f s x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
hn : 0 < n
c : F
⊢ iteratedDerivWithin n (fun z => c + f z) s x = iteratedDerivWithin n f s x

Tactic:
obtain ⟨n, rfl⟩ := n.exists_eq_succ_of_ne_zero hn.ne'

Result:
case intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
⊢ iteratedDerivWithin n.succ (fun z => c + f z) s x = iteratedDerivWithin n.succ f s x

Proof state:
case intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
⊢ iteratedDerivWithin n.succ (fun z => c + f z) s x = iteratedDerivWithin n.succ f s x

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case intro.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ iteratedDerivWithin n.succ (fun z => c + f z) s x = iteratedDerivWithin n.succ f s x

case intro.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
hxs : nhdsWithin x (s \ {x}) = ⊥
⊢ iteratedDerivWithin n.succ (fun z => c + f z) s x = iteratedDerivWithin n.succ f s x

Proof state:
case intro.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
hxs : nhdsWithin x (s \ {x}) = ⊥
⊢ iteratedDerivWithin n.succ (fun z => c + f z) s x = iteratedDerivWithin n.succ f s x

Tactic:
simp [iteratedDerivWithin_succ, derivWithin_zero_of_isolated hxs]

Result:
no goals

Proof state:
case intro.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ iteratedDerivWithin n.succ (fun z => c + f z) s x = iteratedDerivWithin n.succ f s x

Tactic:
rw [iteratedDerivWithin_succ', iteratedDerivWithin_succ']

Result:
case intro.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ iteratedDerivWithin n (derivWithin (fun z => c + f z) s) s x = iteratedDerivWithin n (derivWithin f s) s x

Proof state:
case intro.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ iteratedDerivWithin n.succ (fun z => c + f z) s x = iteratedDerivWithin n.succ f s x

case intro.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
hxs : nhdsWithin x (s \ {x}) = ⊥
⊢ iteratedDerivWithin n.succ (fun z => c + f z) s x = iteratedDerivWithin n.succ f s x

Tactic:
swap

Result:
case intro.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
hxs : nhdsWithin x (s \ {x}) = ⊥
⊢ iteratedDerivWithin n.succ (fun z => c + f z) s x = iteratedDerivWithin n.succ f s x

case intro.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ iteratedDerivWithin n.succ (fun z => c + f z) s x = iteratedDerivWithin n.succ f s x

Proof state:
case intro.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ iteratedDerivWithin n (derivWithin (fun z => c + f z) s) s x = iteratedDerivWithin n (derivWithin f s) s x

Tactic:
congr with y

Result:
case intro.inl.e_f.h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
hxs : UniqueDiffWithinAt 𝕜 s x
y : 𝕜
⊢ derivWithin (fun z => c + f z) s y = derivWithin f s y

Proof state:
case intro.inl.e_f.h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
hxs : UniqueDiffWithinAt 𝕜 s x
y : 𝕜
⊢ derivWithin (fun z => c + f z) s y = derivWithin f s y

Tactic:
exact derivWithin_const_add _

Result:
no goals