awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
r s : ℝ≥0∞
t : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesWithinOnBall f p t e r
hg : HasFPowerSeriesWithinOnBall g q t e s
y : E
h'y : e + y ∈ insert e t
hy : Membership.mem (γ := Set E) (Metric.eball 0 (min r s)) y
⊢ Membership.mem (γ := Set E) (Metric.eball 0 r) y

Tactic:
exact Metric.mem_eball.mpr (lt_of_lt_of_le hy (min_le_left _ _))

Premises used: Iff.mpr, min_le_left, lt_of_lt_of_le, Metric.mem_eball
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
r s : ℝ≥0∞
t : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesWithinOnBall f p t e r
hg : HasFPowerSeriesWithinOnBall g q t e s
y : E
h'y : e + y ∈ insert e t
hy : Membership.mem (γ := Set E) (Metric.eball 0 (min r s)) y
⊢ Membership.mem (γ := Set E) (Metric.eball 0 s) y

Tactic:
Metric.mem_eball.mpr (lt_of_lt_of_le hy (min_le_right _ _))

Premises used: Iff.mpr, min_le_right, lt_of_lt_of_le, Metric.mem_eball
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
r s : ℝ≥0∞
t : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesWithinOnBall f p t e r
hg : HasFPowerSeriesWithinOnBall g q t e s
y : E
h'y : e + y ∈ insert e t
hy : Membership.mem (γ := Set E) (Metric.eball 0 (min r s)) y
⊢ Membership.mem (γ := Set E) (Metric.eball 0 s) y

Tactic:
exact Metric.mem_eball.mpr (lt_of_lt_of_le hy (min_le_right _ _))

Premises used: Iff.mpr, min_le_right, lt_of_lt_of_le, Metric.mem_eball
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
r s : ℝ≥0∞
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesOnBall f p e r
hg : HasFPowerSeriesOnBall g q e s
rw :
  ∀ (hf : HasFPowerSeriesWithinOnBall f p Set.univ e r) (hg : HasFPowerSeriesWithinOnBall g q Set.univ e s),
    HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) Set.univ e (min r s)
⊢ HasFPowerSeriesOnBall (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) e (min r s)

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf hg ⊢

Premises used: hasFPowerSeriesWithinOnBall_univ
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
r s : ℝ≥0∞
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesWithinOnBall f p Set.univ e r
hg : HasFPowerSeriesWithinOnBall g q Set.univ e s
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) Set.univ e (min r s)

Tactic:
hf.prod hg

Premises used: HasFPowerSeriesWithinOnBall.prod
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
r s : ℝ≥0∞
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesWithinOnBall f p Set.univ e r
hg : HasFPowerSeriesWithinOnBall g q Set.univ e s
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) Set.univ e (min r s)

Tactic:
exact hf.prod hg

Premises used: HasFPowerSeriesWithinOnBall.prod
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
s : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesWithinAt f p s e
hg : HasFPowerSeriesWithinAt g q s e
rcases :
  ∀ (w : ℝ≥0∞) (hf : HasFPowerSeriesWithinOnBall f p s e w),
    HasFPowerSeriesWithinAt (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) s e
⊢ HasFPowerSeriesWithinAt (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) s e

Tactic:
rcases hf with ⟨_, hf⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
s : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hg : HasFPowerSeriesWithinAt g q s e
w : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s e w
rcases :
  ∀ (w : ℝ≥0∞) (hg : HasFPowerSeriesWithinOnBall g q s e w),
    HasFPowerSeriesWithinAt (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) s e
⊢ HasFPowerSeriesWithinAt (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) s e

Tactic:
rcases hg with ⟨_, hg⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
s : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
w : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s e w
w_1 : ℝ≥0∞
hg : HasFPowerSeriesWithinOnBall g q s e w_1
⊢ HasFPowerSeriesWithinAt (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) s e

Tactic:
⟨_, hf.prod hg⟩

Premises used: HasFPowerSeriesWithinOnBall.prod, HasFPowerSeriesWithinAt, Exists.intro
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
s : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
w : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s e w
w_1 : ℝ≥0∞
hg : HasFPowerSeriesWithinOnBall g q s e w_1
⊢ HasFPowerSeriesWithinAt (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) s e

Tactic:
exact ⟨_, hf.prod hg⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesAt f p e
hg : HasFPowerSeriesAt g q e
rcases :
  ∀ (w : ℝ≥0∞) (hf : HasFPowerSeriesOnBall f p e w),
    HasFPowerSeriesAt (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) e
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) e

Tactic:
rcases hf with ⟨_, hf⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hg : HasFPowerSeriesAt g q e
w : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p e w
rcases :
  ∀ (w : ℝ≥0∞) (hg : HasFPowerSeriesOnBall g q e w),
    HasFPowerSeriesAt (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) e
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) e

Tactic:
rcases hg with ⟨_, hg⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
w : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p e w
w_1 : ℝ≥0∞
hg : HasFPowerSeriesOnBall g q e w_1
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) e

Tactic:
⟨_, hf.prod hg⟩

Premises used: HasFPowerSeriesOnBall.prod, Exists.intro, HasFPowerSeriesAt
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
w : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p e w
w_1 : ℝ≥0∞
hg : HasFPowerSeriesOnBall g q e w_1
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) e

Tactic:
exact ⟨_, hf.prod hg⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
s : Set E
hf : AnalyticWithinAt 𝕜 f s e
hg : AnalyticWithinAt 𝕜 g s e
rcases :
  ∀ (w : FormalMultilinearSeries 𝕜 E F) (hf : HasFPowerSeriesWithinAt f w s e),
    AnalyticWithinAt 𝕜 (F := F × G) (fun (x : E) ↦ (f x, g x)) s e
⊢ AnalyticWithinAt 𝕜 (F := F × G) (fun (x : E) ↦ (f x, g x)) s e

Tactic:
rcases hf with ⟨_, hf⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
s : Set E
hg : AnalyticWithinAt 𝕜 g s e
w : FormalMultilinearSeries 𝕜 E F
hf : HasFPowerSeriesWithinAt f w s e
rcases :
  ∀ (w : FormalMultilinearSeries 𝕜 E G) (hg : HasFPowerSeriesWithinAt g w s e),
    AnalyticWithinAt 𝕜 (F := F × G) (fun (x : E) ↦ (f x, g x)) s e
⊢ AnalyticWithinAt 𝕜 (F := F × G) (fun (x : E) ↦ (f x, g x)) s e

Tactic:
rcases hg with ⟨_, hg⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
s : Set E
w : FormalMultilinearSeries 𝕜 E F
hf : HasFPowerSeriesWithinAt f w s e
w_1 : FormalMultilinearSeries 𝕜 E G
hg : HasFPowerSeriesWithinAt g w_1 s e
⊢ AnalyticWithinAt 𝕜 (F := F × G) (fun (x : E) ↦ (f x, g x)) s e

Tactic:
⟨_, hf.prod hg⟩

Premises used: AnalyticWithinAt, HasFPowerSeriesWithinAt.prod, Exists.intro
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
s : Set E
w : FormalMultilinearSeries 𝕜 E F
hf : HasFPowerSeriesWithinAt f w s e
w_1 : FormalMultilinearSeries 𝕜 E G
hg : HasFPowerSeriesWithinAt g w_1 s e
⊢ AnalyticWithinAt 𝕜 (F := F × G) (fun (x : E) ↦ (f x, g x)) s e

Tactic:
exact ⟨_, hf.prod hg⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
hf : AnalyticAt 𝕜 f e
hg : AnalyticAt 𝕜 g e
rcases :
  ∀ (w : FormalMultilinearSeries 𝕜 E F) (hf : HasFPowerSeriesAt f w e),
    AnalyticAt 𝕜 (F := F × G) (fun (x : E) ↦ (f x, g x)) e
⊢ AnalyticAt 𝕜 (F := F × G) (fun (x : E) ↦ (f x, g x)) e

Tactic:
rcases hf with ⟨_, hf⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
hg : AnalyticAt 𝕜 g e
w : FormalMultilinearSeries 𝕜 E F
hf : HasFPowerSeriesAt f w e
rcases :
  ∀ (w : FormalMultilinearSeries 𝕜 E G) (hg : HasFPowerSeriesAt g w e),
    AnalyticAt 𝕜 (F := F × G) (fun (x : E) ↦ (f x, g x)) e
⊢ AnalyticAt 𝕜 (F := F × G) (fun (x : E) ↦ (f x, g x)) e

Tactic:
rcases hg with ⟨_, hg⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
w : FormalMultilinearSeries 𝕜 E F
hf : HasFPowerSeriesAt f w e
w_1 : FormalMultilinearSeries 𝕜 E G
hg : HasFPowerSeriesAt g w_1 e
⊢ AnalyticAt 𝕜 (F := F × G) (fun (x : E) ↦ (f x, g x)) e

Tactic:
⟨_, hf.prod hg⟩

Premises used: AnalyticAt, Exists.intro, HasFPowerSeriesAt.prod
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
w : FormalMultilinearSeries 𝕜 E F
hf : HasFPowerSeriesAt f w e
w_1 : FormalMultilinearSeries 𝕜 E G
hg : HasFPowerSeriesAt g w_1 e
⊢ AnalyticAt 𝕜 (F := F × G) (fun (x : E) ↦ (f x, g x)) e

Tactic:
exact ⟨_, hf.prod hg⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
g : E → G
s : Set E
hf : AnalyticOn 𝕜 f s
hg : AnalyticOn 𝕜 g s
⊢ AnalyticOn 𝕜 (F := F × G) (fun (x : E) ↦ (f x, g x)) s

Tactic:
fun x hx ↦ (hf x hx).prod (hg x hx)

Premises used: AnalyticOn, AnalyticWithinAt.prod
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
g : E → G
s : Set E
hf : AnalyticOnNhd 𝕜 f s
hg : AnalyticOnNhd 𝕜 g s
⊢ AnalyticOnNhd 𝕜 (F := F × G) (fun (x : E) ↦ (f x, g x)) s

Tactic:
fun x hx ↦ (hf x hx).prod (hg x hx)

Premises used: AnalyticOnNhd, AnalyticAt.prod
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
H : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
h : F × G → H
f : E → F
g : E → G
x : E
ha : AnalyticAt 𝕜 h (f x, g x)
fa : AnalyticAt 𝕜 f x
ga : AnalyticAt 𝕜 g x
⊢ AnalyticAt.{u_2, u_3, u_6} 𝕜 (F := H) (fun (x : E) ↦ h (f x, g x)) x

Tactic:
AnalyticAt.comp ha (fa.prod ga)

Premises used: AnalyticAt.prod, AnalyticAt.comp
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
H : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
h : F × G → H
f : E → F
g : E → G
s : Set (F × G)
t : Set E
x : E
ha : AnalyticWithinAt 𝕜 h s (f x, g x)
fa : AnalyticWithinAt 𝕜 f t x
ga : AnalyticWithinAt 𝕜 g t x
hf : Set.MapsTo (fun (y : E) ↦ (f y, g y)) t s
⊢ AnalyticWithinAt.{u_2, u_3, u_6} 𝕜 (F := H) (fun (x : E) ↦ h (f x, g x)) t x

Tactic:
AnalyticWithinAt.comp ha (fa.prod ga) hf

Premises used: AnalyticWithinAt.prod, AnalyticWithinAt.comp
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
H : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
h : F × G → H
f : E → F
g : E → G
x : E
s : Set E
ha : AnalyticAt 𝕜 h (f x, g x)
fa : AnalyticWithinAt 𝕜 f s x
ga : AnalyticWithinAt 𝕜 g s x
⊢ AnalyticWithinAt.{u_2, u_3, u_6} 𝕜 (F := H) (fun (x : E) ↦ h (f x, g x)) s x

Tactic:
AnalyticAt.comp_analyticWithinAt ha (fa.prod ga)

Premises used: AnalyticAt.comp_analyticWithinAt, AnalyticWithinAt.prod
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
H : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
h : F × G → H
f : E → F
g : E → G
s : Set (F × G)
t : Set E
ha : AnalyticOnNhd 𝕜 h s
fa : AnalyticOnNhd 𝕜 f t
ga : AnalyticOnNhd 𝕜 g t
m : ∀ x ∈ t, (f x, g x) ∈ s
⊢ AnalyticOnNhd.{u_2, u_3, u_6} 𝕜 (F := H) (fun (x : E) ↦ h (f x, g x)) t

Tactic:
fun _ xt ↦ (ha _ (m _ xt)).comp₂ (fa _ xt) (ga _ xt)

Premises used: AnalyticOnNhd, Prod.mk, AnalyticAt.comp₂
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
H : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
h : F × G → H
f : E → F
g : E → G
s : Set (F × G)
t : Set E
ha : AnalyticOn 𝕜 h s
fa : AnalyticOn 𝕜 f t
ga : AnalyticOn 𝕜 g t
m : Set.MapsTo (fun (y : E) ↦ (f y, g y)) t s
⊢ AnalyticOn.{u_2, u_3, u_6} 𝕜 (F := H) (fun (x : E) ↦ h (f x, g x)) t

Tactic:
fun x hx ↦ (ha _ (m hx)).comp₂ (fa x hx) (ga x hx) m

Premises used: AnalyticOn, Prod.mk, AnalyticWithinAt.comp₂
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E × F → G
p : E × F
fa : AnalyticAt 𝕜 f p
⊢ AnalyticAt.{u_2, u_3, u_5} 𝕜 (F := G) (fun (x : E) ↦ f (x, p.2)) p.1

Tactic:
AnalyticAt.comp₂ fa analyticAt_id analyticAt_const

Premises used: analyticAt_const, analyticAt_id, AnalyticAt.comp₂
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E × F → G
s : Set (E × F)
p : E × F
fa : AnalyticWithinAt 𝕜 f s p
⊢ AnalyticWithinAt.{u_2, u_3, u_5} 𝕜 (F := G) (fun (x : E) ↦ f (x, p.2)) {x : E | (x, p.2) ∈ s} p.1

Tactic:
AnalyticWithinAt.comp₂ fa analyticWithinAt_id analyticWithinAt_const (fun _ hx ↦ hx)

Premises used: analyticWithinAt_id, analyticWithinAt_const, AnalyticWithinAt.comp₂
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E × F → G
p : E × F
fa : AnalyticAt 𝕜 f p
⊢ AnalyticAt.{u_2, u_4, u_5} 𝕜 (F := G) (fun (y : F) ↦ f (p.1, y)) p.2

Tactic:
AnalyticAt.comp₂ fa analyticAt_const analyticAt_id

Premises used: analyticAt_const, analyticAt_id, AnalyticAt.comp₂
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E × F → G
s : Set (E × F)
p : E × F
fa : AnalyticWithinAt 𝕜 f s p
⊢ AnalyticWithinAt.{u_2, u_4, u_5} 𝕜 (F := G) (fun (y : F) ↦ f (p.1, y)) {y : F | (p.1, y) ∈ s} p.2

Tactic:
AnalyticWithinAt.comp₂ fa analyticWithinAt_const analyticWithinAt_id (fun _ hx ↦ hx)

Premises used: analyticWithinAt_id, analyticWithinAt_const, AnalyticWithinAt.comp₂
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E × F → G
s : Set (E × F)
y : F
fa : AnalyticOnNhd 𝕜 f s
⊢ AnalyticOnNhd.{u_2, u_3, u_5} 𝕜 (F := G) (fun (x : E) ↦ f (x, y)) {x : E | (x, y) ∈ s}

Tactic:
fun x m ↦ (fa (x, y) m).curry_left

Premises used: AnalyticOnNhd, Prod.mk, AnalyticAt.curry_left
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E × F → G
s : Set (E × F)
y : F
fa : AnalyticOn 𝕜 f s
⊢ AnalyticOn.{u_2, u_3, u_5} 𝕜 (F := G) (fun (x : E) ↦ f (x, y)) {x : E | (x, y) ∈ s}

Tactic:
fun x m ↦ (fa (x, y) m).curry_left

Premises used: AnalyticOn, Set.Mem, setOf, AnalyticWithinAt.curry_left, Prod.mk
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E × F → G
x : E
s : Set (E × F)
fa : AnalyticOnNhd 𝕜 f s
⊢ AnalyticOnNhd.{u_2, u_4, u_5} 𝕜 (F := G) (fun (y : F) ↦ f (x, y)) {y : F | (x, y) ∈ s}

Tactic:
fun y m ↦ (fa (x, y) m).curry_right

Premises used: AnalyticAt.curry_right, AnalyticOnNhd, Prod.mk