awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →ᴬ[𝕜] E
A : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F →
    ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F :=
  fun (m : ℕ) (h : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F) ↦
    h.compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E) fun (x : Fin m) ↦ g.contLinear
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F)
    (fun (x : G) ↦
      (p ((g : (a : G) → E) x) m).compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E)
        fun (x : Fin m) ↦ g.contLinear)
    ((⇑g : (a : G) → E) ⁻¹' s)

Tactic:
(hA m).continuous.comp_continuousOn <| (hf.cont m hm).comp g.continuous.continuousOn <|
      Subset.refl _

Premises used: Continuous.continuousOn, Set.Subset.refl, Continuous.comp_continuousOn, IsBoundedLinearMap.continuous, HasFTaylorSeriesUpToOn.cont, ContinuousOn.comp, ContinuousMultilinearMap.compContinuousLinearMap, ContinuousAffineMap.continuous
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →ᴬ[𝕜] E
A : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F →
    ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F :=
  fun (m : ℕ) (h : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F) ↦
    h.compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E) fun (x : Fin m) ↦ g.contLinear
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F)
    (fun (x : G) ↦
      (p ((g : (a : G) → E) x) m).compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E)
        fun (x : Fin m) ↦ g.contLinear)
    ((⇑g : (a : G) → E) ⁻¹' s)

Tactic:
exact (hA m).continuous.comp_continuousOn <| (hf.cont m hm).comp g.continuous.continuousOn <|
      Subset.refl _

Premises used: Continuous.continuousOn, Set.Subset.refl, Continuous.comp_continuousOn, IsBoundedLinearMap.continuous, HasFTaylorSeriesUpToOn.cont, ContinuousOn.comp, ContinuousAffineMap.continuous
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →L[𝕜] E
⊢ HasFTaylorSeriesUpToOn.{u_1, u_4, u_3} (𝕜 := 𝕜) n (f ∘ (⇑g : (a : G) → E))
    (fun (x : G) (k : ℕ) ↦
      (p ((g : (a : G) → E) x) k).compContinuousLinearMap (M₁ := fun (i : Fin k) ↦ G) (M₁' := fun (i : Fin k) ↦ E)
        fun (x : Fin k) ↦ g)
    ((⇑g : (a : G) → E) ⁻¹' s)

Tactic:
hf.comp_continuousAffineMap g.toContinuousAffineMap

Premises used: ContinuousAffineMap.contLinear, ContinuousLinearMap.toContinuousAffineMap, HasFTaylorSeriesUpToOn.comp_continuousAffineMap
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n : ℕ∞ω
x : G
g : G →L[𝕜] E
hf : ContDiffWithinAt 𝕜 ω f s ((g : (a : G) → E) x)
obtain :
  ∀ (u : Set E)
    (hu :
      Membership.mem (γ := Filter E) (𝓝[insert (α := E) ((g : (a : G) → E) x : E) s] (g : (a : G) → E) x : Filter E) u)
    (p : E → FormalMultilinearSeries 𝕜 E F) (hp : HasFTaylorSeriesUpToOn ω f p u)
    (h'p :
      ∀ (i : ℕ),
        AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i)
          u),
    ContDiffWithinAt 𝕜 ω (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x
⊢ ContDiffWithinAt 𝕜 ω (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x

Tactic:
obtain ⟨u, hu, p, hp, h'p⟩ := hf
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n : ℕ∞ω
x : G
g : G →L[𝕜] E
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝[insert (α := E) ((g : (a : G) → E) x : E) s] (g : (a : G) → E) x : Filter E) u
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
⊢ ContDiffWithinAt 𝕜 ω (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x

Tactic:
⟨g ⁻¹' u, ?_, _, hp.compContinuousLinearMap g, ?_⟩

Premises used: HasFTaylorSeriesUpToOn.compContinuousLinearMap, Set.preimage, And.intro, Exists.intro, ContDiffWithinAt, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n : ℕ∞ω
x : G
g : G →L[𝕜] E
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝[insert (α := E) ((g : (a : G) → E) x : E) s] (g : (a : G) → E) x : Filter E) u
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
refine_1 : (⇑g : (a : G) → E) ⁻¹' u ∈ 𝓝[insert x ((⇑g : (a : G) → E) ⁻¹' s)] x
refine_2 :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
      (fun (x : G) ↦
        (p ((g : (a : G) → E) x) i).compContinuousLinearMap (M₁ := fun (i : Fin i) ↦ G) (M₁' := fun (i : Fin i) ↦ E)
          fun (x : Fin i) ↦ g)
      ((⇑g : (a : G) → E) ⁻¹' u)
⊢ ContDiffWithinAt 𝕜 ω (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x

Tactic:
refine ⟨g ⁻¹' u, ?_, _, hp.compContinuousLinearMap g, ?_⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n : ℕ∞ω
x : G
g : G →L[𝕜] E
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝[insert (α := E) ((g : (a : G) → E) x : E) s] (g : (a : G) → E) x : Filter E) u
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
⊢ (⇑g : (a : G) → E) ⁻¹' u ∈ 𝓝[insert x ((⇑g : (a : G) → E) ⁻¹' s)] x

Tactic:
g.continuous.continuousWithinAt.tendsto_nhdsWithin ?_ hu

Premises used: Set.Mem, setOf, ContinuousWithinAt.tendsto_nhdsWithin, ContinuousLinearMap.continuous, Set.preimage, Continuous.continuousWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n : ℕ∞ω
x : G
g : G →L[𝕜] E
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝[insert (α := E) ((g : (a : G) → E) x : E) s] (g : (a : G) → E) x : Filter E) u
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
refine_1 :
  MapsTo (α := G) (⇑g : (a : G) → E) (insert x ((⇑g : (a : G) → E) ⁻¹' s)) (insert (α := E) ((g : (a : G) → E) x : E) s)
⊢ (⇑g : (a : G) → E) ⁻¹' u ∈ 𝓝[insert x ((⇑g : (a : G) → E) ⁻¹' s)] x

Tactic:
refine g.continuous.continuousWithinAt.tendsto_nhdsWithin ?_ hu

Premises used: ContinuousWithinAt.tendsto_nhdsWithin, ContinuousLinearMap.continuous, Continuous.continuousWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n : ℕ∞ω
x : G
g : G →L[𝕜] E
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝[insert (α := E) ((g : (a : G) → E) x : E) s] (g : (a : G) → E) x : Filter E) u
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
⊢ MapsTo (α := G) (⇑g : (a : G) → E) (insert x ((⇑g : (a : G) → E) ⁻¹' s)) (insert (α := E) ((g : (a : G) → E) x : E) s)

Tactic:
(mapsTo_singleton.2 <| mem_singleton _).union_union (mapsTo_preimage _ _)

Premises used: Iff.mpr, Set.mem_singleton, Set.insert, Set.Mem, setOf, Set.mapsTo_preimage, Set.singleton, Set.MapsTo.union_union, Set.mapsTo_singleton
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n : ℕ∞ω
x : G
g : G →L[𝕜] E
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝[insert (α := E) ((g : (a : G) → E) x : E) s] (g : (a : G) → E) x : Filter E) u
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
⊢ MapsTo (α := G) (⇑g : (a : G) → E) (insert x ((⇑g : (a : G) → E) ⁻¹' s)) (insert (α := E) ((g : (a : G) → E) x : E) s)

Tactic:
exact (mapsTo_singleton.2 <| mem_singleton _).union_union (mapsTo_preimage _ _)

Premises used: Iff.mpr, Set.mem_singleton, Set.mapsTo_preimage, Set.MapsTo.union_union, Set.mapsTo_singleton
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n : ℕ∞ω
x : G
g : G →L[𝕜] E
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝[insert (α := E) ((g : (a : G) → E) x : E) s] (g : (a : G) → E) x : Filter E) u
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
i : ℕ
refine_2 :
  AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (x : Fin i) ↦ G) F)
    (fun (x : G) ↦
      (ContinuousMultilinearMap.compContinuousLinearMapL (E := fun (x : Fin i) ↦ G) (E₁ := fun (x : Fin i) ↦ E)
            fun (x : Fin i) ↦ g :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ G) F)
        (p ((g : (a : G) → E) x) i))
    ((⇑g : (a : G) → E) ⁻¹' u)
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
    (fun (x : G) ↦
      (p ((g : (a : G) → E) x) i).compContinuousLinearMap (M₁ := fun (i : Fin i) ↦ G) (M₁' := fun (i : Fin i) ↦ E)
        fun (x : Fin i) ↦ g)
    ((⇑g : (a : G) → E) ⁻¹' u)

Tactic:
change AnalyticOn 𝕜 (fun x ↦
        ContinuousMultilinearMap.compContinuousLinearMapL (fun _ ↦ g) (p (g x) i)) (⇑g ⁻¹' u)

Premises used: AnalyticOn, Set.preimage, DFunLike.coe, ContinuousMultilinearMap.compContinuousLinearMapL
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n : ℕ∞ω
x : G
g : G →L[𝕜] E
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝[insert (α := E) ((g : (a : G) → E) x : E) s] (g : (a : G) → E) x : Filter E) u
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
i : ℕ
apply :
  AnalyticOn 𝕜 (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (F :=
    ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (x : Fin i) ↦ G) F)
    (⇑(ContinuousMultilinearMap.compContinuousLinearMapL (E := fun (x : Fin i) ↦ G) (E₁ := fun (x : Fin i) ↦ E)
          fun (x : Fin i) ↦ g) :
      (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ G) F)
    univ
apply₁ :
  AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
    (fun (x : G) ↦ p ((g : (a : G) → E) x) i) ((⇑g : (a : G) → E) ⁻¹' u)
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (x : Fin i) ↦ G) F)
    (fun (x : G) ↦
      (ContinuousMultilinearMap.compContinuousLinearMapL (E := fun (x : Fin i) ↦ G) (E₁ := fun (x : Fin i) ↦ E)
            fun (x : Fin i) ↦ g :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ G) F)
        (p ((g : (a : G) → E) x) i))
    ((⇑g : (a : G) → E) ⁻¹' u)

Tactic:
apply AnalyticOn.comp _ _ (Set.mapsTo_univ _ _)

Premises used: Set.mapsTo_univ, AnalyticOn.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n : ℕ∞ω
x : G
g : G →L[𝕜] E
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝[insert (α := E) ((g : (a : G) → E) x : E) s] (g : (a : G) → E) x : Filter E) u
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (F :=
    ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (x : Fin i) ↦ G) F)
    (⇑(ContinuousMultilinearMap.compContinuousLinearMapL (E := fun (x : Fin i) ↦ G) (E₁ := fun (x : Fin i) ↦ E)
          fun (x : Fin i) ↦ g) :
      (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ G) F)
    univ

Tactic:
ContinuousLinearMap.analyticOn _ _

Premises used: ContinuousLinearMap.analyticOn
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n : ℕ∞ω
x : G
g : G →L[𝕜] E
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝[insert (α := E) ((g : (a : G) → E) x : E) s] (g : (a : G) → E) x : Filter E) u
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (F :=
    ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (x : Fin i) ↦ G) F)
    (⇑(ContinuousMultilinearMap.compContinuousLinearMapL (E := fun (x : Fin i) ↦ G) (E₁ := fun (x : Fin i) ↦ E)
          fun (x : Fin i) ↦ g) :
      (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ G) F)
    univ

Tactic:
exact ContinuousLinearMap.analyticOn _ _

Premises used: ContinuousLinearMap.analyticOn
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n : ℕ∞ω
x : G
g : G →L[𝕜] E
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝[insert (α := E) ((g : (a : G) → E) x : E) s] (g : (a : G) → E) x : Filter E) u
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
    (fun (x : G) ↦ p ((g : (a : G) → E) x) i) ((⇑g : (a : G) → E) ⁻¹' u)

Tactic:
(h'p i).comp (g.analyticOn _) (mapsTo_preimage _ _)

Premises used: Set.mapsTo_preimage, ContinuousLinearMap.analyticOn, AnalyticOn.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n : ℕ∞ω
x : G
g : G →L[𝕜] E
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝[insert (α := E) ((g : (a : G) → E) x : E) s] (g : (a : G) → E) x : Filter E) u
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
    (fun (x : G) ↦ p ((g : (a : G) → E) x) i) ((⇑g : (a : G) → E) ⁻¹' u)

Tactic:
exact (h'p i).comp (g.analyticOn _) (mapsTo_preimage _ _)

Premises used: Set.mapsTo_preimage, ContinuousLinearMap.analyticOn, AnalyticOn.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n_1 : ℕ∞ω
x : G
g : G →L[𝕜] E
n : ℕ∞
hf : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s ((g : (a : G) → E) x)
m : ℕ
hm : (↑m : ℕ∞) ≤ n
rcases :
  ∀ (u : Set E)
    (hu :
      Membership.mem (γ := Filter E) (𝓝[insert (α := E) ((g : (a : G) → E) x : E) s] (g : (a : G) → E) x : Filter E) u)
    (p : E → FormalMultilinearSeries 𝕜 E F) (hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u),
    ∃ u ∈ 𝓝[insert x ((⇑g : (a : G) → E) ⁻¹' s)] x,
      ∃ (p : G → FormalMultilinearSeries 𝕜 G F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) (f ∘ (⇑g : (a : G) → E)) p u
⊢ ∃ u ∈ 𝓝[insert x ((⇑g : (a : G) → E) ⁻¹' s)] x,
    ∃ (p : G → FormalMultilinearSeries 𝕜 G F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) (f ∘ (⇑g : (a : G) → E)) p u

Tactic:
rcases hf m hm with ⟨u, hu, p, hp⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n_1 : ℕ∞ω
x : G
g : G →L[𝕜] E
n : ℕ∞
hf : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s ((g : (a : G) → E) x)
m : ℕ
hm : (↑m : ℕ∞) ≤ n
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝[insert (α := E) ((g : (a : G) → E) x : E) s] (g : (a : G) → E) x : Filter E) u
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
⊢ ∃ u ∈ 𝓝[insert x ((⇑g : (a : G) → E) ⁻¹' s)] x,
    ∃ (p : G → FormalMultilinearSeries 𝕜 G F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) (f ∘ (⇑g : (a : G) → E)) p u

Tactic:
⟨g ⁻¹' u, ?_, _, hp.compContinuousLinearMap g⟩

Premises used: HasFTaylorSeriesUpToOn.compContinuousLinearMap, Set.preimage, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n_1 : ℕ∞ω
x : G
g : G →L[𝕜] E
n : ℕ∞
hf : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s ((g : (a : G) → E) x)
m : ℕ
hm : (↑m : ℕ∞) ≤ n
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝[insert (α := E) ((g : (a : G) → E) x : E) s] (g : (a : G) → E) x : Filter E) u
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
refine : (⇑g : (a : G) → E) ⁻¹' u ∈ 𝓝[insert x ((⇑g : (a : G) → E) ⁻¹' s)] x
⊢ ∃ u ∈ 𝓝[insert x ((⇑g : (a : G) → E) ⁻¹' s)] x,
    ∃ (p : G → FormalMultilinearSeries 𝕜 G F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) (f ∘ (⇑g : (a : G) → E)) p u

Tactic:
refine ⟨g ⁻¹' u, ?_, _, hp.compContinuousLinearMap g⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n_1 : ℕ∞ω
x : G
g : G →L[𝕜] E
n : ℕ∞
hf : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s ((g : (a : G) → E) x)
m : ℕ
hm : (↑m : ℕ∞) ≤ n
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝[insert (α := E) ((g : (a : G) → E) x : E) s] (g : (a : G) → E) x : Filter E) u
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
⊢ (⇑g : (a : G) → E) ⁻¹' u ∈ 𝓝[insert x ((⇑g : (a : G) → E) ⁻¹' s)] x

Tactic:
g.continuous.continuousWithinAt.tendsto_nhdsWithin ?_ hu

Premises used: Set.Mem, setOf, ContinuousWithinAt.tendsto_nhdsWithin, ContinuousLinearMap.continuous, Set.preimage, Continuous.continuousWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
n_1 : ℕ∞ω
x : G
g : G →L[𝕜] E
n : ℕ∞
hf : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s ((g : (a : G) → E) x)
m : ℕ
hm : (↑m : ℕ∞) ≤ n
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝[insert (α := E) ((g : (a : G) → E) x : E) s] (g : (a : G) → E) x : Filter E) u
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
refine :
  MapsTo (α := G) (⇑g : (a : G) → E) (insert x ((⇑g : (a : G) → E) ⁻¹' s)) (insert (α := E) ((g : (a : G) → E) x : E) s)
⊢ (⇑g : (a : G) → E) ⁻¹' u ∈ 𝓝[insert x ((⇑g : (a : G) → E) ⁻¹' s)] x

Tactic:
refine g.continuous.continuousWithinAt.tendsto_nhdsWithin ?_ hu

Premises used: ContinuousWithinAt.tendsto_nhdsWithin, ContinuousLinearMap.continuous, Continuous.continuousWithinAt