-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem iteratedFDerivWithin_of_isOpen (n : ℕ) (hs : IsOpen s) :
    EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s

Proof state:
case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s) x =
    (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 n f)) x

Tactic:
dsimp

Result:
case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ (continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x) =
    (continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x)

Proof state:
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ ∀ a ∈ s, iteratedFDerivWithin 𝕜 n f s a = iteratedFDeriv 𝕜 n f a

Tactic:
exact IH

Result:
no goals

Proof state:
case succ.h.e_6.h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x = fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x

Tactic:
rw [fderivWithin_of_isOpen hs hx]

Result:
case succ.h.e_6.h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ fderiv 𝕜 (iteratedFDerivWithin 𝕜 n f s) x = fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x

Proof state:
case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
⊢ EqOn (iteratedFDerivWithin 𝕜 (n + 1) f s) (iteratedFDeriv 𝕜 (n + 1) f) s

Tactic:
intro x hx

Result:
case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 (n + 1) f s x = iteratedFDeriv 𝕜 (n + 1) f x

Proof state:
case zero.H
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
x : E
a✝ : x ∈ s
x✝ : Fin 0 → E
⊢ (iteratedFDerivWithin 𝕜 0 f s x) x✝ = (iteratedFDeriv 𝕜 0 f x) x✝

Tactic:
simp only [iteratedFDerivWithin_zero_apply, iteratedFDeriv_zero_apply]

Result:
no goals

Proof state:
case zero
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
⊢ EqOn (iteratedFDerivWithin 𝕜 0 f s) (iteratedFDeriv 𝕜 0 f) s

Tactic:
intro x _

Result:
case zero
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
x : E
a✝ : x ∈ s
⊢ iteratedFDerivWithin 𝕜 0 f s x = iteratedFDeriv 𝕜 0 f x

Proof state:
case succ.h.e_6.h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ fderiv 𝕜 (iteratedFDerivWithin 𝕜 n f s) x = fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x

Tactic:
apply Filter.EventuallyEq.fderiv_eq

Result:
case succ.h.e_6.h.h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 n f s =ᶠ[𝓝 x] iteratedFDeriv 𝕜 n f

Proof state:
case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ (continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x) =
    (continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x)

Tactic:
congr 1

Result:
case succ.h.e_6.h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x = fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x

Proof state:
case zero
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
x : E
a✝ : x ∈ s
⊢ iteratedFDerivWithin 𝕜 0 f s x = iteratedFDeriv 𝕜 0 f x

Tactic:
ext1

Result:
case zero.H
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
x : E
a✝ : x ∈ s
x✝ : Fin 0 → E
⊢ (iteratedFDerivWithin 𝕜 0 f s x) x✝ = (iteratedFDeriv 𝕜 0 f x) x✝

Proof state:
case succ.h.e_6.h.h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 n f s =ᶠ[𝓝 x] iteratedFDeriv 𝕜 n f

Tactic:
filter_upwards [hs.mem_nhds hx]

Result:
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ ∀ a ∈ s, iteratedFDerivWithin 𝕜 n f s a = iteratedFDeriv 𝕜 n f a