-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem ContDiffWithinAt.contDiffOn' (hm : m ≤ n) (h' : m = ∞ → n = ω)
    (h : ContDiffWithinAt 𝕜 n f s x) :
    ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 m f (insert x s ∩ u)

Proof state:
case inl.intro.intro.intro.intro.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
m : WithTop ℕ∞
hm : m ≤ ω
h' : m = ∞ → ω = ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p t
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) t
u : Set E
huo : IsOpen u
hxu : x ∈ u
hut : u ∩ insert x s ⊆ t
⊢ ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 m f (insert x s ∩ u)

Tactic:
rw [inter_comm] at hut

Result:
case inl.intro.intro.intro.intro.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
m : WithTop ℕ∞
hm : m ≤ ω
h' : m = ∞ → ω = ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p t
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) t
u : Set E
huo : IsOpen u
hxu : x ∈ u
hut : insert x s ∩ u ⊆ t
⊢ ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 m f (insert x s ∩ u)

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
m✝ n : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 n f s x
hn : n ≠ ω
m : ℕ
hm : ↑m ≤ n
h' : ↑m = ∞ → n = ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m) f p t
⊢ ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 (↑m) f (insert x s ∩ u)

Tactic:
rcases mem_nhdsWithin.1 ht with ⟨u, huo, hxu, hut⟩

Result:
case intro.intro.intro.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
m✝ n : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 n f s x
hn : n ≠ ω
m : ℕ
hm : ↑m ≤ n
h' : ↑m = ∞ → n = ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m) f p t
u : Set E
huo : IsOpen u
hxu : x ∈ u
hut : u ∩ insert x s ⊆ t
⊢ ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 (↑m) f (insert x s ∩ u)

Proof state:
case inl.intro.intro.intro.intro.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
m : WithTop ℕ∞
hm : m ≤ ω
h' : m = ∞ → ω = ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p t
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) t
u : Set E
huo : IsOpen u
hxu : x ∈ u
hut : insert x s ∩ u ⊆ t
y : E
hy : y ∈ insert x s ∩ u
⊢ ContDiffWithinAt 𝕜 ω f (insert x s ∩ u) y

Tactic:
refine ⟨insert x s ∩ u, ?_, p, hp.mono hut,  fun i ↦ (h'p i).mono hut⟩

Result:
case inl.intro.intro.intro.intro.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
m : WithTop ℕ∞
hm : m ≤ ω
h' : m = ∞ → ω = ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p t
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) t
u : Set E
huo : IsOpen u
hxu : x ∈ u
hut : insert x s ∩ u ⊆ t
y : E
hy : y ∈ insert x s ∩ u
⊢ insert x s ∩ u ∈ 𝓝[insert y (insert x s ∩ u)] y

Proof state:
case inl.intro.intro.intro.intro.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
m : WithTop ℕ∞
hm : m ≤ ω
h' : m = ∞ → ω = ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p t
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) t
u : Set E
huo : IsOpen u
hxu : x ∈ u
hut : insert x s ∩ u ⊆ t
⊢ ContDiffOn 𝕜 ω f (insert x s ∩ u)

Tactic:
intro y hy

Result:
case inl.intro.intro.intro.intro.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
m : WithTop ℕ∞
hm : m ≤ ω
h' : m = ∞ → ω = ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p t
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) t
u : Set E
huo : IsOpen u
hxu : x ∈ u
hut : insert x s ∩ u ⊆ t
y : E
hy : y ∈ insert x s ∩ u
⊢ ContDiffWithinAt 𝕜 ω f (insert x s ∩ u) y

Proof state:
case inl.intro.intro.intro.intro.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
m : WithTop ℕ∞
hm : m ≤ ω
h' : m = ∞ → ω = ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p t
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) t
u : Set E
huo : IsOpen u
hxu : x ∈ u
hut : insert x s ∩ u ⊆ t
⊢ ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 m f (insert x s ∩ u)

Tactic:
refine ⟨u, huo, hxu, ?_⟩

Result:
case inl.intro.intro.intro.intro.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
m : WithTop ℕ∞
hm : m ≤ ω
h' : m = ∞ → ω = ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p t
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) t
u : Set E
huo : IsOpen u
hxu : x ∈ u
hut : insert x s ∩ u ⊆ t
⊢ ContDiffOn 𝕜 m f (insert x s ∩ u)

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
m n : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 n f s x
hn : n ≠ ω
hm : ω ≤ n
h' : ω = ∞ → n = ω
⊢ ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 ω f (insert x s ∩ u)

Tactic:
simp [hn] at hm

Result:
no goals

Proof state:
case inl.intro.intro.intro.intro.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
m : WithTop ℕ∞
hm : m ≤ ω
h' : m = ∞ → ω = ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p t
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) t
u : Set E
huo : IsOpen u
hxu : x ∈ u
hut : insert x s ∩ u ⊆ t
⊢ ContDiffOn 𝕜 m f (insert x s ∩ u)

Tactic:
suffices ContDiffOn 𝕜 ω f (insert x s ∩ u) from this.of_le le_top

Result:
case inl.intro.intro.intro.intro.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
m : WithTop ℕ∞
hm : m ≤ ω
h' : m = ∞ → ω = ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p t
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) t
u : Set E
huo : IsOpen u
hxu : x ∈ u
hut : insert x s ∩ u ⊆ t
⊢ ContDiffOn 𝕜 ω f (insert x s ∩ u)