awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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
⊢ 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
have 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
Tactic: apply continuousOn_pi.2 (fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
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
⊢ 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
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FiniteDimension (goal)
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
have 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
Tactic: refine ⟨fun h y => h.clm_apply contDiffOn_const, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FiniteDimension (hypothesis)
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
⊢ ContDiffOn 𝕜 n f s
have hd : d = finrank 𝕜 (Fin d → 𝕜)
Tactic: have hd : d = finrank 𝕜 (Fin d → 𝕜) := (finrank_fin_fun 𝕜).symm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FiniteDimension (goal)
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 𝕜 n f s
have 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
Tactic: rw [← id_comp f, ← e₂.symm_comp_self]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FiniteDimension (goal)
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
⊢ ContDiff 𝕜 n f ↔ ∀ (y : E), ContDiff.{u_1, uD, uF} 𝕜 (F := F) n fun (x : D) ↦ (f x : (a : E) → F) y
have 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
Tactic: simp_rw [← contDiffOn_univ, contDiffOn_clm_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FiniteDimension (goal)
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
⊢ 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
have 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
Tactic: rw [contDiff_succ_iff_fderiv, contDiff_clm_apply_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FiniteDimension (goal)
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
⊢ 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
have 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
Tactic: rw [contDiff_succ_iff_fderiv, contDiff_clm_apply_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FiniteDimension (goal)
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
⊢ 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
have 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
Tactic: rw [contDiffOn_succ_iff_fderivWithin hs, contDiffOn_clm_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FiniteDimension (goal)
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
⊢ 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
have 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
Tactic: rw [contDiffOn_succ_iff_fderivWithin hs, contDiffOn_clm_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
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
have 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
Tactic: refine ⟨fun h i => ?_, fun h => ⟨fun x hx => ?_, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
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
⊢ 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
have 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
Tactic: refine ⟨fun h i => ?_, fun h => ⟨fun x hx => ?_, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
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
⊢ 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
have 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
Tactic: refine ⟨fun h i => ?_, fun h => ⟨fun x hx => ?_, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
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
⊢ 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
have 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
Tactic: refine ⟨fun h i => ?_, fun h => ⟨fun x hx => ?_, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
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
⊢ 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
have 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
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
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 (𝕜 := 𝕜) 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
have 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)
Tactic: convert! hasFTaylorSeriesUpToOn_pi (𝕜 := 𝕜) (φ := fun i x ↦ Φ x i)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
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 : ℕ
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
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
have refine : ∀ (h : ∀ (i : ι), ContDiffWithinAt.{u_1, uE, u_5} 𝕜 (F := F' i) n (fun (x : E) ↦ Φ x i) s x), ContDiffWithinAt 𝕜 n Φ s x
Tactic: refine ⟨fun h i => h.continuousLinearMap_comp (pr i), fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
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
⊢ ContDiffWithinAt 𝕜 ω Φ s x
have 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
Tactic: choose u hux p hp h'p using h
Cleared hypotheses: h