-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem iteratedFDerivWithin_eq_iteratedFDeriv {n : ℕ}
    (hs : UniqueDiffOn 𝕜 s) (h : ContDiffAt 𝕜 n f x) (hx : x ∈ s) :
    iteratedFDerivWithin 𝕜 n f s x = iteratedFDeriv 𝕜 n f x

Proof state:
𝕜 : 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n) f x
hx : x ∈ s
⊢ ↑n = ∞ → ↑n = ω

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n) f x
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f univ x

Tactic:
rcases h.contDiffOn' le_rfl (by simp) with ⟨u, u_open, xu, hu⟩

Result:
case intro.intro.intro
𝕜 : 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n) f x
hx : x ∈ s
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n) f (insert x univ ∩ u)
⊢ iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f univ x

Proof state:
case intro.intro.intro.ht
𝕜 : 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n) f x
hx : x ∈ s
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n) f (insert x univ ∩ u)
⊢ UniqueDiffOn 𝕜 (univ ∩ u)

Tactic:
apply uniqueDiffOn_univ.inter u_open

Result:
no goals

Proof state:
case intro.intro.intro.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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n) f x
hx : x ∈ s
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n) f (insert x univ ∩ u)
⊢ ContDiffOn 𝕜 (↑n) f (univ ∩ u)

Tactic:
simpa using hu

Result:
no goals

Proof state:
case intro.intro.intro
𝕜 : 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n) f x
hx : x ∈ s
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n) f (insert x univ ∩ u)
⊢ iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f (univ ∩ u) x

Tactic:
apply iteratedFDerivWithin_subset

Result:
case intro.intro.intro.st
𝕜 : 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n) f x
hx : x ∈ s
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n) f (insert x univ ∩ u)
⊢ s ∩ u ⊆ univ ∩ u

case intro.intro.intro.hs
𝕜 : 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n) f x
hx : x ∈ s
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n) f (insert x univ ∩ u)
⊢ UniqueDiffOn 𝕜 (s ∩ u)

case intro.intro.intro.ht
𝕜 : 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n) f x
hx : x ∈ s
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n) f (insert x univ ∩ u)
⊢ UniqueDiffOn 𝕜 (univ ∩ u)

case intro.intro.intro.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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n) f x
hx : x ∈ s
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n) f (insert x univ ∩ u)
⊢ ContDiffOn 𝕜 (↑n) f (univ ∩ u)

case intro.intro.intro.hx
𝕜 : 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n) f x
hx : x ∈ s
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n) f (insert x univ ∩ u)
⊢ x ∈ s ∩ u

Proof state:
case intro.intro.intro.st
𝕜 : 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n) f x
hx : x ∈ s
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n) f (insert x univ ∩ u)
⊢ s ∩ u ⊆ univ ∩ u

Tactic:
exact inter_subset_inter_left _ (subset_univ _)

Result:
no goals

Proof state:
case intro.intro.intro.hx
𝕜 : 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n) f x
hx : x ∈ s
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n) f (insert x univ ∩ u)
⊢ x ∈ s ∩ u

Tactic:
exact ⟨hx, xu⟩

Result:
no goals

Proof state:
case intro.intro.intro.hs
𝕜 : 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n) f x
hx : x ∈ s
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n) f (insert x univ ∩ u)
⊢ UniqueDiffOn 𝕜 (s ∩ u)

Tactic:
exact hs.inter u_open

Result:
no goals

Proof state:
𝕜 : 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n) f x
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 n f s x = iteratedFDeriv 𝕜 n f x

Tactic:
rw [← iteratedFDerivWithin_univ]

Result:
𝕜 : 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n) f x
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f univ x