awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries.{u_1, uE, u_5} 𝕜 E (F' i)
n : ℕ∞ω
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj (φ := F')
L : (m : ℕ) →
  ((i : ι) → ContinuousMultilinearMap.{u_1, 0, uE, u_5} 𝕜 (fun (i : Fin m) ↦ E) (F' i)) ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i) :=
  fun (m : ℕ) ↦ ContinuousMultilinearMap.piₗᵢ 𝕜 fun (i : Fin m) ↦ E (E' := F')
h :
  HasFTaylorSeriesUpToOn (𝕜 := 𝕜) (F := (i : ι) → F' i) n (fun (x : E) (i : ι) ↦ φ i x)
    (fun (x : E) (m : ℕ) ↦ ContinuousMultilinearMap.pi (M₁ := fun (i : Fin m) ↦ E) (M' := F') fun (i : ι) ↦ p' i x m) s
i : ι
⊢ HasFTaylorSeriesUpToOn n (φ i) (p' i) s

Tactic:
exact h.continuousLinearMap_comp (pr i)

Premises used: HasFTaylorSeriesUpToOn.continuousLinearMap_comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries.{u_1, uE, u_5} 𝕜 E (F' i)
n : ℕ∞ω
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj (φ := F')
L : (m : ℕ) →
  ((i : ι) → ContinuousMultilinearMap.{u_1, 0, uE, u_5} 𝕜 (fun (i : Fin m) ↦ E) (F' i)) ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i) :=
  fun (m : ℕ) ↦ ContinuousMultilinearMap.piₗᵢ 𝕜 fun (i : Fin m) ↦ E (E' := F')
h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
x : E
hx : x ∈ s
refine_2 :
  ∀ (i : ι),
    ContinuousMultilinearMap.curry0 (𝕜 := 𝕜) (G := E)
        (ContinuousMultilinearMap.pi (M₁ := fun (i : Fin 0) ↦ E) (M' := F') fun (i : ι) ↦ p' i x 0) i =
      φ i x
⊢ Eq (α := (i : ι) → F' i)
    (ContinuousMultilinearMap.curry0 (𝕜 := 𝕜) (G := E)
      (ContinuousMultilinearMap.pi (M₁ := fun (i : Fin 0) ↦ E) (M' := F') fun (i : ι) ↦ p' i x 0))
    fun (i : ι) ↦ φ i x

Tactic:
ext1 i
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries.{u_1, uE, u_5} 𝕜 E (F' i)
n : ℕ∞ω
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj (φ := F')
L : (m : ℕ) →
  ((i : ι) → ContinuousMultilinearMap.{u_1, 0, uE, u_5} 𝕜 (fun (i : Fin m) ↦ E) (F' i)) ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i) :=
  fun (m : ℕ) ↦ ContinuousMultilinearMap.piₗᵢ 𝕜 fun (i : Fin m) ↦ E (E' := F')
h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
x : E
hx : x ∈ s
i : ι
⊢ ContinuousMultilinearMap.curry0 (𝕜 := 𝕜) (G := E)
      (ContinuousMultilinearMap.pi (M₁ := fun (i : Fin 0) ↦ E) (M' := F') fun (i : ι) ↦ p' i x 0) i =
    φ i x

Tactic:
(h i).zero_eq x hx

Premises used: HasFTaylorSeriesUpToOn.zero_eq, ContinuousMultilinearMap.curry0
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries.{u_1, uE, u_5} 𝕜 E (F' i)
n : ℕ∞ω
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj (φ := F')
L : (m : ℕ) →
  ((i : ι) → ContinuousMultilinearMap.{u_1, 0, uE, u_5} 𝕜 (fun (i : Fin m) ↦ E) (F' i)) ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i) :=
  fun (m : ℕ) ↦ ContinuousMultilinearMap.piₗᵢ 𝕜 fun (i : Fin m) ↦ E (E' := F')
h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
x : E
hx : x ∈ s
i : ι
⊢ ContinuousMultilinearMap.curry0 (𝕜 := 𝕜) (G := E)
      (ContinuousMultilinearMap.pi (M₁ := fun (i : Fin 0) ↦ E) (M' := F') fun (i : ι) ↦ p' i x 0) i =
    φ i x

Tactic:
exact (h i).zero_eq x hx

Premises used: HasFTaylorSeriesUpToOn.zero_eq
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries.{u_1, uE, u_5} 𝕜 E (F' i)
n : ℕ∞ω
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj (φ := F')
L : (m : ℕ) →
  ((i : ι) → ContinuousMultilinearMap.{u_1, 0, uE, u_5} 𝕜 (fun (i : Fin m) ↦ E) (F' i)) ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i) :=
  fun (m : ℕ) ↦ ContinuousMultilinearMap.piₗᵢ 𝕜 fun (i : Fin m) ↦ E (E' := F')
h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i))
    (fun (x : E) ↦ ContinuousMultilinearMap.pi (M₁ := fun (i : Fin m) ↦ E) (M' := F') fun (i : ι) ↦ p' i x m)
    (ContinuousMultilinearMap.curryLeft (𝕜 := 𝕜) (Ei := fun (i : Fin m.succ) ↦ E) (G := (i : ι) → F' i)
      (ContinuousMultilinearMap.pi (M₁ := fun (i : Fin m.succ) ↦ E) (M' := F') fun (i : ι) ↦ p' i x m.succ))
    s x

Tactic:
(L m).hasFDerivAt.comp_hasFDerivWithinAt x <|
      hasFDerivWithinAt_pi.2 fun i => (h i).fderivWithin m hm x hx

Premises used: Iff.mpr, HasFDerivAt.comp_hasFDerivWithinAt, MultilinearMap.pi, ContinuousMultilinearMap.pi, ContinuousMultilinearMap.curryLeft, MultilinearMap.mkContinuous, HasFTaylorSeriesUpToOn.fderivWithin, LinearIsometryEquiv.hasFDerivAt, MultilinearMap.mk', hasFDerivWithinAt_pi, MultilinearMap.mkContinuousLinear, LinearMap.mkContinuous
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries.{u_1, uE, u_5} 𝕜 E (F' i)
n : ℕ∞ω
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj (φ := F')
L : (m : ℕ) →
  ((i : ι) → ContinuousMultilinearMap.{u_1, 0, uE, u_5} 𝕜 (fun (i : Fin m) ↦ E) (F' i)) ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i) :=
  fun (m : ℕ) ↦ ContinuousMultilinearMap.piₗᵢ 𝕜 fun (i : Fin m) ↦ E (E' := F')
h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i))
    (fun (x : E) ↦ ContinuousMultilinearMap.pi (M₁ := fun (i : Fin m) ↦ E) (M' := F') fun (i : ι) ↦ p' i x m)
    (ContinuousMultilinearMap.curryLeft (𝕜 := 𝕜) (Ei := fun (i : Fin m.succ) ↦ E) (G := (i : ι) → F' i)
      (ContinuousMultilinearMap.pi (M₁ := fun (i : Fin m.succ) ↦ E) (M' := F') fun (i : ι) ↦ p' i x m.succ))
    s x

Tactic:
exact (L m).hasFDerivAt.comp_hasFDerivWithinAt x <|
      hasFDerivWithinAt_pi.2 fun i => (h i).fderivWithin m hm x hx

Premises used: Iff.mpr, HasFDerivAt.comp_hasFDerivWithinAt, HasFTaylorSeriesUpToOn.fderivWithin, LinearIsometryEquiv.hasFDerivAt, hasFDerivWithinAt_pi
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries.{u_1, uE, u_5} 𝕜 E (F' i)
n : ℕ∞ω
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj (φ := F')
L : (m : ℕ) →
  ((i : ι) → ContinuousMultilinearMap.{u_1, 0, uE, u_5} 𝕜 (fun (i : Fin m) ↦ E) (F' i)) ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i) :=
  fun (m : ℕ) ↦ ContinuousMultilinearMap.piₗᵢ 𝕜 fun (i : Fin m) ↦ E (E' := F')
h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
⊢ ContinuousOn (Y := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i))
    (fun (x : E) ↦ ContinuousMultilinearMap.pi (M₁ := fun (i : Fin m) ↦ E) (M' := F') fun (i : ι) ↦ p' i x m) s

Tactic:
(L m).continuous.comp_continuousOn <| continuousOn_pi.2 fun i => (h i).cont m hm

Premises used: Iff.mpr, Continuous.comp_continuousOn, HasFTaylorSeriesUpToOn.cont, ContinuousMultilinearMap.pi, LinearIsometryEquiv.continuous, continuousOn_pi
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries.{u_1, uE, u_5} 𝕜 E (F' i)
n : ℕ∞ω
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj (φ := F')
L : (m : ℕ) →
  ((i : ι) → ContinuousMultilinearMap.{u_1, 0, uE, u_5} 𝕜 (fun (i : Fin m) ↦ E) (F' i)) ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i) :=
  fun (m : ℕ) ↦ ContinuousMultilinearMap.piₗᵢ 𝕜 fun (i : Fin m) ↦ E (E' := F')
h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
⊢ ContinuousOn (Y := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i))
    (fun (x : E) ↦ ContinuousMultilinearMap.pi (M₁ := fun (i : Fin m) ↦ E) (M' := F') fun (i : ι) ↦ p' i x m) s

Tactic:
exact (L m).continuous.comp_continuousOn <| continuousOn_pi.2 fun i => (h i).cont m hm

Premises used: Iff.mpr, Continuous.comp_continuousOn, HasFTaylorSeriesUpToOn.cont, LinearIsometryEquiv.continuous, continuousOn_pi
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)
n : ℕ∞ω
⊢ HasFTaylorSeriesUpToOn (𝕜 := 𝕜) (F := (i : ι) → F' i) n (fun (x : E) (i : ι) ↦ Φ x i)
      (fun (x : E) (m : ℕ) ↦
        ContinuousMultilinearMap.pi (M₁ := fun (i : Fin m) ↦ E) (M' := F') fun (i : ι) ↦
          ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin m) ↦ E)
            (ContinuousLinearMap.proj (φ := F') i) (P' x m))
      s ↔
    ∀ (i : ι),
      HasFTaylorSeriesUpToOn.{u_1, uE, u_5} (𝕜 := 𝕜) (F := F' i) n (fun (x : E) ↦ Φ x i)
        (fun (x : E) (m : ℕ) ↦
          ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin m) ↦ E)
            (ContinuousLinearMap.proj (φ := F') i) (P' x m))
        s

Tactic:
hasFTaylorSeriesUpToOn_pi (𝕜 := 𝕜) (φ := fun i x ↦ Φ x i)

Premises used: hasFTaylorSeriesUpToOn_pi
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)
n : ℕ∞ω
h :
  ∀ (x : E) (x_1 : ℕ),
    P' x x_1 =
      ContinuousMultilinearMap.pi (M₁ := fun (i : Fin x_1) ↦ E) (M' := F') fun (i : ι) ↦
        ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin x_1) ↦ E)
          (ContinuousLinearMap.proj (φ := F') i) (P' x x_1)
⊢ HasFTaylorSeriesUpToOn (𝕜 := 𝕜) n Φ P' s ↔
    ∀ (i : ι),
      HasFTaylorSeriesUpToOn.{u_1, uE, u_5} (𝕜 := 𝕜) (F := F' i) n (fun (x : E) ↦ Φ x i)
        (fun (x : E) (m : ℕ) ↦
          ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin m) ↦ E)
            (ContinuousLinearMap.proj (φ := F') i) (P' x m))
        s

Tactic:
convert! hasFTaylorSeriesUpToOn_pi (𝕜 := 𝕜) (φ := fun i x ↦ Φ x i)

Premises used: hasFTaylorSeriesUpToOn_pi
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)
n : ℕ∞ω
x : E
x_1 : ℕ
h :
  ∀ (x_2 : (i : Fin x_1) → E) (x_3 : ι),
    Eq.{u_5 + 1} (α := F' x_3) ((P' x x_1 : (a : (i : Fin x_1) → E) → (i : ι) → F' i) x_2 x_3 : F' x_3)
      (((ContinuousMultilinearMap.pi (M₁ := fun (i : Fin x_1) ↦ E) (M' := F') fun (i : ι) ↦
                ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin x_1) ↦ E)
                  (ContinuousLinearMap.proj (φ := F') i) (P' x x_1) :
              ContinuousMultilinearMap 𝕜 (fun (i : Fin x_1) ↦ E) ((i : ι) → F' i)) :
            (a : (i : Fin x_1) → E) → (i : ι) → F' i)
          x_2 x_3 :
        F' x_3)
⊢ P' x x_1 =
    ContinuousMultilinearMap.pi (M₁ := fun (i : Fin x_1) ↦ E) (M' := F') fun (i : ι) ↦
      ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin x_1) ↦ E)
        (ContinuousLinearMap.proj (φ := F') i) (P' x x_1)

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)
n : ℕ∞ω
x : E
x_1 : ℕ
x_2 : (i : Fin x_1) → E
x_3 : ι
⊢ Eq.{u_5 + 1} (α := F' x_3) ((P' x x_1 : (a : (i : Fin x_1) → E) → (i : ι) → F' i) x_2 x_3 : F' x_3)
    (((ContinuousMultilinearMap.pi (M₁ := fun (i : Fin x_1) ↦ E) (M' := F') fun (i : ι) ↦
              ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin x_1) ↦ E)
                (ContinuousLinearMap.proj (φ := F') i) (P' x x_1) :
            ContinuousMultilinearMap 𝕜 (fun (i : Fin x_1) ↦ E) ((i : ι) → F' i)) :
          (a : (i : Fin x_1) → E) → (i : ι) → F' i)
        x_2 x_3 :
      F' x_3)

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
n : ℕ∞ω
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj (φ := F')
⊢ ContDiffWithinAt 𝕜 n Φ s x ↔ ∀ (i : ι), ContDiffWithinAt.{u_1, uE, u_5} 𝕜 (F := F' i) n (fun (x : E) ↦ Φ x i) s x

Tactic:
⟨fun h i => h.continuousLinearMap_comp (pr i), fun h ↦ ?_⟩

Premises used: ContDiffWithinAt.continuousLinearMap_comp, Iff.intro
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
n : ℕ∞ω
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj (φ := F')
refine :
  ∀ (h : ∀ (i : ι), ContDiffWithinAt.{u_1, uE, u_5} 𝕜 (F := F' i) n (fun (x : E) ↦ Φ x i) s x),
    ContDiffWithinAt 𝕜 n Φ s x
⊢ ContDiffWithinAt 𝕜 n Φ s x ↔ ∀ (i : ι), ContDiffWithinAt.{u_1, uE, u_5} 𝕜 (F := F' i) n (fun (x : E) ↦ Φ x i) s x

Tactic:
refine ⟨fun h i => h.continuousLinearMap_comp (pr i), fun h ↦ ?_⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
n : ℕ∞ω
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj (φ := F')
h : ∀ (i : ι), ContDiffWithinAt.{u_1, uE, u_5} 𝕜 (F := F' i) ω (fun (x : E) ↦ Φ x i) s x
choose :
  ∀ (u : (i : ι) → Set E) (hux : ∀ (i : ι), u i ∈ 𝓝[insert x s] x)
    (p : (i : ι) → E → FormalMultilinearSeries.{u_1, uE, u_5} 𝕜 E (F' i))
    (hp : ∀ (i : ι), HasFTaylorSeriesUpToOn ω (fun (x : E) ↦ Φ x i) (p i) (u i))
    (h'p :
      ∀ (i : ι) (i_1 : ℕ),
        AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, uE, u_5} 𝕜 (fun (i : Fin i_1) ↦ E) (F' i))
          (fun (x : E) ↦ p i x i_1) (u i)),
    ContDiffWithinAt 𝕜 ω Φ s x
⊢ ContDiffWithinAt 𝕜 ω Φ s x

Tactic:
choose u hux p hp h'p using h
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
n : ℕ∞ω
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj (φ := F')
u : (i : ι) → Set E
hux : ∀ (i : ι), u i ∈ 𝓝[insert x s] x
p : (i : ι) → E → FormalMultilinearSeries.{u_1, uE, u_5} 𝕜 E (F' i)
hp : ∀ (i : ι), HasFTaylorSeriesUpToOn ω (fun (x : E) ↦ Φ x i) (p i) (u i)
h'p :
  ∀ (i : ι) (i_1 : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, uE, u_5} 𝕜 (fun (i : Fin i_1) ↦ E) (F' i))
      (fun (x : E) ↦ p i x i_1) (u i)
⊢ ContDiffWithinAt 𝕜 ω Φ s x

Tactic:
⟨⋂ i, u i, Filter.iInter_mem.2 hux, _,
      hasFTaylorSeriesUpToOn_pi.2 fun i => (hp i).mono <| iInter_subset _ _, fun m ↦ ?_⟩

Premises used: Iff.mpr, Set.iInter, HasFTaylorSeriesUpToOn.mono, Filter.iInter_mem, And.intro, Exists.intro, Set.iInter_subset, ContDiffWithinAt, hasFTaylorSeriesUpToOn_pi
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
n : ℕ∞ω
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj (φ := F')
u : (i : ι) → Set E
hux : ∀ (i : ι), u i ∈ 𝓝[insert x s] x
p : (i : ι) → E → FormalMultilinearSeries.{u_1, uE, u_5} 𝕜 E (F' i)
hp : ∀ (i : ι), HasFTaylorSeriesUpToOn ω (fun (x : E) ↦ Φ x i) (p i) (u i)
h'p :
  ∀ (i : ι) (i_1 : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, uE, u_5} 𝕜 (fun (i : Fin i_1) ↦ E) (F' i))
      (fun (x : E) ↦ p i x i_1) (u i)
refine :
  ∀ (m : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i))
      (fun (x : E) ↦ ContinuousMultilinearMap.pi (M₁ := fun (i : Fin m) ↦ E) (M' := F') fun (i : ι) ↦ p i x m)
      (⋂ (i : ι), u i)
⊢ ContDiffWithinAt 𝕜 ω Φ s x

Tactic:
refine ⟨⋂ i, u i, Filter.iInter_mem.2 hux, _,
      hasFTaylorSeriesUpToOn_pi.2 fun i => (hp i).mono <| iInter_subset _ _, fun m ↦ ?_⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
n : ℕ∞ω
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj (φ := F')
u : (i : ι) → Set E
hux : ∀ (i : ι), u i ∈ 𝓝[insert x s] x
p : (i : ι) → E → FormalMultilinearSeries.{u_1, uE, u_5} 𝕜 E (F' i)
hp : ∀ (i : ι), HasFTaylorSeriesUpToOn ω (fun (x : E) ↦ Φ x i) (p i) (u i)
h'p :
  ∀ (i : ι) (i_1 : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, uE, u_5} 𝕜 (fun (i : Fin i_1) ↦ E) (F' i))
      (fun (x : E) ↦ p i x i_1) (u i)
m : ℕ
L : ((i : ι) → ContinuousMultilinearMap.{u_1, 0, uE, u_5} 𝕜 (fun (i : Fin m) ↦ E) (F' i)) ≃ₗᵢ[𝕜]
  ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i) :=
  ContinuousMultilinearMap.piₗᵢ 𝕜 fun (i : Fin m) ↦ E (E' := F')
change :
  AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i))
    (fun (x : E) ↦
      (L :
          (a : (i : ι) → ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (F' i)) →
            ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i))
        fun (i : ι) ↦ p i x m)
    (⋂ (i : ι), u i)
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i))
    (fun (x : E) ↦ ContinuousMultilinearMap.pi (M₁ := fun (i : Fin m) ↦ E) (M' := F') fun (i : ι) ↦ p i x m)
    (⋂ (i : ι), u i)

Tactic:
change AnalyticOn 𝕜 (fun x ↦ L (fun i ↦ p i x m)) (⋂ i, u i)

Premises used: AnalyticOn, Set.iInter, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
n : ℕ∞ω
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj (φ := F')
u : (i : ι) → Set E
hux : ∀ (i : ι), u i ∈ 𝓝[insert x s] x
p : (i : ι) → E → FormalMultilinearSeries.{u_1, uE, u_5} 𝕜 E (F' i)
hp : ∀ (i : ι), HasFTaylorSeriesUpToOn ω (fun (x : E) ↦ Φ x i) (p i) (u i)
h'p :
  ∀ (i : ι) (i_1 : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, uE, u_5} 𝕜 (fun (i : Fin i_1) ↦ E) (F' i))
      (fun (x : E) ↦ p i x i_1) (u i)
m : ℕ
L : ((i : ι) → ContinuousMultilinearMap.{u_1, 0, uE, u_5} 𝕜 (fun (i : Fin m) ↦ E) (F' i)) ≃ₗᵢ[𝕜]
  ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i) :=
  ContinuousMultilinearMap.piₗᵢ 𝕜 fun (i : Fin m) ↦ E (E' := F')
apply :
  AnalyticOn 𝕜 (F := (i : ι) → ContinuousMultilinearMap.{u_1, 0, uE, u_5} 𝕜 (fun (i : Fin m) ↦ E) (F' i))
    (fun (x : E) (i : ι) ↦ p i x m) (⋂ (i : ι), u i)
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i))
    (fun (x : E) ↦
      (L :
          (a : (i : ι) → ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (F' i)) →
            ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i))
        fun (i : ι) ↦ p i x m)
    (⋂ (i : ι), u i)

Tactic:
apply (L.analyticOnNhd univ).comp_analyticOn ?_ (mapsTo_univ _ _)

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