awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
this : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p.prod q n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
have a : ∀ (n : ℕ), ‖‖p n‖ * (↑r : ℝ) ^ n‖ ≤ ‖‖p.prod q n‖ * (↑r : ℝ) ^ n‖
Tactic: refine (isBigO_of_le _ fun n ↦ ?_).trans this.isBigO
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
this : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p.prod q n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
n : ℕ
⊢ ‖‖p n‖ * (↑r : ℝ) ^ n‖ ≤ ‖‖p.prod q n‖ * (↑r : ℝ) ^ n‖
have a : ‖p n‖ * ‖(↑r : ℝ) ^ n‖ ≤ ‖p.prod q n‖ * ‖(↑r : ℝ) ^ n‖
Tactic: rw [norm_mul, norm_norm, norm_mul, norm_norm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
this : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p.prod q n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
n : ℕ
⊢ ‖p n‖ * ‖(↑r : ℝ) ^ n‖ ≤ ‖p.prod q n‖ * ‖(↑r : ℝ) ^ n‖
have a : ‖p n‖ ≤ ‖p.prod q n‖
Tactic: refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
this : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p.prod q n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
n : ℕ
⊢ ‖p n‖ ≤ ‖p.prod q n‖
have a : ‖p n‖ ≤ max ‖p n‖ ‖q n‖
Tactic: rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.opNorm_prod]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
this : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p.prod q n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
⊢ (↑r : ℝ≥0∞) ≤ q.radius
have a : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖q n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
Tactic: apply FormalMultilinearSeries.le_radius_of_isBigO
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
this : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p.prod q n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖q n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
have a : ∀ (n : ℕ), ‖‖q n‖ * (↑r : ℝ) ^ n‖ ≤ ‖‖p.prod q n‖ * (↑r : ℝ) ^ n‖
Tactic: refine (isBigO_of_le _ fun n ↦ ?_).trans this.isBigO
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
this : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p.prod q n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
n : ℕ
⊢ ‖‖q n‖ * (↑r : ℝ) ^ n‖ ≤ ‖‖p.prod q n‖ * (↑r : ℝ) ^ n‖
have a : ‖q n‖ * ‖(↑r : ℝ) ^ n‖ ≤ ‖p.prod q n‖ * ‖(↑r : ℝ) ^ n‖
Tactic: rw [norm_mul, norm_norm, norm_mul, norm_norm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
this : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p.prod q n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
n : ℕ
⊢ ‖q n‖ * ‖(↑r : ℝ) ^ n‖ ≤ ‖p.prod q n‖ * ‖(↑r : ℝ) ^ n‖
have a : ‖q n‖ ≤ ‖p.prod q n‖
Tactic: refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
this : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p.prod q n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
n : ℕ
⊢ ‖q n‖ ≤ ‖p.prod q n‖
have a : ‖q n‖ ≤ max ‖p n‖ ‖q n‖
Tactic: rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.opNorm_prod]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
⊢ min p.radius q.radius ≤ (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
have a : ∀ (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) < min p.radius q.radius), (↑r : ℝ≥0∞) ≤ (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
Tactic: refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (hypothesis)
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
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < min p.radius q.radius
⊢ (↑r : ℝ≥0∞) ≤ (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
have hr₁ : (↑r : ℝ≥0∞) < p.radius ∧ (↑r : ℝ≥0∞) < q.radius
Tactic: rw [lt_min_iff] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (hypothesis)
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
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius ∧ (↑r : ℝ≥0∞) < q.radius
⊢ (↑r : ℝ≥0∞) ≤ (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
have this : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℕ) ↦ ‖p x‖ * (↑r : ℝ) ^ x + ‖q x‖ * (↑r : ℝ) ^ x) fun (x : ℕ) ↦ 1
Tactic: have := ((p.isLittleO_one_of_lt_radius hr.1).add
      (q.isLittleO_one_of_lt_radius hr.2)).isBigO
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius ∧ (↑r : ℝ≥0∞) < q.radius
this : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℕ) ↦ ‖p x‖ * (↑r : ℝ) ^ x + ‖q x‖ * (↑r : ℝ) ^ x) fun (x : ℕ) ↦ 1
⊢ (↑r : ℝ≥0∞) ≤ (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
have a : ∀ (n : ℕ), ‖‖p.prod q n‖ * (↑r : ℝ) ^ n‖ ≤ ‖‖p n‖ * (↑r : ℝ) ^ n + ‖q n‖ * (↑r : ℝ) ^ n‖
Tactic: refine (p.prod q).le_radius_of_isBigO ((isBigO_of_le _ fun n ↦ ?_).trans this)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius ∧ (↑r : ℝ≥0∞) < q.radius
this : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℕ) ↦ ‖p x‖ * (↑r : ℝ) ^ x + ‖q x‖ * (↑r : ℝ) ^ x) fun (x : ℕ) ↦ 1
n : ℕ
⊢ ‖‖p.prod q n‖ * (↑r : ℝ) ^ n‖ ≤ ‖‖p n‖ * (↑r : ℝ) ^ n + ‖q n‖ * (↑r : ℝ) ^ n‖
have a : ‖p.prod q n‖ * ‖(↑r : ℝ) ^ n‖ ≤ ‖‖p n‖ + ‖q n‖‖ * ‖(↑r : ℝ) ^ n‖
Tactic: rw [norm_mul, norm_norm, ← add_mul, norm_mul]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius ∧ (↑r : ℝ≥0∞) < q.radius
this : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℕ) ↦ ‖p x‖ * (↑r : ℝ) ^ x + ‖q x‖ * (↑r : ℝ) ^ x) fun (x : ℕ) ↦ 1
n : ℕ
⊢ ‖p.prod q n‖ * ‖(↑r : ℝ) ^ n‖ ≤ ‖‖p n‖ + ‖q n‖‖ * ‖(↑r : ℝ) ^ n‖
have a : ‖p.prod q n‖ ≤ ‖‖p n‖ + ‖q n‖‖
Tactic: refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius ∧ (↑r : ℝ≥0∞) < q.radius
this : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℕ) ↦ ‖p x‖ * (↑r : ℝ) ^ x + ‖q x‖ * (↑r : ℝ) ^ x) fun (x : ℕ) ↦ 1
n : ℕ
⊢ ‖p.prod q n‖ ≤ ‖‖p n‖ + ‖q n‖‖
have a : max ‖p n‖ ‖q n‖ ≤ ‖‖p n‖ + ‖q n‖‖
Tactic: rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.opNorm_prod]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius ∧ (↑r : ℝ≥0∞) < q.radius
this : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℕ) ↦ ‖p x‖ * (↑r : ℝ) ^ x + ‖q x‖ * (↑r : ℝ) ^ x) fun (x : ℕ) ↦ 1
n : ℕ
⊢ max ‖p n‖ ‖q n‖ ≤ ‖‖p n‖ + ‖q n‖‖
have a : ‖p n‖ + ‖q n‖ ≤ ‖‖p n‖ + ‖q n‖‖
Tactic: refine (max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _)).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
⊢ min r s ≤ (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
have rw : min r s ≤ min p.radius q.radius
Tactic: rw [p.radius_prod_eq_min]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
⊢ HasSum (fun (n : ℕ) ↦ (p.prod q n : (a : (i : Fin n) → E) → F × G) fun (x : Fin n) ↦ y) (f (e + y), g (e + y))
have simp_rw : HasSum
  (fun (n : ℕ) ↦
    ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y, (q n : (a : (i : Fin n) → E) → G) fun (x : Fin n) ↦ y))
  (f (e + y), g (e + y))
Tactic: simp_rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.prod_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
⊢ HasSum
    (fun (n : ℕ) ↦
      ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y, (q n : (a : (i : Fin n) → E) → G) fun (x : Fin n) ↦ y))
    (f (e + y), g (e + y))
have refine_1 : Membership.mem (γ := Set E) (Metric.eball 0 r) y
Tactic: refine (hf.hasSum h'y ?_).prodMk (hg.hasSum h'y ?_)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
refine_1 : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ HasSum
    (fun (n : ℕ) ↦
      ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y, (q n : (a : (i : Fin n) → E) → G) fun (x : Fin n) ↦ y))
    (f (e + y), g (e + y))
have refine_2 : Membership.mem (γ := Set E) (Metric.eball 0 s) y
Tactic: refine (hf.hasSum h'y ?_).prodMk (hg.hasSum h'y ?_)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
⊢ HasFPowerSeriesOnBall (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) e (min r s)
have 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)
Tactic: rw [← hasFPowerSeriesWithinOnBall_univ] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
⊢ HasFPowerSeriesWithinAt (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) s e
have 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
Tactic: rcases hf with ⟨_, hf⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
⊢ HasFPowerSeriesWithinAt (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) s e
have 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
Tactic: rcases hg with ⟨_, hg⟩
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) e
have rcases : ∀ (w : ℝ≥0∞) (hf : HasFPowerSeriesOnBall f p e w),
  HasFPowerSeriesAt (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) e
Tactic: rcases hf with ⟨_, hf⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) e
have rcases : ∀ (w : ℝ≥0∞) (hg : HasFPowerSeriesOnBall g q e w),
  HasFPowerSeriesAt (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f x, g x)) (p.prod q) e
Tactic: rcases hg with ⟨_, hg⟩
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
⊢ AnalyticWithinAt 𝕜 (F := F × G) (fun (x : E) ↦ (f x, g x)) s e
have rcases : ∀ (w : FormalMultilinearSeries 𝕜 E F) (hf : HasFPowerSeriesWithinAt f w s e),
  AnalyticWithinAt 𝕜 (F := F × G) (fun (x : E) ↦ (f x, g x)) s e
Tactic: rcases hf with ⟨_, hf⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
⊢ AnalyticWithinAt 𝕜 (F := F × G) (fun (x : E) ↦ (f x, g x)) s e
have rcases : ∀ (w : FormalMultilinearSeries 𝕜 E G) (hg : HasFPowerSeriesWithinAt g w s e),
  AnalyticWithinAt 𝕜 (F := F × G) (fun (x : E) ↦ (f x, g x)) s e
Tactic: rcases hg with ⟨_, hg⟩
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
⊢ AnalyticAt 𝕜 (F := F × G) (fun (x : E) ↦ (f x, g x)) e
have rcases : ∀ (w : FormalMultilinearSeries 𝕜 E F) (hf : HasFPowerSeriesAt f w e),
  AnalyticAt 𝕜 (F := F × G) (fun (x : E) ↦ (f x, g x)) e
Tactic: rcases hf with ⟨_, hf⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
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
⊢ AnalyticAt 𝕜 (F := F × G) (fun (x : E) ↦ (f x, g x)) e
have rcases : ∀ (w : FormalMultilinearSeries 𝕜 E G) (hg : HasFPowerSeriesAt g w e),
  AnalyticAt 𝕜 (F := F × G) (fun (x : E) ↦ (f x, g x)) e
Tactic: rcases hg with ⟨_, hg⟩
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Constructions (goal)
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
i : ι
⊢ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p) ≤ (p i).radius
have apply : ∀ (r' : ℝ≥0) (hr' : (↑r' : ℝ≥0∞) < radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)),
  (↑r' : ℝ≥0∞) ≤ (p i).radius
Tactic: apply le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)