awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
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
x : G
hx : Membership.mem (γ := Set G) ((⇑g : (a : G) → E) ⁻¹' s) x
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := 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)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ G)
      (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin m.succ) ↦ G) (M₁' := fun (i : Fin m.succ) ↦
        E) (p ((g : (a : G) → E) x) m.succ) fun (x : Fin m.succ) ↦ g.contLinear))
    ((⇑g : (a : G) → E) ⁻¹' s) x
have h : Eq (α := AddCommGroup (ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F))
    (ContinuousMultilinearMap.instAddCommGroup (M₁ := fun (i : Fin m) ↦ G)) NormedAddCommGroup.toAddCommGroup →
  HEq (α := Module 𝕜 (ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F))
      (ContinuousMultilinearMap.instModule (M₁ := fun (i : Fin m) ↦ G)) (β :=
      Module 𝕜 (ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F)) NormedSpace.toModule →
    Eq (α := TopologicalSpace (ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F))
        (ContinuousMultilinearMap.instTopologicalSpace (E := fun (i : Fin m) ↦ G)) UniformSpace.toTopologicalSpace →
      Eq (α := G →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F)
        (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ G)
            (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin m.succ) ↦ G) (M₁' :=
              fun (i : Fin m.succ) ↦ E) (p ((g : (a : G) → E) x) m.succ) fun (x : Fin m.succ) ↦ g.contLinear) :
          G →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F)
        (IsBoundedLinearMap.toContinuousLinearMap (A m) sorry ∘SL
            ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p ((g : (a : G) → E) x) m.succ) ∘SL
              g.contLinear :
          G →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F)
Tactic: convert!
      (hA m).hasFDerivAt.comp_hasFDerivWithinAt x
        ((hf.fderivWithin m hm (g x) hx).comp x g.hasFDerivWithinAt (Subset.refl _))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
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
x : G
hx : Membership.mem (γ := Set G) ((⇑g : (a : G) → E) ⁻¹' s) x
e_8 :
  Eq (α := AddCommGroup (ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F))
    (ContinuousMultilinearMap.instAddCommGroup (M₁ := fun (i : Fin m) ↦ G)) NormedAddCommGroup.toAddCommGroup
e_9 :
  HEq (α := Module 𝕜 (ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F))
    (ContinuousMultilinearMap.instModule (M₁ := fun (i : Fin m) ↦ G)) (β :=
    Module 𝕜 (ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F)) NormedSpace.toModule
e_10 :
  Eq (α := TopologicalSpace (ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F))
    (ContinuousMultilinearMap.instTopologicalSpace (E := fun (i : Fin m) ↦ G)) UniformSpace.toTopologicalSpace
y : G
v : (i : Fin m) → G
⊢ Eq.{u_3 + 1} (α := F)
    ((p ((g : (a : G) → E) x) m.succ : (a : (i : Fin m.succ) → E) → F)
        (comp.{1, u_4 + 1, u_2 + 1} (β := G) (⇑g.contLinear : (a : G) → E) (cons (α := fun (a : Fin m.succ) ↦ G) y v)) :
      F)
    ((p ((g : (a : G) → E) x) m.succ : (a : (i : Fin m.succ) → E) → F)
        (cons (α := fun (i : Fin m.succ) ↦ E) ((g.contLinear : (a : G) → E) y) ((⇑g.contLinear : (a : G) → E) ∘ v)) :
      F)
have h : Eq.{u_3 + 1} (α := F)
  ((p ((g : (a : G) → E) x) m.succ : (a : (i : Fin m.succ) → E) → F)
      (cons (α := fun (i : Fin (m + 1)) ↦ E) ((g.contLinear : (a : G) → E) y) ((⇑g.contLinear : (a : G) → E) ∘ v)) :
    F)
  ((p ((g : (a : G) → E) x) m.succ : (a : (i : Fin m.succ) → E) → F)
      (cons (α := fun (i : Fin m.succ) ↦ E) ((g.contLinear : (a : G) → E) y) ((⇑g.contLinear : (a : G) → E) ∘ v)) :
    F)
Tactic: rw [comp_cons]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
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)
⊢ ContDiffWithinAt 𝕜 ω (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x
have 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
Tactic: obtain ⟨u, hu, p, hp, h'p⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
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
have refine_1 : (⇑g : (a : G) → E) ⁻¹' u ∈ 𝓝[insert x ((⇑g : (a : G) → E) ⁻¹' s)] x
Tactic: refine ⟨g ⁻¹' u, ?_, _, hp.compContinuousLinearMap g, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
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
⊢ ContDiffWithinAt 𝕜 ω (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x
have 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)
Tactic: refine ⟨g ⁻¹' u, ?_, _, hp.compContinuousLinearMap g, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
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
have refine_1 : MapsTo (α := G) (⇑g : (a : G) → E) (insert x ((⇑g : (a : G) → E) ⁻¹' s)) (insert (α := E) ((g : (a : G) → E) x : E) s)
Tactic: refine g.continuous.continuousWithinAt.tendsto_nhdsWithin ?_ hu
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
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_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)
have 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)
Tactic: change AnalyticOn 𝕜 (fun x ↦
        ContinuousMultilinearMap.compContinuousLinearMapL (fun _ ↦ g) (p (g x) i)) (⇑g ⁻¹' u)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
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_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)
have 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
Tactic: apply AnalyticOn.comp _ _ (Set.mapsTo_univ _ _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
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
⊢ 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)
have 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)
Tactic: apply AnalyticOn.comp _ _ (Set.mapsTo_univ _ _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
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 ∈ 𝓝[insert x ((⇑g : (a : G) → E) ⁻¹' s)] x,
    ∃ (p : G → FormalMultilinearSeries 𝕜 G F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) (f ∘ (⇑g : (a : G) → E)) p u
have 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
Tactic: rcases hf m hm with ⟨u, hu, p, hp⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
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
have refine : (⇑g : (a : G) → E) ⁻¹' u ∈ 𝓝[insert x ((⇑g : (a : G) → E) ⁻¹' s)] x
Tactic: refine ⟨g ⁻¹' u, ?_, _, hp.compContinuousLinearMap g⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
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
have refine : MapsTo (α := G) (⇑g : (a : G) → E) (insert x ((⇑g : (a : G) → E) ⁻¹' s)) (insert (α := E) ((g : (a : G) → E) x : E) s)
Tactic: refine g.continuous.continuousWithinAt.tendsto_nhdsWithin ?_ hu
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
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
g : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin 0) ↦ G) F)
    (iteratedFDerivWithin 𝕜 0 (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x)
    (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin 0) ↦ G) (M₁' := fun (i : Fin 0) ↦ E)
      (iteratedFDerivWithin 𝕜 0 f s ((g : (a : G) → E) x)) fun (x : Fin 0) ↦ (↑g : G →L[𝕜] E))
have zero : ∀ (m : (i : Fin 0) → G),
  Eq.{u_3 + 1} (α := F)
    ((iteratedFDerivWithin 𝕜 0 (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x : (a : (i : Fin 0) → G) → F) m : F)
    ((ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin 0) ↦ G) (M₁' := fun (i : Fin 0) ↦ E)
            (iteratedFDerivWithin 𝕜 0 f s ((g : (a : G) → E) x)) fun (x : Fin 0) ↦ (↑g : G →L[𝕜] E) :
          (a : (i : Fin 0) → G) → F)
        m :
      F)
Tactic: ext1 m
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
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
g : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : G} (hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
      (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x)
      (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin i) ↦ G) (M₁' := fun (i : Fin i) ↦ E)
        (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x)) fun (x : Fin i) ↦ (↑g : G →L[𝕜] E))
x : G
hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin (i + 1)) ↦ G) F)
    (iteratedFDerivWithin 𝕜 (i + 1) (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x)
    (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin (i + 1)) ↦ G) (M₁' := fun (i : Fin (i + 1)) ↦
      E) (iteratedFDerivWithin 𝕜 (i + 1) f s ((g : (a : G) → E) x)) fun (x : Fin (i + 1)) ↦ (↑g : G →L[𝕜] E))
have succ : ∀ (m : (i : Fin (i + 1)) → G),
  Eq.{u_3 + 1} (α := F)
    ((iteratedFDerivWithin 𝕜 (i + 1) (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x :
          (a : (i : Fin (i + 1)) → G) → F)
        m :
      F)
    ((ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin (i + 1)) ↦ G) (M₁' := fun (i : Fin (i + 1)) ↦
            E) (iteratedFDerivWithin 𝕜 (i + 1) f s ((g : (a : G) → E) x)) fun (x : Fin (i + 1)) ↦ (↑g : G →L[𝕜] E) :
          (a : (i : Fin (i + 1)) → G) → F)
        m :
      F)
Tactic: ext1 m
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
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
g : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : G} (hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
      (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x)
      (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin i) ↦ G) (M₁' := fun (i : Fin i) ↦ E)
        (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x)) fun (x : Fin i) ↦ (↑g : G →L[𝕜] E))
x : G
hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)
m : (i : Fin (i + 1)) → G
⊢ Eq.{u_3 + 1} (α := F)
    ((iteratedFDerivWithin 𝕜 (i + 1) (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x :
          (a : (i : Fin (i + 1)) → G) → F)
        m :
      F)
    ((ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin (i + 1)) ↦ G) (M₁' := fun (i : Fin (i + 1)) ↦
            E) (iteratedFDerivWithin 𝕜 (i + 1) f s ((g : (a : G) → E) x)) fun (x : Fin (i + 1)) ↦ (↑g : G →L[𝕜] E) :
          (a : (i : Fin (i + 1)) → G) → F)
        m :
      F)
have succ : Eq.{u_3 + 1} (α := F)
  ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s))
                ((⇑g : (a : G) → E) ⁻¹' s) x :
              (a : G) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ G) F)
            (m 0) :
          ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F) :
        (a : (i : Fin i) → G) → F)
      (tail (α := fun (i : Fin (i + 1)) ↦ G) m) :
    F)
  ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s ((g : (a : G) → E) x) :
              (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
            ((g : (a : G) → E) (m 0)) :
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) :
        (a : (i : Fin i) → E) → F)
      (tail (α := fun (i : Fin (i + 1)) ↦ E) fun (i : Fin (i + 1)) ↦ (g : (a : G) → E) (m i) : (i : Fin i) → E) :
    F)
Tactic: simp only [ContinuousMultilinearMap.compContinuousLinearMap_apply,
      ContinuousLinearEquiv.coe_coe, iteratedFDerivWithin_succ_apply_left]