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
x : E
n : ℕ∞ω
e : G ≃L[𝕜] E
H :
  ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E) : G → F) ((⇑e : (a : G) → E) ⁻¹' s : Set G)
    ((e.symm : (a : E) → G) x : G)
⊢ ContDiffWithinAt 𝕜 n f s x

Tactic:
simpa [← preimage_comp, Function.comp_def] using H.comp_continuousLinearMap (e.symm : E →L[𝕜] G)

Premises used: ContinuousLinearEquiv.symm, Set.preimage_comp, ContDiffWithinAt.comp_continuousLinearMap, Function.comp_def, ContinuousLinearEquiv.toContinuousLinearMap
-- 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 : ℕ∞ω
e : G ≃L[𝕜] E
H : ContDiffWithinAt 𝕜 n f s x
⊢ ContDiffWithinAt 𝕜 n f s (((↑e : G →L[𝕜] E) : (a : G) → E) ((e.symm : (a : E) → G) x : G))

Tactic:
rw [← e.apply_symm_apply x, ← e.coe_coe] at H

Premises used: ContinuousLinearEquiv.apply_symm_apply, ContinuousLinearEquiv.coe_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
x : E
n : ℕ∞ω
e : G ≃L[𝕜] E
H : ContDiffWithinAt 𝕜 n f s (((↑e : G →L[𝕜] E) : (a : G) → E) ((e.symm : (a : E) → G) x : G))
⊢ ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E) : G → F) ((⇑e : (a : G) → E) ⁻¹' s : Set G)
    ((e.symm : (a : E) → G) x : G)

Tactic:
H.comp_continuousLinearMap _

Premises used: ContDiffWithinAt.comp_continuousLinearMap
-- 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 : ℕ∞ω
e : G ≃L[𝕜] E
H : ContDiffWithinAt 𝕜 n f s (((↑e : G →L[𝕜] E) : (a : G) → E) ((e.symm : (a : E) → G) x : G))
⊢ ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E) : G → F) ((⇑e : (a : G) → E) ⁻¹' s : Set G)
    ((e.symm : (a : E) → G) x : G)

Tactic:
exact H.comp_continuousLinearMap _

Premises used: ContDiffWithinAt.comp_continuousLinearMap
-- 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 : ℕ∞ω
e : G ≃L[𝕜] E
rw :
  ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E) : G → F)
      (preimage.{u_4, u_2} (β := E) (⇑e : (a : G) → E) univ : Set G) ((e.symm : (a : E) → G) x : G) ↔
    ContDiffWithinAt 𝕜 n f univ x
rw₁ : Type u_2
rw₂ : G → E
⊢ ContDiffAt.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E) : G → F) ((e.symm : (a : E) → G) x : G) ↔
    ContDiffAt 𝕜 n f x

Tactic:
rw [← contDiffWithinAt_univ, ← contDiffWithinAt_univ, ← preimage_univ]

Premises used: contDiffWithinAt_univ, Set.preimage_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
f : E → F
x : E
n : ℕ∞ω
e : G ≃L[𝕜] E
⊢ ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E) : G → F)
      (preimage.{u_4, u_2} (β := E) (⇑e : (a : G) → E) univ : Set G) ((e.symm : (a : E) → G) x : G) ↔
    ContDiffWithinAt 𝕜 n f univ x

Tactic:
e.contDiffWithinAt_comp_iff

Premises used: ContinuousLinearEquiv.contDiffWithinAt_comp_iff
-- 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 : ℕ∞ω
e : G ≃L[𝕜] E
H : ContDiffOn.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E)) ((⇑e : (a : G) → E) ⁻¹' s)
⊢ ContDiffOn 𝕜 n f s

Tactic:
simpa [Function.comp_def] using H.comp_continuousLinearMap (e.symm : E →L[𝕜] G)

Premises used: ContinuousLinearEquiv.symm, Function.comp_def, ContDiffOn.comp_continuousLinearMap, ContinuousLinearEquiv.toContinuousLinearMap
-- 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
n : ℕ∞ω
e : G ≃L[𝕜] E
rw :
  ContDiffOn.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E))
      (preimage.{u_4, u_2} (β := E) (⇑e : (a : G) → E) univ) ↔
    ContDiffOn 𝕜 n f univ
rw₁ : Type u_2
rw₂ : G → E
⊢ ContDiff.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E)) ↔ ContDiff 𝕜 n f

Tactic:
rw [← contDiffOn_univ, ← contDiffOn_univ, ← preimage_univ]

Premises used: Set.preimage_univ, 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
f : E → F
n : ℕ∞ω
e : G ≃L[𝕜] E
⊢ ContDiffOn.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E))
      (preimage.{u_4, u_2} (β := E) (⇑e : (a : G) → E) univ) ↔
    ContDiffOn 𝕜 n f univ

Tactic:
e.contDiffOn_comp_iff

Premises used: ContinuousLinearEquiv.contDiffOn_comp_iff
-- 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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ∞ω
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
L : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin m) ↦ E) F ×
      ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin m) ↦ E) G ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun (x : Fin m) ↦ E) (F × G) :=
  fun (m : ℕ) ↦ ContinuousMultilinearMap.prodL 𝕜 (fun (x : Fin m) ↦ E) F G
zero_eq :
  ∀ x ∈ s,
    ContinuousMultilinearMap.curry0 (𝕜 := 𝕜) (G := E)
        (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin 0) ↦ E) (p x 0) (q x 0)) =
      (f x, g x)
fderivWithin :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) < n →
      ∀ x ∈ s,
        HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (F × G))
          (fun (x : E) ↦ (p x m).prod (M₁ := fun (i : Fin m) ↦ E) (q x m))
          (ContinuousMultilinearMap.curryLeft (𝕜 := 𝕜) (Ei := fun (i : Fin m.succ) ↦ E) (G := F × G)
            (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin m.succ) ↦ E) (p x m.succ) (q x m.succ)))
          s x
cont :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) ≤ n →
      ContinuousOn (Y := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (F × G))
        (fun (x : E) ↦ (p x m).prod (M₁ := fun (i : Fin m) ↦ E) (q x m)) s
⊢ HasFTaylorSeriesUpToOn (𝕜 := 𝕜) (F := F × G) n (fun (y : E) ↦ (f y, g y))
    (fun (y : E) (k : ℕ) ↦ (p y k).prod (M₁ := fun (i : Fin k) ↦ E) (q y k)) s

Tactic:
constructor
-- 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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ∞ω
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
L : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin m) ↦ E) F ×
      ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin m) ↦ E) G ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun (x : Fin m) ↦ E) (F × G) :=
  fun (m : ℕ) ↦ ContinuousMultilinearMap.prodL 𝕜 (fun (x : Fin m) ↦ E) F G
x : E
hx : x ∈ s
zero_eq :
  ContinuousMultilinearMap.curry0 (𝕜 := 𝕜) (G := E)
      (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin 0) ↦ E) (p x 0) (q x 0)) =
    (ContinuousMultilinearMap.curry0 (p x 0), ContinuousMultilinearMap.curry0 (q x 0))
⊢ ContinuousMultilinearMap.curry0 (𝕜 := 𝕜) (G := E)
      (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin 0) ↦ E) (p x 0) (q x 0)) =
    (f x, g x)

Tactic:
rw [← hf.zero_eq x hx, ← hg.zero_eq x hx]

Premises used: HasFTaylorSeriesUpToOn.zero_eq
-- 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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ∞ω
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
L : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin m) ↦ E) F ×
      ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin m) ↦ E) G ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun (x : Fin m) ↦ E) (F × G) :=
  fun (m : ℕ) ↦ ContinuousMultilinearMap.prodL 𝕜 (fun (x : Fin m) ↦ E) F G
x : E
hx : x ∈ s
⊢ ContinuousMultilinearMap.curry0 (𝕜 := 𝕜) (G := E)
      (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin 0) ↦ E) (p x 0) (q x 0)) =
    (ContinuousMultilinearMap.curry0 (p x 0), ContinuousMultilinearMap.curry0 (q x 0))

Tactic:
rfl
-- 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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ∞ω
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
L : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin m) ↦ E) F ×
      ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin m) ↦ E) G ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun (x : Fin m) ↦ E) (F × G) :=
  fun (m : ℕ) ↦ ContinuousMultilinearMap.prodL 𝕜 (fun (x : Fin m) ↦ E) F G
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt
    (comp (β :=
      ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin m) ↦ E) F ×
        ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin m) ↦ E) G)
      (⇑(L m) :
        (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin m) ↦ E) F × ContinuousMultilinearMap 𝕜 (fun (x : Fin m) ↦ E) G) →
          ContinuousMultilinearMap 𝕜 (fun (x : Fin m) ↦ E) (F × G))
      fun (x : E) ↦ (p x m, q x m))
    ((↑(↑(L m) :
            (ContinuousMultilinearMap 𝕜 (fun (x : Fin m) ↦ E) F ×
                ContinuousMultilinearMap 𝕜 (fun (x : Fin m) ↦ E) G) ≃L[𝕜]
              ContinuousMultilinearMap 𝕜 (fun (x : Fin m) ↦ E) (F × G)) :
        ContinuousMultilinearMap 𝕜 (fun (x : Fin m) ↦ E) F × ContinuousMultilinearMap 𝕜 (fun (x : Fin m) ↦ E) G →L[𝕜]
          ContinuousMultilinearMap 𝕜 (fun (x : Fin m) ↦ E) (F × G)) ∘SL
      ContinuousLinearMap.prod (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ))
        (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (q x m.succ)))
    s x

Tactic:
(L m).hasFDerivAt.comp_hasFDerivWithinAt x
        ((hf.fderivWithin m hm x hx).prodMk (hg.fderivWithin m hm x hx))

Premises used: HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.prodMk, HasFTaylorSeriesUpToOn.fderivWithin, LinearIsometryEquiv.hasFDerivAt
-- 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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ∞ω
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
L : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin m) ↦ E) F ×
      ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin m) ↦ E) G ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun (x : Fin m) ↦ E) (F × G) :=
  fun (m : ℕ) ↦ ContinuousMultilinearMap.prodL 𝕜 (fun (x : Fin m) ↦ E) F G
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (F × G))
    (fun (x : E) ↦ (p x m).prod (M₁ := fun (i : Fin m) ↦ E) (q x m))
    (ContinuousMultilinearMap.curryLeft (𝕜 := 𝕜) (Ei := fun (i : Fin m.succ) ↦ E) (G := F × G)
      (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin m.succ) ↦ E) (p x m.succ) (q x m.succ)))
    s x

Tactic:
convert!
      (L m).hasFDerivAt.comp_hasFDerivWithinAt x
        ((hf.fderivWithin m hm x hx).prodMk (hg.fderivWithin m hm x hx))

Premises used: HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.prodMk, HasFTaylorSeriesUpToOn.fderivWithin, LinearIsometryEquiv.hasFDerivAt
-- 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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ∞ω
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
L : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin m) ↦ E) F ×
      ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin m) ↦ E) G ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun (x : Fin m) ↦ E) (F × G) :=
  fun (m : ℕ) ↦ ContinuousMultilinearMap.prodL 𝕜 (fun (x : Fin m) ↦ E) F G
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
⊢ ContinuousOn (Y := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (F × G))
    (fun (x : E) ↦ (p x m).prod (M₁ := fun (i : Fin m) ↦ E) (q x m)) s

Tactic:
(L m).continuous.comp_continuousOn ((hf.cont m hm).prodMk (hg.cont m hm))

Premises used: Continuous.comp_continuousOn, setOf, HasFTaylorSeriesUpToOn.cont, ContinuousOn.prodMk, LinearIsometryEquiv.continuous, ContinuousMultilinearMap.prod
-- 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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ∞ω
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
L : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin m) ↦ E) F ×
      ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (x : Fin m) ↦ E) G ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun (x : Fin m) ↦ E) (F × G) :=
  fun (m : ℕ) ↦ ContinuousMultilinearMap.prodL 𝕜 (fun (x : Fin m) ↦ E) F G
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
⊢ ContinuousOn (Y := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (F × G))
    (fun (x : E) ↦ (p x m).prod (M₁ := fun (i : Fin m) ↦ E) (q x m)) s

Tactic:
exact (L m).continuous.comp_continuousOn ((hf.cont m hm).prodMk (hg.cont m hm))

Premises used: Continuous.comp_continuousOn, HasFTaylorSeriesUpToOn.cont, ContinuousOn.prodMk, LinearIsometryEquiv.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
x : E
n : ℕ∞ω
s : Set E
f : E → F
g : E → G
hf : ContDiffWithinAt 𝕜 ω f s x
hg : ContDiffWithinAt 𝕜 ω g 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 𝕜 (F := F × G) ω (fun (x : E) ↦ (f x, g x)) s x
⊢ ContDiffWithinAt 𝕜 (F := F × G) ω (fun (x : E) ↦ (f x, g x)) 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
x : E
n : ℕ∞ω
s : Set E
f : E → F
g : E → G
hg : ContDiffWithinAt 𝕜 ω g s x
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
obtain :
  ∀ (v : Set E) (hv : v ∈ 𝓝[insert x s] x) (q : E → FormalMultilinearSeries 𝕜 E G) (hq : HasFTaylorSeriesUpToOn ω g q v)
    (h'q :
      ∀ (i : ℕ),
        AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) (fun (x : E) ↦ q x i)
          v),
    ContDiffWithinAt 𝕜 (F := F × G) ω (fun (x : E) ↦ (f x, g x)) s x
⊢ ContDiffWithinAt 𝕜 (F := F × G) ω (fun (x : E) ↦ (f x, g x)) s x

Tactic:
obtain ⟨v, hv, q, hq, h'q⟩ := hg
-- 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
x : E
n : ℕ∞ω
s : Set E
f : E → F
g : E → 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
v : Set E
hv : v ∈ 𝓝[insert x s] x
q : E → FormalMultilinearSeries 𝕜 E G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) (fun (x : E) ↦ q x i) v
⊢ ContDiffWithinAt 𝕜 (F := F × G) ω (fun (x : E) ↦ (f x, g x)) s x

Tactic:
⟨u ∩ v, Filter.inter_mem hu hv, _,
      (hp.mono inter_subset_left).prodMk (hq.mono inter_subset_right), fun i ↦ ?_⟩

Premises used: Filter.inter_mem, HasFTaylorSeriesUpToOn.mono, Set.inter_subset_left, Inter.inter, HasFTaylorSeriesUpToOn.prodMk, And.intro, Exists.intro, ContDiffWithinAt, Set.inter_subset_right
-- 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
x : E
n : ℕ∞ω
s : Set E
f : E → F
g : E → 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
v : Set E
hv : v ∈ 𝓝[insert x s] x
q : E → FormalMultilinearSeries 𝕜 E G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) (fun (x : E) ↦ q x i) v
refine :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F × G))
      (fun (x : E) ↦ (p x i).prod (M₁ := fun (i : Fin i) ↦ E) (q x i)) (u ∩ v)
⊢ ContDiffWithinAt 𝕜 (F := F × G) ω (fun (x : E) ↦ (f x, g x)) s x

Tactic:
refine ⟨u ∩ v, Filter.inter_mem hu hv, _,
      (hp.mono inter_subset_left).prodMk (hq.mono inter_subset_right), 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
x : E
n : ℕ∞ω
s : Set E
f : E → F
g : E → 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
v : Set E
hv : v ∈ 𝓝[insert x s] x
q : E → FormalMultilinearSeries 𝕜 E G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) (fun (x : E) ↦ q x i) v
i : ℕ
change :
  AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F × G))
    (fun (x : E) ↦
      (ContinuousMultilinearMap.prodL 𝕜 (fun (i : Fin i) ↦ E) F G :
          (a :
              ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F × ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) G) →
            ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F × G))
        (p x i, q x i))
    (u ∩ v)
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F × G))
    (fun (x : E) ↦ (p x i).prod (M₁ := fun (i : Fin i) ↦ E) (q x i)) (u ∩ v)

Tactic:
change AnalyticOn 𝕜 (fun x ↦ ContinuousMultilinearMap.prodL _ _ _ _ (p x i, q x i)) (u ∩ v)

Premises used: AnalyticOn, Prod.mk, ContinuousMultilinearMap.prodL, Inter.inter, 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
x : E
n : ℕ∞ω
s : Set E
f : E → F
g : E → 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
v : Set E
hv : v ∈ 𝓝[insert x s] x
q : E → FormalMultilinearSeries 𝕜 E G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) (fun (x : E) ↦ q x i) v
i : ℕ
apply :
  AnalyticOn 𝕜 (F :=
    ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F ×
      ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (fun (x : E) ↦ (p x i, q x i)) (u ∩ v)
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F × G))
    (fun (x : E) ↦
      (ContinuousMultilinearMap.prodL 𝕜 (fun (i : Fin i) ↦ E) F G :
          (a :
              ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F × ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) G) →
            ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F × G))
        (p x i, q x i))
    (u ∩ v)

Tactic:
apply (LinearIsometryEquiv.analyticOnNhd _ _).comp_analyticOn _ (Set.mapsTo_univ _ _)

Premises used: LinearIsometryEquiv.analyticOnNhd, Set.mapsTo_univ, AnalyticOnNhd.comp_analyticOn