case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type ?u.85634
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝¹ x✝ : 𝕜
hs : UniqueDiffOn 𝕜 s
hx✝ : x✝ ∈ s
x : 𝕜
hx : x ∈ s
⊢ iteratedDerivWithin Nat.zero f s x = ((fun g => derivWithin g s)^[Nat.zero]) f x

case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type ?u.85634
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝¹ x✝ : 𝕜
hs : UniqueDiffOn 𝕜 s
hx✝ : x✝ ∈ s
n : ℕ
IH : ∀ {x : 𝕜}, x ∈ s → iteratedDerivWithin n f s x = ((fun g => derivWithin g s)^[n]) f x
x : 𝕜
hx : x ∈ s
⊢ iteratedDerivWithin (Nat.succ n) f s x = ((fun g => derivWithin g s)^[Nat.succ n]) f x
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type ?u.85634
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ iteratedDerivWithin n f s x = ((fun g => derivWithin g s)^[n]) f x
induction' n with n IH generalizing x
no goals
case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type ?u.85634
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝¹ x✝ : 𝕜
hs : UniqueDiffOn 𝕜 s
hx✝ : x✝ ∈ s
x : 𝕜
hx : x ∈ s
⊢ iteratedDerivWithin Nat.zero f s x = ((fun g => derivWithin g s)^[Nat.zero]) f x
simp
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type ?u.85634
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝¹ x✝ : 𝕜
hs : UniqueDiffOn 𝕜 s
hx✝ : x✝ ∈ s
n : ℕ
IH : ∀ {x : 𝕜}, x ∈ s → iteratedDerivWithin n f s x = ((fun g => derivWithin g s)^[n]) f x
x : 𝕜
hx : x ∈ s
⊢ derivWithin (iteratedDerivWithin n f s) s x = ((fun g => derivWithin g s) ∘ (fun g => derivWithin g s)^[n]) f x
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type ?u.85634
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝¹ x✝ : 𝕜
hs : UniqueDiffOn 𝕜 s
hx✝ : x✝ ∈ s
n : ℕ
IH : ∀ {x : 𝕜}, x ∈ s → iteratedDerivWithin n f s x = ((fun g => derivWithin g s)^[n]) f x
x : 𝕜
hx : x ∈ s
⊢ iteratedDerivWithin (Nat.succ n) f s x = ((fun g => derivWithin g s)^[Nat.succ n]) f x
rw [iteratedDerivWithin_succ (hs x hx), Function.iterate_succ']
no goals
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type ?u.85634
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝¹ x✝ : 𝕜
hs : UniqueDiffOn 𝕜 s
hx✝ : x✝ ∈ s
n : ℕ
IH : ∀ {x : 𝕜}, x ∈ s → iteratedDerivWithin n f s x = ((fun g => derivWithin g s)^[n]) f x
x : 𝕜
hx : x ∈ s
⊢ derivWithin (iteratedDerivWithin n f s) s x = ((fun g => derivWithin g s) ∘ (fun g => derivWithin g s)^[n]) f x
exact derivWithin_congr (fun y hy => IH hy) (IH hx)