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
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
f : E →L[𝕜] F
⊢ ContDiff.{u_1, u_2, u_3} 𝕜 (E := E) (F := F) n (⇑f : (a : E) → F)

Tactic:
f.isBoundedLinearMap.contDiff

Premises used: IsBoundedLinearMap.contDiff, ContinuousLinearMap.isBoundedLinearMap
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
f : E ≃L[𝕜] F
⊢ ContDiff.{u_1, u_2, u_3} 𝕜 (E := E) (F := F) n (⇑f : (a : E) → F)

Tactic:
(f : E →L[𝕜] F).contDiff

Premises used: ContinuousLinearMap.contDiff, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
f : E →ₗᵢ[𝕜] F
⊢ ContDiff.{u_1, u_2, u_3} 𝕜 (E := E) (F := F) n (⇑f : (a : E) → F)

Tactic:
f.toContinuousLinearMap.contDiff

Premises used: ContinuousLinearMap.contDiff, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
f : E ≃ₗᵢ[𝕜] F
⊢ ContDiff.{u_1, u_2, u_3} 𝕜 (E := E) (F := F) n (⇑f : (a : E) → F)

Tactic:
(f : E →L[𝕜] F).contDiff

Premises used: LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousLinearMap.contDiff, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
⊢ ContDiff.{u_1, u_2, u_2} 𝕜 (E := E) n id

Tactic:
IsBoundedLinearMap.id.contDiff

Premises used: IsBoundedLinearMap.contDiff, IsBoundedLinearMap.id
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
s : Set E
x : E
⊢ ContDiffWithinAt 𝕜 n id s x

Tactic:
contDiff_id.contDiffWithinAt

Premises used: contDiff_id, ContDiff.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
x : E
⊢ ContDiffAt 𝕜 n id x

Tactic:
contDiff_id.contDiffAt

Premises used: contDiff_id, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
s : Set E
⊢ ContDiffOn 𝕜 n id s

Tactic:
contDiff_id.contDiffOn

Premises used: contDiff_id, ContDiff.contDiffOn
-- 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
b : E × F → G
n : ℕ∞ω
hb : IsBoundedBilinearMap 𝕜 b
⊢ ContDiff 𝕜 n b

Tactic:
(hb.toContinuousLinearMap.analyticOnNhd_bilinear _).contDiff

Premises used: IsBoundedBilinearMap.toContinuousLinearMap, AnalyticOnNhd.contDiff, ContinuousLinearMap.analyticOnNhd_bilinear
-- 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
x : E
n : ℕ∞ω
g : F →L[𝕜] G
hf : ContDiffWithinAt 𝕜 ω f s x
obtain :
  ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (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.{u_1, u_2, u_4} 𝕜 (F := G) ω ((⇑g : (a : F) → G) ∘ f) s x
⊢ ContDiffWithinAt.{u_1, u_2, u_4} 𝕜 (F := G) ω ((⇑g : (a : F) → G) ∘ f) 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
x : E
n : ℕ∞ω
g : F →L[𝕜] G
u : Set E
hu : u ∈ 𝓝[insert x s] x
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.{u_1, u_2, u_4} 𝕜 (F := G) ω ((⇑g : (a : F) → G) ∘ f) s x

Tactic:
⟨u, hu, _, hp.continuousLinearMap_comp g, fun i ↦ ?_⟩

Premises used: HasFTaylorSeriesUpToOn.continuousLinearMap_comp, And.intro, Exists.intro, ContDiffWithinAt
-- 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
x : E
n : ℕ∞ω
g : F →L[𝕜] G
u : Set E
hu : u ∈ 𝓝[insert x s] x
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 :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
      (fun (x : E) ↦ g.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (p x i)) u
⊢ ContDiffWithinAt.{u_1, u_2, u_4} 𝕜 (F := G) ω ((⇑g : (a : F) → G) ∘ f) s x

Tactic:
refine ⟨u, hu, _, hp.continuousLinearMap_comp g, fun i ↦ ?_⟩
-- 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
x : E
n : ℕ∞ω
g : F →L[𝕜] G
u : Set E
hu : u ∈ 𝓝[insert x s] x
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 : ℕ
change :
  AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin i) ↦ E) G)
    (fun (x : E) ↦
      (((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 (fun (x : Fin i) ↦ E) F G :
                (a : F →L[𝕜] G) →
                  ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F →L[𝕜]
                    ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
              g :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F →L[𝕜]
              ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin i) ↦ E) G) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
        (p x i))
    u
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (fun (x : E) ↦ g.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (p x i)) u

Tactic:
change AnalyticOn 𝕜
      (fun x ↦ (ContinuousLinearMap.compContinuousMultilinearMapL 𝕜
      (fun _ : Fin i ↦ E) F G g) (p x i)) u

Premises used: AnalyticOn, DFunLike.coe, ContinuousLinearMap.compContinuousMultilinearMapL
-- 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
x : E
n : ℕ∞ω
g : F →L[𝕜] G
u : Set E
hu : u ∈ 𝓝[insert x s] x
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 :
  AnalyticOnNhd 𝕜 (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (F :=
    ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin i) ↦ E) G)
    (⇑((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 (fun (x : Fin i) ↦ E) F G :
              (a : F →L[𝕜] G) →
                ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F →L[𝕜]
                  ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
            g :
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F →L[𝕜]
            ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin i) ↦ E) G) :
      (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
    univ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin i) ↦ E) G)
    (fun (x : E) ↦
      (((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 (fun (x : Fin i) ↦ E) F G :
                (a : F →L[𝕜] G) →
                  ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F →L[𝕜]
                    ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
              g :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F →L[𝕜]
              ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin i) ↦ E) G) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
        (p x i))
    u

Tactic:
apply AnalyticOnNhd.comp_analyticOn _ (h'p i) (Set.mapsTo_univ _ _)

Premises used: Set.mapsTo_univ, AnalyticOnNhd.comp_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
x : E
n : ℕ∞ω
g : F →L[𝕜] G
u : Set E
hu : u ∈ 𝓝[insert x s] x
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 : ℕ
⊢ AnalyticOnNhd 𝕜 (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (F :=
    ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin i) ↦ E) G)
    (⇑((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 (fun (x : Fin i) ↦ E) F G :
              (a : F →L[𝕜] G) →
                ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F →L[𝕜]
                  ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
            g :
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F →L[𝕜]
            ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin i) ↦ E) G) :
      (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
    univ

Tactic:
ContinuousLinearMap.analyticOnNhd _ _

Premises used: ContinuousLinearMap.analyticOnNhd
-- 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
x : E
n : ℕ∞ω
g : F →L[𝕜] G
u : Set E
hu : u ∈ 𝓝[insert x s] x
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 : ℕ
⊢ AnalyticOnNhd 𝕜 (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (F :=
    ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin i) ↦ E) G)
    (⇑((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 (fun (x : Fin i) ↦ E) F G :
              (a : F →L[𝕜] G) →
                ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F →L[𝕜]
                  ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
            g :
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F →L[𝕜]
            ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin i) ↦ E) G) :
      (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
    univ

Tactic:
exact ContinuousLinearMap.analyticOnNhd _ _

Premises used: ContinuousLinearMap.analyticOnNhd
-- 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
x : E
n_1 : ℕ∞ω
g : F →L[𝕜] G
n : ℕ∞
hf : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s x
m : ℕ
hm : (↑m : ℕ∞) ≤ n
rcases :
  ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries 𝕜 E F)
    (hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u),
    ∃ u ∈ 𝓝[insert x s] x,
      ∃ (p : E → FormalMultilinearSeries 𝕜 E G), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) ((⇑g : (a : F) → G) ∘ f) p u
⊢ ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E G), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) ((⇑g : (a : F) → G) ∘ f) 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
x : E
n_1 : ℕ∞ω
g : F →L[𝕜] G
n : ℕ∞
hf : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s x
m : ℕ
hm : (↑m : ℕ∞) ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
⊢ ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E G), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) ((⇑g : (a : F) → G) ∘ f) p u

Tactic:
⟨u, hu, _, hp.continuousLinearMap_comp g⟩

Premises used: HasFTaylorSeriesUpToOn.continuousLinearMap_comp, And.intro, Exists.intro
-- 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
x : E
n_1 : ℕ∞ω
g : F →L[𝕜] G
n : ℕ∞
hf : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s x
m : ℕ
hm : (↑m : ℕ∞) ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
⊢ ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E G), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) ((⇑g : (a : F) → G) ∘ f) p u

Tactic:
exact ⟨u, hu, _, hp.continuousLinearMap_comp 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
x : E
n : ℕ∞ω
g : F →L[𝕜] G
hf : ContDiffWithinAt 𝕜 n f s x
⊢ ContDiffWithinAt.{u_1, u_2, u_4} 𝕜 (F := G) n ((⇑g : (a : F) → G) ∘ f) s x

Tactic:
match n with
  | ω =>
    obtain ⟨u, hu, p, hp, h'p⟩ := hf
    refine ⟨u, hu, _, hp.continuousLinearMap_comp g, fun i ↦ ?_⟩
    change AnalyticOn 𝕜
      (fun x ↦ (ContinuousLinearMap.compContinuousMultilinearMapL 𝕜
      (fun _ : Fin i ↦ E) F G g) (p x i)) u
    apply AnalyticOnNhd.comp_analyticOn _ (h'p i) (Set.mapsTo_univ _ _)
    exact ContinuousLinearMap.analyticOnNhd _ _
  | (n : ℕ∞) =>
    intro m hm
    rcases hf m hm with ⟨u, hu, p, hp⟩
    exact ⟨u, hu, _, hp.continuousLinearMap_comp 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
f : E → F
x : E
n : ℕ∞ω
g : F →L[𝕜] G
hf : ContDiffAt 𝕜 n f x
⊢ ContDiffAt.{u_1, u_2, u_4} 𝕜 (F := G) n ((⇑g : (a : F) → G) ∘ f) x

Tactic:
ContDiffWithinAt.continuousLinearMap_comp g hf

Premises used: ContDiffAt, ContDiffWithinAt.continuousLinearMap_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 : ℕ∞ω
g : F →L[𝕜] G
hf : ContDiffOn 𝕜 n f s
⊢ ContDiffOn.{u_1, u_2, u_4} 𝕜 (F := G) n ((⇑g : (a : F) → G) ∘ f) s

Tactic:
fun x hx => (hf x hx).continuousLinearMap_comp g

Premises used: ContDiffOn, ContDiffWithinAt.continuousLinearMap_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
n : ℕ∞ω
f : E → F
g : F →L[𝕜] G
hf : ContDiff 𝕜 n f
⊢ ContDiff.{u_1, u_2, u_4} 𝕜 (F := G) n fun (x : E) ↦ (g : (a : F) → G) (f x)

Tactic:
contDiffOn_univ.1 <| ContDiffOn.continuousLinearMap_comp _ (contDiffOn_univ.2 hf)

Premises used: Iff.mpr, ContDiffOn.continuousLinearMap_comp, Iff.mp, contDiffOn_univ
-- 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
x : E
n : ℕ∞ω
f : E → F
g : F →L[𝕜] G
hf : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
⊢ Eq (α := ℕ∞ω) (↑i : ℕ∞ω) ∞ → n = ω

Tactic:
simp
-- 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
x : E
n : ℕ∞ω
f : E → F
g : F →L[𝕜] G
hf : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
rcases :
  ∀ (U : Set E) (hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) (hxU : x ∈ U)
    (hfU : ContDiffOn 𝕜 (↑i : ℕ∞ω) f (insert x s ∩ U)),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
      (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s x)
      (g.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x))
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s x)
    (g.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x))

Tactic:
rcases hf.contDiffOn' hi (by simp) with ⟨U, hU, hxU, hfU⟩

Premises used: ContDiffWithinAt.contDiffOn'
-- 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
x : E
n : ℕ∞ω
f : E → F
g : F →L[𝕜] G
hf : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hxU : x ∈ U
hfU : ContDiffOn 𝕜 (↑i : ℕ∞ω) f (insert x s ∩ U)
rw :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) (s ∩ U) x)
    (g.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f (s ∩ U) x))
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s x)
    (g.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x))

Tactic:
rw [← iteratedFDerivWithin_inter_open hU hxU, ← iteratedFDerivWithin_inter_open (f := f) hU hxU]

Premises used: iteratedFDerivWithin_inter_open
-- 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
x : E
n : ℕ∞ω
f : E → F
g : F →L[𝕜] G
hf : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hxU : x ∈ U
hfU : ContDiffOn 𝕜 (↑i : ℕ∞ω) f (insert x s ∩ U)
⊢ ContDiffOn 𝕜 (↑i : ℕ∞ω) f (s ∩ U)

Tactic:
rw [insert_eq_of_mem hx] at hfU

Premises used: Set.insert_eq_of_mem
-- 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
x : E
n : ℕ∞ω
f : E → F
g : F →L[𝕜] G
hf : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hxU : x ∈ U
hfU : ContDiffOn 𝕜 (↑i : ℕ∞ω) f (s ∩ U)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) (s ∩ U) x)
    (g.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f (s ∩ U) x))

Tactic:
.symm <| (hfU.ftaylorSeriesWithin (hs.inter hU)).continuousLinearMap_comp g
    |>.eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl (hs.inter hU) ⟨hx, hxU⟩

Premises used: le_rfl, HasFTaylorSeriesUpToOn.continuousLinearMap_comp, And.intro, HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn, UniqueDiffOn.inter, Eq.symm, ContDiffOn.ftaylorSeriesWithin