-- 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:
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)

Tactic:
intro x hx

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 : E
hx : x ∈ s
⊢ ((p x 0).prod (q x 0)).curry0 = (f x, g x)

Proof state:
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 : E
hx : x ∈ s
⊢ ((p x 0).prod (q x 0)).curry0 = (f x, g x)

Tactic:
rw [← hf.zero_eq x hx, ← hg.zero_eq x hx]

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 : E
hx : x ∈ s
⊢ ((p x 0).prod (q x 0)).curry0 = ((p x 0).curry0, (q x 0).curry0)

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 : ℕ
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

Tactic:
convert (L m).hasFDerivAt.comp_hasFDerivWithinAt x
    ((hf.fderivWithin m hm x hx).prod (hg.fderivWithin m hm x hx))

Result:
no goals

Proof state:
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 : ℕ
hm : ↑m ≤ n
⊢ ContinuousOn (fun x => (p x m).prod (q x m)) s

Tactic:
exact (L m).continuous.comp_continuousOn ((hf.cont m hm).prod (hg.cont m hm))

Result:
no goals

Proof state:
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

Tactic:
intro m hm

Result:
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 : ℕ
hm : ↑m ≤ n
⊢ ContinuousOn (fun x => (p x m).prod (q x m)) s

Proof state:
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 : E
hx : x ∈ s
⊢ ((p x 0).prod (q x 0)).curry0 = ((p x 0).curry0, (q x 0).curry0)

Tactic:
rfl

Result:
no goals