-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem hasFTaylorSeriesUpToOn_pi {n : WithTop ℕ∞} :
    HasFTaylorSeriesUpToOn n (fun x i => φ i x)
        (fun x m => ContinuousMultilinearMap.pi fun i => p' i x m) s ↔
      ∀ i, HasFTaylorSeriesUpToOn n (φ i) (p' i) s

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
n : WithTop ℕ∞
⊢ HasFTaylorSeriesUpToOn n (fun x i => φ i x) (fun x m => ContinuousMultilinearMap.pi fun i => p' i x m) s ↔
    ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s

Tactic:
set pr := @ContinuousLinearMap.proj 𝕜 _ ι F' _ _ _

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
n : WithTop ℕ∞
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
⊢ HasFTaylorSeriesUpToOn n (fun x i => φ i x) (fun x m => ContinuousMultilinearMap.pi fun i => p' i x m) s ↔
    ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s

Proof state:
case refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
n : WithTop ℕ∞
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
L : (m : ℕ) →
  ((i : ι) → ContinuousMultilinearMap 𝕜 (fun i => E) (F' i)) ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun i => E) ((i : ι) → F' i) :=
  fun m => ContinuousMultilinearMap.piₗᵢ 𝕜 fun i => E
h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
x : E
hx : x ∈ s
⊢ (ContinuousMultilinearMap.pi fun i => p' i x 0).curry0 = fun i => φ i x

Tactic:
ext1 i

Result:
case refine_2.h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
n : WithTop ℕ∞
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
L : (m : ℕ) →
  ((i : ι) → ContinuousMultilinearMap 𝕜 (fun i => E) (F' i)) ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun i => E) ((i : ι) → F' i) :=
  fun m => ContinuousMultilinearMap.piₗᵢ 𝕜 fun i => E
h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
x : E
hx : x ∈ s
i : ι
⊢ (ContinuousMultilinearMap.pi fun i => p' i x 0).curry0 i = φ i x

Proof state:
case refine_4
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
n : WithTop ℕ∞
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
L : (m : ℕ) →
  ((i : ι) → ContinuousMultilinearMap 𝕜 (fun i => E) (F' i)) ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun i => E) ((i : ι) → F' i) :=
  fun m => ContinuousMultilinearMap.piₗᵢ 𝕜 fun i => E
h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
m : ℕ
hm : ↑m ≤ n
⊢ ContinuousOn (fun x => ContinuousMultilinearMap.pi fun i => p' i x m) s

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

Result:
no goals

Proof state:
case refine_2.h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
n : WithTop ℕ∞
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
L : (m : ℕ) →
  ((i : ι) → ContinuousMultilinearMap 𝕜 (fun i => E) (F' i)) ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun i => E) ((i : ι) → F' i) :=
  fun m => ContinuousMultilinearMap.piₗᵢ 𝕜 fun i => E
h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
x : E
hx : x ∈ s
i : ι
⊢ (ContinuousMultilinearMap.pi fun i => p' i x 0).curry0 i = φ i x

Tactic:
exact (h i).zero_eq x hx

Result:
no goals

Proof state:
case refine_3
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
n : WithTop ℕ∞
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
L : (m : ℕ) →
  ((i : ι) → ContinuousMultilinearMap 𝕜 (fun i => E) (F' i)) ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun i => E) ((i : ι) → F' i) :=
  fun m => ContinuousMultilinearMap.piₗᵢ 𝕜 fun i => E
h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x => ContinuousMultilinearMap.pi fun i => p' i x m)
    (ContinuousMultilinearMap.pi fun i => p' i x m.succ).curryLeft s x

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

Result:
no goals