-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContDiffWithinAt.prod {s : Set E} {f : E → F} {g : E → G} (hf : ContDiffWithinAt 𝕜 n f s x)
    (hg : ContDiffWithinAt 𝕜 n g s x) : ContDiffWithinAt 𝕜 n (fun x : E => (f x, g x)) 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
x : E
n : WithTop ℕ∞
s : Set E
f : E → F
g : E → G
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
⊢ ContDiffWithinAt 𝕜 n (fun x => (f x, g x)) s x

Tactic:
match n with
| ω =>
  obtain ⟨u, hu, p, hp, h'p⟩ := hf
  obtain ⟨v, hv, q, hq, h'q⟩ := hg
  refine ⟨u ∩ v, Filter.inter_mem hu hv, _,
    (hp.mono inter_subset_left).prod (hq.mono inter_subset_right), fun i ↦ ?_⟩
  change AnalyticOn 𝕜 (fun x ↦ ContinuousMultilinearMap.prodL _ _ _ _ (p x i, q x i))
    (u ∩ v)
  apply AnalyticOnNhd.comp_analyticOn (LinearIsometryEquiv.analyticOnNhd _ _) _
    (Set.mapsTo_univ _ _)
  exact ((h'p i).mono inter_subset_left).prod ((h'q i).mono inter_subset_right)
| (n : ℕ∞) =>
  intro m hm
  rcases hf m hm with ⟨u, hu, p, hp⟩
  rcases hg m hm with ⟨v, hv, q, hq⟩
  exact
    ⟨u ∩ v, Filter.inter_mem hu hv, _,
      (hp.mono inter_subset_left).prod (hq.mono inter_subset_right)⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
𝕜 : 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
x : E
n✝ : WithTop ℕ∞
s : Set E
f : E → F
g : E → G
n : ℕ∞
hf : ContDiffWithinAt 𝕜 (↑n) f s x
hg : ContDiffWithinAt 𝕜 (↑n) g s x
m : ℕ
hm : ↑m ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m) f p u
v : Set E
hv : v ∈ 𝓝[insert x s] x
q : E → FormalMultilinearSeries 𝕜 E G
hq : HasFTaylorSeriesUpToOn (↑m) g q v
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (fun x => (f x, g x)) p u

Tactic:
exact
  ⟨u ∩ v, Filter.inter_mem hu hv, _,
    (hp.mono inter_subset_left).prod (hq.mono inter_subset_right)⟩

Result:
no goals

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
x : E
n : WithTop ℕ∞
s : Set E
f : E → F
g : E → G
hf : ContDiffWithinAt 𝕜 ω f s x
hg : ContDiffWithinAt 𝕜 ω g s x
⊢ ContDiffWithinAt 𝕜 ω (fun x => (f x, g x)) s x

Tactic:
obtain ⟨u, hu, p, hp, h'p⟩ := hf

Result:
case intro.intro.intro.intro
𝕜 : 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
x : E
n : WithTop ℕ∞
s : Set E
f : E → F
g : E → G
hg : ContDiffWithinAt 𝕜 ω g s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
⊢ ContDiffWithinAt 𝕜 ω (fun x => (f x, g x)) 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
x : E
n✝ : WithTop ℕ∞
s : Set E
f : E → F
g : E → G
n : ℕ∞
hf : ContDiffWithinAt 𝕜 (↑n) f s x
hg : ContDiffWithinAt 𝕜 (↑n) g s x
m : ℕ
hm : ↑m ≤ n
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (fun x => (f x, g x)) p u

Tactic:
rcases hf m hm with ⟨u, hu, p, hp⟩

Result:
case intro.intro.intro
𝕜 : 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
x : E
n✝ : WithTop ℕ∞
s : Set E
f : E → F
g : E → G
n : ℕ∞
hf : ContDiffWithinAt 𝕜 (↑n) f s x
hg : ContDiffWithinAt 𝕜 (↑n) g s x
m : ℕ
hm : ↑m ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m) f p u
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (fun x => (f x, g x)) p u

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : 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
x : E
n : WithTop ℕ∞
s : Set E
f : E → F
g : E → G
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
v : Set E
hv : v ∈ 𝓝[insert x s] x
q : E → FormalMultilinearSeries 𝕜 E G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => q x i) v
⊢ ContDiffWithinAt 𝕜 ω (fun x => (f x, g x)) s x

Tactic:
refine ⟨u ∩ v, Filter.inter_mem hu hv, _,
  (hp.mono inter_subset_left).prod (hq.mono inter_subset_right), fun i ↦ ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : 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
x : E
n : WithTop ℕ∞
s : Set E
f : E → F
g : E → G
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
v : Set E
hv : v ∈ 𝓝[insert x s] x
q : E → FormalMultilinearSeries 𝕜 E G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => q x i) v
i : ℕ
⊢ AnalyticOn 𝕜 (fun x => (p x i).prod (q x i)) (u ∩ v)