-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem HasFTaylorSeriesUpToOn.prod {n : WithTop ℕ∞}
    (hf : HasFTaylorSeriesUpToOn n f p s) {g : E → G}
    {q : E → FormalMultilinearSeries 𝕜 E G} (hg : HasFTaylorSeriesUpToOn n g q s) :
    HasFTaylorSeriesUpToOn n (fun y => (f y, g y)) (fun y k => (p y k).prod (q y k)) s

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
⊢ HasFTaylorSeriesUpToOn n (fun y => (f y, g y)) (fun y k => (p y k).prod (q y k)) s

Tactic:
set L := fun m => ContinuousMultilinearMap.prodL 𝕜 (fun _ : Fin m => E) F G

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
L : (m : ℕ) →
  ContinuousMultilinearMap 𝕜 (fun x => E) F × ContinuousMultilinearMap 𝕜 (fun x => E) G ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun x => E) (F × G) :=
  fun m => ContinuousMultilinearMap.prodL 𝕜 (fun x => E) F G
⊢ HasFTaylorSeriesUpToOn n (fun y => (f y, g y)) (fun y k => (p y k).prod (q y k)) s

Proof state:
case fderivWithin
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
L : (m : ℕ) →
  ContinuousMultilinearMap 𝕜 (fun x => E) F × ContinuousMultilinearMap 𝕜 (fun x => E) G ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun x => E) (F × G) :=
  fun m => ContinuousMultilinearMap.prodL 𝕜 (fun x => E) F G
⊢ ∀ (m : ℕ),
    ↑m < n → ∀ x ∈ s, HasFDerivWithinAt (fun x => (p x m).prod (q x m)) ((p x m.succ).prod (q x m.succ)).curryLeft s x

Tactic:
intro m hm x hx

Result:
case fderivWithin
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
L : (m : ℕ) →
  ContinuousMultilinearMap 𝕜 (fun x => E) F × ContinuousMultilinearMap 𝕜 (fun x => E) G ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun x => E) (F × G) :=
  fun m => ContinuousMultilinearMap.prodL 𝕜 (fun x => E) F G
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x => (p x m).prod (q x m)) ((p x m.succ).prod (q x m.succ)).curryLeft s x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
L : (m : ℕ) →
  ContinuousMultilinearMap 𝕜 (fun x => E) F × ContinuousMultilinearMap 𝕜 (fun x => E) G ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun x => E) (F × G) :=
  fun m => ContinuousMultilinearMap.prodL 𝕜 (fun x => E) F G
⊢ HasFTaylorSeriesUpToOn n (fun y => (f y, g y)) (fun y k => (p y k).prod (q y k)) s

Tactic:
constructor

Result:
case zero_eq
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
L : (m : ℕ) →
  ContinuousMultilinearMap 𝕜 (fun x => E) F × ContinuousMultilinearMap 𝕜 (fun x => E) G ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun x => E) (F × G) :=
  fun m => ContinuousMultilinearMap.prodL 𝕜 (fun x => E) F G
⊢ ∀ x ∈ s, ((p x 0).prod (q x 0)).curry0 = (f x, g x)

case fderivWithin
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
L : (m : ℕ) →
  ContinuousMultilinearMap 𝕜 (fun x => E) F × ContinuousMultilinearMap 𝕜 (fun x => E) G ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun x => E) (F × G) :=
  fun m => ContinuousMultilinearMap.prodL 𝕜 (fun x => E) F G
⊢ ∀ (m : ℕ),
    ↑m < n → ∀ x ∈ s, HasFDerivWithinAt (fun x => (p x m).prod (q x m)) ((p x m.succ).prod (q x m.succ)).curryLeft s x

case cont
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
L : (m : ℕ) →
  ContinuousMultilinearMap 𝕜 (fun x => E) F × ContinuousMultilinearMap 𝕜 (fun x => E) G ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun x => E) (F × G) :=
  fun m => ContinuousMultilinearMap.prodL 𝕜 (fun x => E) F G
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => (p x m).prod (q x m)) s