-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem ContDiffWithinAt.mono_of_mem_nhdsWithin (h : ContDiffWithinAt 𝕜 n f s x) {t : Set E}
    (hst : s ∈ 𝓝[t] x) : ContDiffWithinAt 𝕜 n f t x

Proof state:
case 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
n : WithTop ℕ∞
t : Set E
hst : s ∈ 𝓝[t] x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn ω f p u
H' : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
⊢ ContDiffWithinAt 𝕜 ω f t x

Tactic:
exact ⟨u, nhdsWithin_le_of_mem (insert_mem_nhdsWithin_insert hst) hu, p, H, H'⟩

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 : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 n f s x
t : Set E
hst : s ∈ 𝓝[t] x
⊢ ContDiffWithinAt 𝕜 n f t x

Tactic:
match n with
| ω =>
  obtain ⟨u, hu, p, H, H'⟩ := h
  exact ⟨u, nhdsWithin_le_of_mem (insert_mem_nhdsWithin_insert hst) hu, p, H, H'⟩
| (n : ℕ∞) =>
  intro m hm
  rcases h m hm with ⟨u, hu, p, H⟩
  exact ⟨u, nhdsWithin_le_of_mem (insert_mem_nhdsWithin_insert hst) hu, p, H⟩

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✝ : WithTop ℕ∞
t : Set E
hst : s ∈ 𝓝[t] x
n : ℕ∞
h : ContDiffWithinAt 𝕜 (↑n) f s x
m : ℕ
hm : ↑m ≤ n
⊢ ∃ u ∈ 𝓝[insert x t] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u

Tactic:
rcases h m hm with ⟨u, hu, p, H⟩

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✝ : WithTop ℕ∞
t : Set E
hst : s ∈ 𝓝[t] x
n : ℕ∞
h : ContDiffWithinAt 𝕜 (↑n) f s x
m : ℕ
hm : ↑m ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn (↑m) f p u
⊢ ∃ u ∈ 𝓝[insert x t] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p 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
n : WithTop ℕ∞
t : Set E
hst : s ∈ 𝓝[t] x
h : ContDiffWithinAt 𝕜 ω f s x
⊢ ContDiffWithinAt 𝕜 ω f t x

Tactic:
obtain ⟨u, hu, p, H, H'⟩ := h

Result:
case 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
n : WithTop ℕ∞
t : Set E
hst : s ∈ 𝓝[t] x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn ω f p u
H' : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
⊢ ContDiffWithinAt 𝕜 ω f t 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✝ : WithTop ℕ∞
t : Set E
hst : s ∈ 𝓝[t] x
n : ℕ∞
h : ContDiffWithinAt 𝕜 (↑n) f s x
⊢ ContDiffWithinAt 𝕜 (↑n) f t x

Tactic:
intro m hm

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✝ : WithTop ℕ∞
t : Set E
hst : s ∈ 𝓝[t] x
n : ℕ∞
h : ContDiffWithinAt 𝕜 (↑n) f s x
m : ℕ
hm : ↑m ≤ n
⊢ ∃ u ∈ 𝓝[insert x t] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p 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
n✝ : WithTop ℕ∞
t : Set E
hst : s ∈ 𝓝[t] x
n : ℕ∞
h : ContDiffWithinAt 𝕜 (↑n) f s x
m : ℕ
hm : ↑m ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn (↑m) f p u
⊢ ∃ u ∈ 𝓝[insert x t] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u

Tactic:
exact ⟨u, nhdsWithin_le_of_mem (insert_mem_nhdsWithin_insert hst) hu, p, H⟩

Result:
no goals