awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
y : F
x : E
hg : ContDiffWithinAt 𝕜 n g t y
hf : ContDiffWithinAt 𝕜 n f s x
hs : t ∈ 𝓝[f '' s] f x
hy : f x = y
⊢ ContDiffWithinAt 𝕜 n g t (f x)

Tactic:
subst hy
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 n f s x
hs : t ∈ 𝓝[f '' s] f x
hg : ContDiffWithinAt 𝕜 n g t (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
hg.comp_of_mem_nhdsWithin_image x hf hs

Premises used: ContDiffWithinAt.comp_of_mem_nhdsWithin_image
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 n f s x
hs : t ∈ 𝓝[f '' s] f x
hg : ContDiffWithinAt 𝕜 n g t (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
exact hg.comp_of_mem_nhdsWithin_image x hf hs

Premises used: ContDiffWithinAt.comp_of_mem_nhdsWithin_image
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) (s ∩ f ⁻¹' t) x

Tactic:
hg.comp x (hf.mono inter_subset_left) inter_subset_right

Premises used: ContDiffWithinAt.comp, Set.inter_subset_left, Set.inter_subset_right, ContDiffWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
y : F
x : E
hg : ContDiffWithinAt 𝕜 n g t y
hf : ContDiffWithinAt 𝕜 n f s x
hy : f x = y
⊢ ContDiffWithinAt 𝕜 n g t (f x)

Tactic:
subst hy
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g t (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) (s ∩ f ⁻¹' t) x

Tactic:
hg.comp_inter x hf

Premises used: ContDiffWithinAt.comp_inter
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g t (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) (s ∩ f ⁻¹' t) x

Tactic:
exact hg.comp_inter x hf

Premises used: ContDiffWithinAt.comp_inter
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
hs : f ⁻¹' t ∈ 𝓝[s] x
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
(hg.comp_inter x hf).mono_of_mem_nhdsWithin (inter_mem self_mem_nhdsWithin hs)

Premises used: ContDiffWithinAt.mono_of_mem_nhdsWithin, Filter.inter_mem, self_mem_nhdsWithin, ContDiffWithinAt.comp_inter
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
y : F
x : E
hg : ContDiffWithinAt 𝕜 n g t y
hf : ContDiffWithinAt 𝕜 n f s x
hs : f ⁻¹' t ∈ 𝓝[s] x
hy : f x = y
⊢ ContDiffWithinAt 𝕜 n g t (f x)

Tactic:
subst hy
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 n f s x
hs : f ⁻¹' t ∈ 𝓝[s] x
hg : ContDiffWithinAt 𝕜 n g t (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
hg.comp_of_preimage_mem_nhdsWithin x hf hs

Premises used: ContDiffWithinAt.comp_of_preimage_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 n f s x
hs : f ⁻¹' t ∈ 𝓝[s] x
hg : ContDiffWithinAt 𝕜 n g t (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
exact hg.comp_of_preimage_mem_nhdsWithin x hf hs

Premises used: ContDiffWithinAt.comp_of_preimage_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
g : F → G
n : ℕ∞ω
x : E
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffWithinAt 𝕜 n f s x
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
hg.comp x hf (mapsTo_univ _ _)

Premises used: Set.mapsTo_univ, ContDiffWithinAt.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
g : F → G
n : ℕ∞ω
y : F
x : E
hg : ContDiffAt 𝕜 n g y
hf : ContDiffWithinAt 𝕜 n f s x
hy : f x = y
⊢ ContDiffAt 𝕜 n g (f x)

Tactic:
subst hy
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
g : F → G
n : ℕ∞ω
x : E
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffAt 𝕜 n g (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
hg.comp_contDiffWithinAt x hf

Premises used: ContDiffAt.comp_contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
g : F → G
n : ℕ∞ω
x : E
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffAt 𝕜 n g (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
exact hg.comp_contDiffWithinAt x hf

Premises used: ContDiffAt.comp_contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
g : F → G
n : ℕ∞ω
x : E
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
⊢ ContDiffAt 𝕜 n (g ∘ f) x

Tactic:
hg.comp x hf (mapsTo_univ _ _)

Premises used: ContDiffAt, Set.mapsTo_univ, ContDiffWithinAt.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
g : F → G
n : ℕ∞ω
x : E
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
⊢ ContDiffAt.{u_1, u_2, u_4} 𝕜 (F := G) n (fun (x : E) ↦ g (f x)) x

Tactic:
hg.comp x hf

Premises used: ContDiffAt.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
t : Set E
x : E
n : ℕ∞ω
g : F → G
f : E → F
h : ContDiff 𝕜 n g
hf : ContDiffWithinAt 𝕜 n f t x
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) t x

Tactic:
haveI : ContDiffWithinAt 𝕜 n g univ (f x) := h.contDiffAt.contDiffWithinAt
  this.comp x hf (subset_univ _)

Premises used: Set.subset_univ, ContDiffWithinAt.comp, ContDiffAt.contDiffWithinAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
g : F → G
f : E → F
x : E
hg : ContDiff 𝕜 n g
hf : ContDiffAt 𝕜 n f x
⊢ ContDiffAt 𝕜 n (g ∘ f) x

Tactic:
hg.comp_contDiffWithinAt hf

Premises used: ContDiff.comp_contDiffWithinAt, ContDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
g : F → G
x : E
n : ℕ∞ω
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
⊢ f x ∈ t

Tactic:
have hxt : f x ∈ t := hst.self_of_nhdsWithin hxs
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
g : F → G
x : E
n : ℕ∞ω
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
hxt : f x ∈ t
⊢ Tendsto f (𝓝[s] x) (𝓝[t] f x)

Tactic:
have hf_tendsto : Tendsto f (𝓝[s] x) (𝓝[t] (f x)) :=
      tendsto_nhdsWithin_iff.mpr ⟨hf.continuousWithinAt, hst⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
g : F → G
x : E
n : ℕ∞ω
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
hxt : f x ∈ t
hf_tendsto : Tendsto f (𝓝[s] x) (𝓝[t] f x)
⊢ ∀ᶠ (u : Set E) in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) u

Tactic:
have H₁ : ∀ᶠ u in (𝓝[s] x).smallSets,
        HasFTaylorSeriesUpToOn i f (ftaylorSeriesWithin 𝕜 f s) u :=
      hf.eventually_hasFTaylorSeriesUpToOn hs hxs hi
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
g : F → G
x : E
n : ℕ∞ω
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
hxt : f x ∈ t
hf_tendsto : Tendsto f (𝓝[s] x) (𝓝[t] f x)
H₁ : ∀ᶠ (u : Set E) in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) u
⊢ ∀ᶠ (u : Set E) in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) g (ftaylorSeriesWithin 𝕜 g t) (f '' u)

Tactic:
have H₂ : ∀ᶠ u in (𝓝[s] x).smallSets,
        HasFTaylorSeriesUpToOn i g (ftaylorSeriesWithin 𝕜 g t) (f '' u) :=
      hf_tendsto.image_smallSets.eventually (hg.eventually_hasFTaylorSeriesUpToOn ht hxt hi)
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
g : F → G
x : E
n : ℕ∞ω
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
hxt : f x ∈ t
hf_tendsto : Tendsto f (𝓝[s] x) (𝓝[t] f x)
H₁ : ∀ᶠ (u : Set E) in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) u
H₂ : ∀ᶠ (u : Set E) in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) g (ftaylorSeriesWithin 𝕜 g t) (f '' u)
rcases :
  ∀ (u : Set E)
    (hu :
      ∀ ⦃x : Set E⦄,
        x ∈ 𝒫 (u ∩ s) →
          HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) x ∧
            HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) g (ftaylorSeriesWithin 𝕜 g t) (f '' x))
    (hxu : x ∈ u) (huo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u),
    ∃ (u : Set E),
      x ∈ u ∧
        IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧
          HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ u) ∧
            HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) g (ftaylorSeriesWithin 𝕜 g t) (f '' (s ∩ u))
⊢ ∃ (u : Set E),
    x ∈ u ∧
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧
        HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ u) ∧
          HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) g (ftaylorSeriesWithin 𝕜 g t) (f '' (s ∩ u))

Tactic:
rcases (nhdsWithin_basis_open _ _).smallSets.eventually_iff.mp (H₁.and H₂)
      with ⟨u, ⟨hxu, huo⟩, hu⟩

Premises used: nhdsWithin_basis_open, Filter.Eventually.and, Filter.HasBasis.smallSets, Iff.mp, Filter.HasBasis.eventually_iff
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
g : F → G
x : E
n : ℕ∞ω
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
hxt : f x ∈ t
hf_tendsto : Tendsto f (𝓝[s] x) (𝓝[t] f x)
H₁ : ∀ᶠ (u : Set E) in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) u
H₂ : ∀ᶠ (u : Set E) in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) g (ftaylorSeriesWithin 𝕜 g t) (f '' u)
u : Set E
hu :
  ∀ ⦃x : Set E⦄,
    x ∈ 𝒫 (u ∩ s) →
      HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) x ∧
        HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) g (ftaylorSeriesWithin 𝕜 g t) (f '' x)
hxu : x ∈ u
huo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
⊢ s ∩ u ∈ 𝒫 (u ∩ s)

Tactic:
simp [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
g : F → G
x : E
n : ℕ∞ω
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
hxt : f x ∈ t
hf_tendsto : Tendsto f (𝓝[s] x) (𝓝[t] f x)
H₁ : ∀ᶠ (u : Set E) in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) u
H₂ : ∀ᶠ (u : Set E) in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) g (ftaylorSeriesWithin 𝕜 g t) (f '' u)
u : Set E
hu :
  ∀ ⦃x : Set E⦄,
    x ∈ 𝒫 (u ∩ s) →
      HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) x ∧
        HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) g (ftaylorSeriesWithin 𝕜 g t) (f '' x)
hxu : x ∈ u
huo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
⊢ ∃ (u : Set E),
    x ∈ u ∧
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧
        HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ u) ∧
          HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) g (ftaylorSeriesWithin 𝕜 g t) (f '' (s ∩ u))

Tactic:
exact ⟨u, hxu, huo, hu (by simp [inter_comm])⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
g : F → G
x : E
n : ℕ∞ω
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
obtain :
  ∀ (u : Set E) (hxu : x ∈ u) (huo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u)
    (hfu : HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ u))
    (hgu : HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) g (ftaylorSeriesWithin 𝕜 g t) (f '' (s ∩ u))),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
      (iteratedFDerivWithin 𝕜 i (g ∘ f) s x)
      (FormalMultilinearSeries.taylorComp (ftaylorSeriesWithin 𝕜 g t (f x)) (ftaylorSeriesWithin 𝕜 f s x) i)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) (iteratedFDerivWithin 𝕜 i (g ∘ f) s x)
    (FormalMultilinearSeries.taylorComp (ftaylorSeriesWithin 𝕜 g t (f x)) (ftaylorSeriesWithin 𝕜 f s x) i)

Tactic:
obtain ⟨u, hxu, huo, hfu, hgu⟩ : ∃ u, x ∈ u ∧ IsOpen u ∧
      HasFTaylorSeriesUpToOn i f (ftaylorSeriesWithin 𝕜 f s) (s ∩ u) ∧
      HasFTaylorSeriesUpToOn i g (ftaylorSeriesWithin 𝕜 g t) (f '' (s ∩ u)) := by
    have hxt : f x ∈ t := hst.self_of_nhdsWithin hxs
    have hf_tendsto : Tendsto f (𝓝[s] x) (𝓝[t] (f x)) :=
      tendsto_nhdsWithin_iff.mpr ⟨hf.continuousWithinAt, hst⟩
    have H₁ : ∀ᶠ u in (𝓝[s] x).smallSets,
        HasFTaylorSeriesUpToOn i f (ftaylorSeriesWithin 𝕜 f s) u :=
      hf.eventually_hasFTaylorSeriesUpToOn hs hxs hi
    have H₂ : ∀ᶠ u in (𝓝[s] x).smallSets,
        HasFTaylorSeriesUpToOn i g (ftaylorSeriesWithin 𝕜 g t) (f '' u) :=
      hf_tendsto.image_smallSets.eventually (hg.eventually_hasFTaylorSeriesUpToOn ht hxt hi)
    rcases (nhdsWithin_basis_open _ _).smallSets.eventually_iff.mp (H₁.and H₂)
      with ⟨u, ⟨hxu, huo⟩, hu⟩
    exact ⟨u, hxu, huo, hu (by simp [inter_comm])⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
g : F → G
x : E
n : ℕ∞ω
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
u : Set E
hxu : x ∈ u
huo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hfu : HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ u)
hgu : HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) g (ftaylorSeriesWithin 𝕜 g t) (f '' (s ∩ u))
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) (iteratedFDerivWithin 𝕜 i (g ∘ f) s x)
    (FormalMultilinearSeries.taylorComp (ftaylorSeriesWithin 𝕜 g t (f x)) (ftaylorSeriesWithin 𝕜 f s x) i)

Tactic:
.symm <| (hgu.comp hfu (mapsTo_image _ _)).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl
    (hs.inter huo) ⟨hxs, hxu⟩ |>.trans <| iteratedFDerivWithin_inter_open huo hxu

Premises used: le_rfl, Set.mapsTo_image, HasFTaylorSeriesUpToOn.comp, And.intro, HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn, iteratedFDerivWithin_inter_open, UniqueDiffOn.inter, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
g : F → G
x : E
n : ℕ∞ω
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
u : Set E
hxu : x ∈ u
huo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hfu : HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ u)
hgu : HasFTaylorSeriesUpToOn (↑i : ℕ∞ω) g (ftaylorSeriesWithin 𝕜 g t) (f '' (s ∩ u))
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) (iteratedFDerivWithin 𝕜 i (g ∘ f) s x)
    (FormalMultilinearSeries.taylorComp (ftaylorSeriesWithin 𝕜 g t (f x)) (ftaylorSeriesWithin 𝕜 f s x) i)

Tactic:
exact .symm <| (hgu.comp hfu (mapsTo_image _ _)).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl
    (hs.inter huo) ⟨hxs, hxu⟩ |>.trans <| iteratedFDerivWithin_inter_open huo hxu

Premises used: le_rfl, Set.mapsTo_image, HasFTaylorSeriesUpToOn.comp, And.intro, HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn, iteratedFDerivWithin_inter_open, UniqueDiffOn.inter, Eq.trans