awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : (↑m : WithTop ℕ∞) ≤ n
c : OrderedFinpartition m
h_1 : Membership.mem (γ := Finset (OrderedFinpartition m)) Finset.univ c
B : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜
    (fun (i : Fin c.length) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
    (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G) :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
this : LE.le (α := WithTop ℕ∞) (↑c.length : WithTop ℕ∞) (↑m : WithTop ℕ∞)
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G)
    (fun (x : E) ↦ q (f x) c.length) s

Tactic:
(hg.cont c.length (this.trans hm)).comp hf.continuousOn h

Premises used: HasFTaylorSeriesUpToOn.cont, HasFTaylorSeriesUpToOn.continuousOn, ContinuousOn.comp, LE.le.trans, OrderedFinpartition.length
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : (↑m : WithTop ℕ∞) ≤ n
c : OrderedFinpartition m
h_1 : Membership.mem (γ := Finset (OrderedFinpartition m)) Finset.univ c
B : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜
    (fun (i : Fin c.length) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
    (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G) :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
this : LE.le (α := WithTop ℕ∞) (↑c.length : WithTop ℕ∞) (↑m : WithTop ℕ∞)
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G)
    (fun (x : E) ↦ q (f x) c.length) s

Tactic:
exact (hg.cont c.length (this.trans hm)).comp hf.continuousOn h

Premises used: HasFTaylorSeriesUpToOn.cont, HasFTaylorSeriesUpToOn.continuousOn, ContinuousOn.comp, LE.le.trans, OrderedFinpartition.length
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : (↑m : WithTop ℕ∞) ≤ n
c : OrderedFinpartition m
h_1 : Membership.mem (γ := Finset (OrderedFinpartition m)) Finset.univ c
B : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜
    (fun (i : Fin c.length) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
    (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G) :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
apply :
  ∀ (i : Fin c.length),
    ContinuousOn (Y := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
      (fun (y : E) ↦ p y (c.partSize i)) s
⊢ ContinuousOn (Y :=
    (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
    (fun (x : E) (i : Fin c.length) ↦ p x (c.partSize i)) s

Tactic:
apply continuousOn_pi.2 (fun i ↦ ?_)

Premises used: Iff.mpr, continuousOn_pi
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : (↑m : WithTop ℕ∞) ≤ n
c : OrderedFinpartition m
h_1 : Membership.mem (γ := Finset (OrderedFinpartition m)) Finset.univ c
B : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜
    (fun (i : Fin c.length) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
    (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G) :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
i : Fin c.length
⊢ LE.le (α := WithTop ℕ∞) (↑(c.partSize i) : WithTop ℕ∞) (↑m : WithTop ℕ∞)

Tactic:
exact_mod_cast OrderedFinpartition.partSize_le c i

Premises used: OrderedFinpartition.partSize_le
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : (↑m : WithTop ℕ∞) ≤ n
c : OrderedFinpartition m
h_1 : Membership.mem (γ := Finset (OrderedFinpartition m)) Finset.univ c
B : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜
    (fun (i : Fin c.length) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
    (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G) :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
i : Fin c.length
⊢ LE.le (α := WithTop ℕ∞) (↑(c.partSize i) : WithTop ℕ∞) (↑m : WithTop ℕ∞)

Tactic:
have : (c.partSize i : WithTop ℕ∞) ≤ m := by
        exact_mod_cast OrderedFinpartition.partSize_le c i
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : (↑m : WithTop ℕ∞) ≤ n
c : OrderedFinpartition m
h_1 : Membership.mem (γ := Finset (OrderedFinpartition m)) Finset.univ c
B : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜
    (fun (i : Fin c.length) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
    (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G) :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
i : Fin c.length
this : LE.le (α := WithTop ℕ∞) (↑(c.partSize i) : WithTop ℕ∞) (↑m : WithTop ℕ∞)
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
    (fun (y : E) ↦ p y (c.partSize i)) s

Tactic:
hf.cont _ (this.trans hm)

Premises used: HasFTaylorSeriesUpToOn.cont, LE.le.trans
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : (↑m : WithTop ℕ∞) ≤ n
c : OrderedFinpartition m
h_1 : Membership.mem (γ := Finset (OrderedFinpartition m)) Finset.univ c
B : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜
    (fun (i : Fin c.length) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
    (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G) :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
i : Fin c.length
this : LE.le (α := WithTop ℕ∞) (↑(c.partSize i) : WithTop ℕ∞) (↑m : WithTop ℕ∞)
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
    (fun (y : E) ↦ p y (c.partSize i)) s

Tactic:
exact hf.cont _ (this.trans hm)

Premises used: HasFTaylorSeriesUpToOn.cont, LE.le.trans
-- Module: Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
D : Type uD
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace 𝕜 D
E : Type uE
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
F : Type uF
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_7 : CompleteSpace 𝕜
f : D → E →L[𝕜] F
s : Set D
inst_8 : FiniteDimensional 𝕜 E
⊢ ContDiffOn 𝕜 n f s ↔ ∀ (y : E), ContDiffOn.{u_1, uD, uF} 𝕜 (F := F) n (fun (x : D) ↦ (f x : (a : E) → F) y) s

Tactic:
⟨fun h y => h.clm_apply contDiffOn_const, fun h => ?_⟩

Premises used: ContDiffOn.clm_apply, Iff.intro, contDiffOn_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
D : Type uD
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace 𝕜 D
E : Type uE
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
F : Type uF
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_7 : CompleteSpace 𝕜
f : D → E →L[𝕜] F
s : Set D
inst_8 : FiniteDimensional 𝕜 E
refine :
  ∀ (h : ∀ (y : E), ContDiffOn.{u_1, uD, uF} 𝕜 (F := F) n (fun (x : D) ↦ (f x : (a : E) → F) y) s), ContDiffOn 𝕜 n f s
⊢ ContDiffOn 𝕜 n f s ↔ ∀ (y : E), ContDiffOn.{u_1, uD, uF} 𝕜 (F := F) n (fun (x : D) ↦ (f x : (a : E) → F) y) s

Tactic:
refine ⟨fun h y => h.clm_apply contDiffOn_const, fun h => ?_⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
D : Type uD
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace 𝕜 D
E : Type uE
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
F : Type uF
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_7 : CompleteSpace 𝕜
f : D → E →L[𝕜] F
s : Set D
inst_8 : FiniteDimensional 𝕜 E
h : ∀ (y : E), ContDiffOn.{u_1, uD, uF} 𝕜 (F := F) n (fun (x : D) ↦ (f x : (a : E) → F) y) s
d : ℕ := finrank 𝕜 E
⊢ d = finrank 𝕜 (Fin d → 𝕜)

Tactic:
have hd : d = finrank 𝕜 (Fin d → 𝕜) := (finrank_fin_fun 𝕜).symm
-- Module: Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
D : Type uD
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace 𝕜 D
E : Type uE
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
F : Type uF
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_7 : CompleteSpace 𝕜
f : D → E →L[𝕜] F
s : Set D
inst_8 : FiniteDimensional 𝕜 E
h : ∀ (y : E), ContDiffOn.{u_1, uD, uF} 𝕜 (F := F) n (fun (x : D) ↦ (f x : (a : E) → F) y) s
d : ℕ := finrank 𝕜 E
hd : d = finrank 𝕜 (Fin d → 𝕜)
e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq.{u_1, uE, u_1} (𝕜 := 𝕜) (E := E) (F := Fin d → 𝕜) hd
e₂ : (E →L[𝕜] F) ≃L[𝕜] Fin d → F :=
  ContinuousLinearEquiv.trans (M₂ := (Fin d → 𝕜) →L[𝕜] F)
    (ContinuousLinearEquiv.arrowCongr.{u_1, uE, u_1, uF, uF} (𝕜 := 𝕜) (E := E) (F := Fin d → 𝕜) (G := F) (H := F) e₁ 1)
    (ContinuousLinearEquiv.piRing (Fin d))
rw :
  ContDiffOn 𝕜 (F := E →L[𝕜] F) n
    (comp (β := Fin d → F) (⇑e₂.symm : (a : Fin d → F) → E →L[𝕜] F) (⇑e₂ : (a : E →L[𝕜] F) → Fin d → F) ∘ f) s
⊢ ContDiffOn 𝕜 n f s

Tactic:
rw [← id_comp f, ← e₂.symm_comp_self]

Premises used: ContinuousLinearEquiv.symm_comp_self, Function.id_comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
D : Type uD
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace 𝕜 D
E : Type uE
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
F : Type uF
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_7 : CompleteSpace 𝕜
f : D → E →L[𝕜] F
s : Set D
inst_8 : FiniteDimensional 𝕜 E
h : ∀ (y : E), ContDiffOn.{u_1, uD, uF} 𝕜 (F := F) n (fun (x : D) ↦ (f x : (a : E) → F) y) s
d : ℕ := finrank 𝕜 E
hd : d = finrank 𝕜 (Fin d → 𝕜)
e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq.{u_1, uE, u_1} (𝕜 := 𝕜) (E := E) (F := Fin d → 𝕜) hd
e₂ : (E →L[𝕜] F) ≃L[𝕜] Fin d → F :=
  ContinuousLinearEquiv.trans (M₂ := (Fin d → 𝕜) →L[𝕜] F)
    (ContinuousLinearEquiv.arrowCongr.{u_1, uE, u_1, uF, uF} (𝕜 := 𝕜) (E := E) (F := Fin d → 𝕜) (G := F) (H := F) e₁ 1)
    (ContinuousLinearEquiv.piRing (Fin d))
⊢ ContDiffOn 𝕜 (F := E →L[𝕜] F) n
    (comp (β := Fin d → F) (⇑e₂.symm : (a : Fin d → F) → E →L[𝕜] F) (⇑e₂ : (a : E →L[𝕜] F) → Fin d → F) ∘ f) s

Tactic:
e₂.symm.contDiff.comp_contDiffOn (contDiffOn_pi.mpr fun i => h _)

Premises used: Iff.mpr, ContDiff.comp_contDiffOn, ContinuousLinearEquiv.symm, LinearMap.single, ContinuousLinearMap.toLinearMap, contDiffOn_pi, OfNat.ofNat, DFunLike.coe, ContinuousLinearEquiv.toContinuousLinearMap, ContinuousLinearEquiv.contDiff
-- Module: Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
D : Type uD
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace 𝕜 D
E : Type uE
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
F : Type uF
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_7 : CompleteSpace 𝕜
f : D → E →L[𝕜] F
s : Set D
inst_8 : FiniteDimensional 𝕜 E
h : ∀ (y : E), ContDiffOn.{u_1, uD, uF} 𝕜 (F := F) n (fun (x : D) ↦ (f x : (a : E) → F) y) s
d : ℕ := finrank 𝕜 E
hd : d = finrank 𝕜 (Fin d → 𝕜)
e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq.{u_1, uE, u_1} (𝕜 := 𝕜) (E := E) (F := Fin d → 𝕜) hd
e₂ : (E →L[𝕜] F) ≃L[𝕜] Fin d → F :=
  ContinuousLinearEquiv.trans (M₂ := (Fin d → 𝕜) →L[𝕜] F)
    (ContinuousLinearEquiv.arrowCongr.{u_1, uE, u_1, uF, uF} (𝕜 := 𝕜) (E := E) (F := Fin d → 𝕜) (G := F) (H := F) e₁ 1)
    (ContinuousLinearEquiv.piRing (Fin d))
⊢ ContDiffOn 𝕜 (F := E →L[𝕜] F) n
    (comp (β := Fin d → F) (⇑e₂.symm : (a : Fin d → F) → E →L[𝕜] F) (⇑e₂ : (a : E →L[𝕜] F) → Fin d → F) ∘ f) s

Tactic:
exact e₂.symm.contDiff.comp_contDiffOn (contDiffOn_pi.mpr fun i => h _)

Premises used: Iff.mpr, ContDiff.comp_contDiffOn, ContinuousLinearEquiv.symm, contDiffOn_pi, ContinuousLinearEquiv.contDiff
-- Module: Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
D : Type uD
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace 𝕜 D
E : Type uE
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
F : Type uF
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_7 : CompleteSpace 𝕜
f : D → E →L[𝕜] F
inst_8 : FiniteDimensional 𝕜 E
simp_rw :
  ContDiffOn 𝕜 n f Set.univ ↔
    ∀ (y : E), ContDiffOn.{u_1, uD, uF} 𝕜 (F := F) n (fun (x : D) ↦ (f x : (a : E) → F) y) Set.univ
⊢ ContDiff 𝕜 n f ↔ ∀ (y : E), ContDiff.{u_1, uD, uF} 𝕜 (F := F) n fun (x : D) ↦ (f x : (a : E) → F) y

Tactic:
simp_rw [← contDiffOn_univ, contDiffOn_clm_apply]

Premises used: contDiffOn_clm_apply, contDiffOn_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
D : Type uD
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace 𝕜 D
E : Type uE
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
n : ℕ∞ω
f : D → E
inst_5 : CompleteSpace 𝕜
inst_6 : FiniteDimensional 𝕜 D
rw :
  Differentiable 𝕜 f ∧ (n = ω → AnalyticOnNhd 𝕜 f Set.univ) ∧ ContDiff 𝕜 (F := D →L[𝕜] E) n (fderiv 𝕜 f) ↔
    Differentiable 𝕜 f ∧
      (n = ω → AnalyticOnNhd 𝕜 f Set.univ) ∧
        ∀ (y : D), ContDiff.{u_1, uD, uE} 𝕜 (F := E) n fun (x : D) ↦ (fderiv 𝕜 f x : (a : D) → E) y
rw₁ rw₂ :
  (Differentiable 𝕜 f ∧
      (n = ω → AnalyticOnNhd 𝕜 f Set.univ) ∧
        ∀ (y : D), ContDiff.{u_1, uD, uE} 𝕜 (F := E) n fun (x : D) ↦ (fderiv 𝕜 f x : (a : D) → E) y) ↔
    Differentiable 𝕜 f ∧
      (n = ω → AnalyticOnNhd 𝕜 f Set.univ) ∧
        ∀ (y : D), ContDiff.{u_1, uD, uE} 𝕜 (F := E) n fun (x : D) ↦ (fderiv 𝕜 f x : (a : D) → E) y
⊢ ContDiff 𝕜 (n + 1) f ↔
    Differentiable 𝕜 f ∧
      (n = ω → AnalyticOnNhd 𝕜 f Set.univ) ∧
        ∀ (y : D), ContDiff.{u_1, uD, uE} 𝕜 (F := E) n fun (x : D) ↦ (fderiv 𝕜 f x : (a : D) → E) y

Tactic:
rw [contDiff_succ_iff_fderiv, contDiff_clm_apply_iff]

Premises used: contDiff_succ_iff_fderiv, contDiff_clm_apply_iff
-- Module: Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
D : Type uD
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace 𝕜 D
E : Type uE
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
n : ℕ∞ω
f : D → E
s : Set D
inst_5 : CompleteSpace 𝕜
inst_6 : FiniteDimensional 𝕜 D
hf : DifferentiableOn 𝕜 f s
h'f : n = ω → AnalyticOn 𝕜 f s
h : ∀ (y : D), ContDiffOn.{u_1, uD, uE} 𝕜 (F := E) n (fun (x : D) ↦ (fderivWithin 𝕜 f s x : (a : D) → E) y) s
⊢ ContDiffOn 𝕜 (n + 1) f s

Tactic:
contDiffOn_succ_of_fderivWithin hf h'f <| contDiffOn_clm_apply.mpr h

Premises used: Iff.mpr, contDiffOn_succ_of_fderivWithin, contDiffOn_clm_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
D : Type uD
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace 𝕜 D
E : Type uE
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
n : ℕ∞ω
f : D → E
s : Set D
inst_5 : CompleteSpace 𝕜
inst_6 : FiniteDimensional 𝕜 D
hs : UniqueDiffOn 𝕜 s
rw :
  DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 (F := D →L[𝕜] E) n (fderivWithin 𝕜 f s) s ↔
    DifferentiableOn 𝕜 f s ∧
      (n = ω → AnalyticOn 𝕜 f s) ∧
        ∀ (y : D), ContDiffOn.{u_1, uD, uE} 𝕜 (F := E) n (fun (x : D) ↦ (fderivWithin 𝕜 f s x : (a : D) → E) y) s
rw₁ rw₂ :
  (DifferentiableOn 𝕜 f s ∧
      (n = ω → AnalyticOn 𝕜 f s) ∧
        ∀ (y : D), ContDiffOn.{u_1, uD, uE} 𝕜 (F := E) n (fun (x : D) ↦ (fderivWithin 𝕜 f s x : (a : D) → E) y) s) ↔
    DifferentiableOn 𝕜 f s ∧
      (n = ω → AnalyticOn 𝕜 f s) ∧
        ∀ (y : D), ContDiffOn.{u_1, uD, uE} 𝕜 (F := E) n (fun (x : D) ↦ (fderivWithin 𝕜 f s x : (a : D) → E) y) s
⊢ ContDiffOn 𝕜 (n + 1) f s ↔
    DifferentiableOn 𝕜 f s ∧
      (n = ω → AnalyticOn 𝕜 f s) ∧
        ∀ (y : D), ContDiffOn.{u_1, uD, uE} 𝕜 (F := E) n (fun (x : D) ↦ (fderivWithin 𝕜 f s x : (a : D) → E) y) s

Tactic:
rw [contDiffOn_succ_iff_fderivWithin hs, contDiffOn_clm_apply]

Premises used: contDiffOn_clm_apply, contDiffOn_succ_iff_fderivWithin
-- 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')
⊢ 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:
⟨fun h i => ?_, fun h => ⟨fun x hx => ?_, ?_, ?_⟩⟩

Premises used: Iff.intro, HasFTaylorSeriesUpToOn.mk
-- 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')
refine_1 :
  ∀
    (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
refine_2 :
  ∀ (h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s) (x : E) (hx : x ∈ s),
    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
refine_3 :
  ∀ (h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s) (m : ℕ),
    (↑m : ℕ∞ω) < n →
      ∀ 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
refine_4 :
  ∀ (h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s) (m : ℕ),
    (↑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
⊢ 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:
refine ⟨fun h i => ?_, fun h => ⟨fun x hx => ?_, ?_, ?_⟩⟩
-- 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:
h.continuousLinearMap_comp (pr i)

Premises used: ContinuousLinearMap.compContinuousMultilinearMap, HasFTaylorSeriesUpToOn.continuousLinearMap_comp, LinearMap.compMultilinearMap