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
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‖

Tactic:
mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)

Premises used: mul_le_mul_of_nonneg_right, norm_nonneg
-- 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
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 : ℕ
a : ‖p n‖ ≤ ‖p.prod q n‖
⊢ ‖p n‖ * ‖(↑r : ℝ) ^ n‖ ≤ ‖p.prod q n‖ * ‖(↑r : ℝ) ^ n‖

Tactic:
refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)

Premises used: mul_le_mul_of_nonneg_right, norm_nonneg
-- 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
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 : ℕ
a : ‖p n‖ ≤ max ‖p n‖ ‖q n‖
⊢ ‖p n‖ ≤ ‖p.prod q n‖

Tactic:
rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.opNorm_prod]

Premises used: ContinuousMultilinearMap.opNorm_prod, FormalMultilinearSeries.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
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
a : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖q n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
⊢ (↑r : ℝ≥0∞) ≤ q.radius

Tactic:
apply FormalMultilinearSeries.le_radius_of_isBigO

Premises used: FormalMultilinearSeries.le_radius_of_isBigO
-- 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
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

Tactic:
(isBigO_of_le _ fun n ↦ ?_).trans this.isBigO

Premises used: Asymptotics.IsBigO.trans, Asymptotics.IsLittleO.isBigO, Asymptotics.isBigO_of_le
-- 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
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
a : ∀ (n : ℕ), ‖‖q n‖ * (↑r : ℝ) ^ n‖ ≤ ‖‖p.prod q n‖ * (↑r : ℝ) ^ n‖
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖q n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1

Tactic:
refine (isBigO_of_le _ fun n ↦ ?_).trans this.isBigO

Premises used: Asymptotics.IsBigO.trans, Asymptotics.IsLittleO.isBigO, Asymptotics.isBigO_of_le
-- 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
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 : ℕ
a : ‖q n‖ * ‖(↑r : ℝ) ^ n‖ ≤ ‖p.prod q n‖ * ‖(↑r : ℝ) ^ n‖
⊢ ‖‖q n‖ * (↑r : ℝ) ^ n‖ ≤ ‖‖p.prod q n‖ * (↑r : ℝ) ^ n‖

Tactic:
rw [norm_mul, norm_norm, norm_mul, norm_norm]

Premises used: norm_mul, norm_norm
-- 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
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‖

Tactic:
mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)

Premises used: mul_le_mul_of_nonneg_right, norm_nonneg
-- 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
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 : ℕ
a : ‖q n‖ ≤ ‖p.prod q n‖
⊢ ‖q n‖ * ‖(↑r : ℝ) ^ n‖ ≤ ‖p.prod q n‖ * ‖(↑r : ℝ) ^ n‖

Tactic:
refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)

Premises used: mul_le_mul_of_nonneg_right, norm_nonneg
-- 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
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 : ℕ
a : ‖q n‖ ≤ max ‖p n‖ ‖q n‖
⊢ ‖q n‖ ≤ ‖p.prod q n‖

Tactic:
rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.opNorm_prod]

Premises used: ContinuousMultilinearMap.opNorm_prod, FormalMultilinearSeries.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
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‖ ≤ max ‖p n‖ ‖q n‖

Tactic:
apply le_max_left

Premises used: le_max_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
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‖ ≤ max ‖p n‖ ‖q n‖

Tactic:
apply le_max_right

Premises used: le_max_right
-- 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
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
⊢ min p.radius q.radius ≤ (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)

Tactic:
ENNReal.le_of_forall_nnreal_lt fun r hr => ?_

Premises used: ENNReal.le_of_forall_nnreal_lt
-- 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
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
a :
  ∀ (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) < min p.radius q.radius), (↑r : ℝ≥0∞) ≤ (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)
⊢ min p.radius q.radius ≤ (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)

Tactic:
refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_

Premises used: ENNReal.le_of_forall_nnreal_lt
-- 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
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < min p.radius q.radius
⊢ (↑r : ℝ≥0∞) < p.radius ∧ (↑r : ℝ≥0∞) < q.radius

Tactic:
rw [lt_min_iff] at hr

Premises used: lt_min_iff
-- 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
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius ∧ (↑r : ℝ≥0∞) < q.radius
⊢ 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
-- 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
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)

Tactic:
(p.prod q).le_radius_of_isBigO ((isBigO_of_le _ fun n ↦ ?_).trans this)

Premises used: Asymptotics.IsBigO.trans, FormalMultilinearSeries.le_radius_of_isBigO, Asymptotics.isBigO_of_le, FormalMultilinearSeries.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
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
a : ∀ (n : ℕ), ‖‖p.prod q n‖ * (↑r : ℝ) ^ n‖ ≤ ‖‖p n‖ * (↑r : ℝ) ^ n + ‖q n‖ * (↑r : ℝ) ^ n‖
⊢ (↑r : ℝ≥0∞) ≤ (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)

Tactic:
refine (p.prod q).le_radius_of_isBigO ((isBigO_of_le _ fun n ↦ ?_).trans this)

Premises used: Asymptotics.IsBigO.trans, FormalMultilinearSeries.le_radius_of_isBigO, Asymptotics.isBigO_of_le, FormalMultilinearSeries.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
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 : ℕ
a : ‖p.prod q n‖ * ‖(↑r : ℝ) ^ n‖ ≤ ‖‖p n‖ + ‖q n‖‖ * ‖(↑r : ℝ) ^ n‖
⊢ ‖‖p.prod q n‖ * (↑r : ℝ) ^ n‖ ≤ ‖‖p n‖ * (↑r : ℝ) ^ n + ‖q n‖ * (↑r : ℝ) ^ n‖

Tactic:
rw [norm_mul, norm_norm, ← add_mul, norm_mul]

Premises used: add_mul, norm_mul, norm_norm
-- 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
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‖

Tactic:
mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)

Premises used: mul_le_mul_of_nonneg_right, norm_nonneg
-- 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
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 : ℕ
a : ‖p.prod q n‖ ≤ ‖‖p n‖ + ‖q n‖‖
⊢ ‖p.prod q n‖ * ‖(↑r : ℝ) ^ n‖ ≤ ‖‖p n‖ + ‖q n‖‖ * ‖(↑r : ℝ) ^ n‖

Tactic:
refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)

Premises used: mul_le_mul_of_nonneg_right, norm_nonneg
-- 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
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 : ℕ
a : max ‖p n‖ ‖q n‖ ≤ ‖‖p n‖ + ‖q n‖‖
⊢ ‖p.prod q n‖ ≤ ‖‖p n‖ + ‖q n‖‖

Tactic:
rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.opNorm_prod]

Premises used: ContinuousMultilinearMap.opNorm_prod, FormalMultilinearSeries.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
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‖‖

Tactic:
(max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _)).trans ?_

Premises used: max_le_add_of_nonneg, LE.le.trans, norm_nonneg
-- 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
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 : ℕ
a : ‖p n‖ + ‖q n‖ ≤ ‖‖p n‖ + ‖q n‖‖
⊢ max ‖p n‖ ‖q n‖ ≤ ‖‖p n‖ + ‖q n‖‖

Tactic:
refine (max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _)).trans ?_

Premises used: max_le_add_of_nonneg, LE.le.trans, norm_nonneg
-- 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
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 n‖ + ‖q n‖ ≤ ‖‖p n‖ + ‖q n‖‖

Tactic:
apply Real.le_norm_self

Premises used: Real.le_norm_self
-- 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
rw : min r s ≤ min p.radius q.radius
⊢ min r s ≤ (p.prod q).radius (𝕜 := 𝕜) (E := E) (F := F × G)

Tactic:
rw [p.radius_prod_eq_min]

Premises used: FormalMultilinearSeries.radius_prod_eq_min
-- 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
⊢ min r s ≤ min p.radius q.radius

Tactic:
min_le_min hf.r_le hg.r_le

Premises used: HasFPowerSeriesWithinOnBall.r_le, min_le_min
-- 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
⊢ min r s ≤ min p.radius q.radius

Tactic:
exact min_le_min hf.r_le hg.r_le

Premises used: HasFPowerSeriesWithinOnBall.r_le, min_le_min
-- 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
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))
⊢ 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))

Tactic:
simp_rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.prod_apply]

Premises used: ContinuousMultilinearMap.prod_apply, FormalMultilinearSeries.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∞
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))

Tactic:
(hf.hasSum h'y ?_).prodMk (hg.hasSum h'y ?_)

Premises used: setOf, HasSum.prodMk, HasFPowerSeriesWithinOnBall.hasSum
-- 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
refine_1 : Membership.mem (γ := Set E) (Metric.eball 0 r) y
refine_2 : Membership.mem (γ := Set E) (Metric.eball 0 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))

Tactic:
refine (hf.hasSum h'y ?_).prodMk (hg.hasSum h'y ?_)

Premises used: HasSum.prodMk, HasFPowerSeriesWithinOnBall.hasSum
-- 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:
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