awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
h : 0 < p.radius
r : ℝ≥0
r0 : 0 < (↑r : ℝ≥0∞)
rlt : (↑r : ℝ≥0∞) < p.radius
rpos : 0 < (↑r : ℝ)
C : ℝ
Cpos : C > 0
hCp : ∀ (n : ℕ), ‖p n‖ ≤ C / (↑r : ℝ) ^ n
n : ℕ
⊢ ‖p n‖ ≤ C / (↑r : ℝ) ^ n

Tactic:
hCp n
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
h : 0 < p.radius
r : ℝ≥0
r0 : 0 < (↑r : ℝ≥0∞)
rlt : (↑r : ℝ≥0∞) < p.radius
rpos : 0 < (↑r : ℝ)
C : ℝ
Cpos : C > 0
hCp : ∀ (n : ℕ), ‖p n‖ ≤ C / (↑r : ℝ) ^ n
n : ℕ
⊢ ‖p n‖ ≤ C / (↑r : ℝ) ^ n

Tactic:
exact hCp n
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_5
E' : Type u_6
F' : Type u_7
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜' E'
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜' F'
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜' E' F'
h : ∀ (n : ℕ), ‖p n‖ ≤ ‖q n‖
apply : ∀ (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) < q.radius), (↑r : ℝ≥0∞) ≤ p.radius
⊢ q.radius ≤ p.radius

Tactic:
apply le_of_forall_nnreal_lt (fun r hr ↦ ?_)

Premises used: ENNReal.le_of_forall_nnreal_lt
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_5
E' : Type u_6
F' : Type u_7
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜' E'
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜' F'
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜' E' F'
h : ∀ (n : ℕ), ‖p n‖ ≤ ‖q n‖
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < q.radius
rcases : ∀ (C : ℝ) (hC : ∀ (n : ℕ), ‖q n‖ * (↑r : ℝ) ^ n ≤ C), (↑r : ℝ≥0∞) ≤ p.radius
⊢ (↑r : ℝ≥0∞) ≤ p.radius

Tactic:
rcases norm_mul_pow_le_of_lt_radius _ hr with ⟨C, -, hC⟩

Premises used: FormalMultilinearSeries.norm_mul_pow_le_of_lt_radius
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_5
E' : Type u_6
F' : Type u_7
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜' E'
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜' F'
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜' E' F'
h : ∀ (n : ℕ), ‖p n‖ ≤ ‖q n‖
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < q.radius
C : ℝ
hC : ∀ (n : ℕ), ‖q n‖ * (↑r : ℝ) ^ n ≤ C
apply : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
⊢ (↑r : ℝ≥0∞) ≤ p.radius

Tactic:
apply le_radius_of_bound _ C (fun n ↦ ?_)

Premises used: FormalMultilinearSeries.le_radius_of_bound
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_5
E' : Type u_6
F' : Type u_7
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜' E'
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜' F'
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜' E' F'
h : ∀ (n : ℕ), ‖p n‖ ≤ ‖q n‖
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < q.radius
C : ℝ
hC : ∀ (n : ℕ), ‖q n‖ * (↑r : ℝ) ^ n ≤ C
n : ℕ
apply : ‖p n‖ * (↑r : ℝ) ^ n ≤ ‖q n‖ * (↑r : ℝ) ^ n
⊢ ‖p n‖ * (↑r : ℝ) ^ n ≤ C

Tactic:
apply le_trans _ (hC n)

Premises used: le_trans
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_5
E' : Type u_6
F' : Type u_7
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜' E'
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜' F'
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜' E' F'
h : ∀ (n : ℕ), ‖p n‖ ≤ ‖q n‖
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < q.radius
C : ℝ
hC : ∀ (n : ℕ), ‖q n‖ * (↑r : ℝ) ^ n ≤ C
n : ℕ
hbc : ‖p n‖ ≤ ‖q n‖
⊢ ‖p n‖ * (↑r : ℝ) ^ n ≤ ‖q n‖ * (↑r : ℝ) ^ n

Tactic:
gcongr
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_5
E' : Type u_6
F' : Type u_7
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜' E'
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜' F'
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜' E' F'
h : ∀ (n : ℕ), ‖p n‖ ≤ ‖q n‖
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < q.radius
C : ℝ
hC : ∀ (n : ℕ), ‖q n‖ * (↑r : ℝ) ^ n ≤ C
n : ℕ
⊢ ‖p n‖ ≤ ‖q n‖

Tactic:
h n
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_5
E' : Type u_6
F' : Type u_7
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜' E'
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜' F'
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜' E' F'
h : ∀ (n : ℕ), ‖p n‖ ≤ ‖q n‖
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < q.radius
C : ℝ
hC : ∀ (n : ℕ), ‖q n‖ * (↑r : ℝ) ^ n ≤ C
n : ℕ
⊢ ‖p n‖ ≤ ‖q n‖

Tactic:
exact h n
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p q : FormalMultilinearSeries 𝕜 E F
⊢ min p.radius q.radius ≤ (p + q).radius

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

Premises used: ENNReal.le_of_forall_nnreal_lt
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p q : FormalMultilinearSeries 𝕜 E F
refine : ∀ (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) < min p.radius q.radius), (↑r : ℝ≥0∞) ≤ (p + q).radius
⊢ min p.radius q.radius ≤ (p + q).radius

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

Premises used: ENNReal.le_of_forall_nnreal_lt
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p q : FormalMultilinearSeries 𝕜 E F
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.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p q : FormalMultilinearSeries 𝕜 E F
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.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p q : FormalMultilinearSeries 𝕜 E F
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 + q).radius

Tactic:
(p + q).le_radius_of_isBigO ((isBigO_of_le _ fun n => ?_).trans this)

Premises used: Asymptotics.IsBigO.trans, FormalMultilinearSeries.le_radius_of_isBigO, HAdd.hAdd, Asymptotics.isBigO_of_le
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p q : FormalMultilinearSeries 𝕜 E F
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
refine : ∀ (n : ℕ), ‖‖(p + q) n‖ * (↑r : ℝ) ^ n‖ ≤ ‖‖p n‖ * (↑r : ℝ) ^ n + ‖q n‖ * (↑r : ℝ) ^ n‖
⊢ (↑r : ℝ≥0∞) ≤ (p + q).radius

Tactic:
refine (p + q).le_radius_of_isBigO ((isBigO_of_le _ fun n => ?_).trans this)

Premises used: Asymptotics.IsBigO.trans, FormalMultilinearSeries.le_radius_of_isBigO, HAdd.hAdd, Asymptotics.isBigO_of_le
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p q : FormalMultilinearSeries 𝕜 E F
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 : ℕ
rw : ‖(p + q) n‖ * ‖(↑r : ℝ) ^ n‖ ≤ ‖‖p n‖ + ‖q n‖‖ * ‖(↑r : ℝ) ^ n‖
⊢ ‖‖(p + q) n‖ * (↑r : ℝ) ^ n‖ ≤ ‖‖p n‖ * (↑r : ℝ) ^ n + ‖q n‖ * (↑r : ℝ) ^ n‖

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

Premises used: add_mul, norm_mul, norm_norm
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p q : FormalMultilinearSeries 𝕜 E F
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 : ℕ
hbc : ‖(p + q) n‖ ≤ ‖‖p n‖ + ‖q n‖‖
⊢ ‖(p + q) n‖ * ‖(↑r : ℝ) ^ n‖ ≤ ‖‖p n‖ + ‖q n‖‖ * ‖(↑r : ℝ) ^ n‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p q : FormalMultilinearSeries 𝕜 E F
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 + q) n‖ ≤ ‖‖p n‖ + ‖q n‖‖

Tactic:
(norm_add_le _ _).trans (le_abs_self _)

Premises used: le_abs_self, norm_add_le, LE.le.trans
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p q : FormalMultilinearSeries 𝕜 E F
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 + q) n‖ ≤ ‖‖p n‖ + ‖q n‖‖

Tactic:
exact (norm_add_le _ _).trans (le_abs_self _)

Premises used: le_abs_self, norm_add_le, LE.le.trans
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
⊢ (-p).radius = p.radius

Tactic:
simp only [radius, neg_apply, norm_neg]

Premises used: FormalMultilinearSeries.neg_apply, FormalMultilinearSeries.radius, norm_neg
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
𝕜' : Type u_5
c : 𝕜'
inst_5 : NormedRing 𝕜'
inst_6 : Module 𝕜' F
inst_7 : SMulCommClass 𝕜 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
⊢ LE.le (α := ℝ≥0∞) (⨆ (r : ℝ≥0), ⨆ (C : ℝ), ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C), (↑r : ℝ≥0∞))
    (⨆ (r : ℝ≥0), ⨆ (C : ℝ), ⨆ (_ : ∀ (n : ℕ), ‖c • p n‖ * (↑r : ℝ) ^ n ≤ C), (↑r : ℝ≥0∞))

Tactic:
iSup_mono fun r ↦ iSup_mono' fun C ↦ ⟨‖c‖ * C, iSup_mono' fun h ↦ ?_⟩

Premises used: Norm.norm, HMul.hMul, iSup_mono', Exists.intro, iSup_mono
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
𝕜' : Type u_5
c : 𝕜'
inst_5 : NormedRing 𝕜'
inst_6 : Module 𝕜' F
inst_7 : SMulCommClass 𝕜 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
refine :
  ∀ (r : ℝ≥0) (C : ℝ) (h : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C),
    ∃ (_ : ∀ (n : ℕ), ‖c • p n‖ * (↑r : ℝ) ^ n ≤ ‖c‖ * C), (↑r : ℝ≥0∞) ≤ (↑r : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (⨆ (r : ℝ≥0), ⨆ (C : ℝ), ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C), (↑r : ℝ≥0∞))
    (⨆ (r : ℝ≥0), ⨆ (C : ℝ), ⨆ (_ : ∀ (n : ℕ), ‖c • p n‖ * (↑r : ℝ) ^ n ≤ C), (↑r : ℝ≥0∞))

Tactic:
refine iSup_mono fun r ↦ iSup_mono' fun C ↦ ⟨‖c‖ * C, iSup_mono' fun h ↦ ?_⟩

Premises used: Norm.norm, HMul.hMul, iSup_mono', Exists.intro, iSup_mono
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
𝕜' : Type u_5
c : 𝕜'
inst_5 : NormedRing 𝕜'
inst_6 : Module 𝕜' F
inst_7 : SMulCommClass 𝕜 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
simp : ∀ (n : ℕ), ‖c • p n‖ * (↑r : ℝ) ^ n ≤ ‖c‖ * C
⊢ ∃ (_ : ∀ (n : ℕ), ‖c • p n‖ * (↑r : ℝ) ^ n ≤ ‖c‖ * C), (↑r : ℝ≥0∞) ≤ (↑r : ℝ≥0∞)

Tactic:
simp only [le_refl, exists_prop, and_true]

Premises used: le_refl, and_true, exists_prop
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
𝕜' : Type u_5
c : 𝕜'
inst_5 : NormedDivisionRing 𝕜'
inst_6 : Module 𝕜' F
inst_7 : NormSMulClass 𝕜' F
inst_8 : SMulCommClass 𝕜 𝕜' F
hc : c ≠ 0
apply : (c • p).radius ≤ p.radius
⊢ (c • p).radius = p.radius

Tactic:
apply eq_of_le_of_ge _ radius_le_smul

Premises used: FormalMultilinearSeries.radius_le_smul, eq_of_le_of_ge
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
𝕜' : Type u_5
c : 𝕜'
inst_5 : NormedDivisionRing 𝕜'
inst_6 : Module 𝕜' F
inst_7 : NormSMulClass 𝕜' F
inst_8 : SMulCommClass 𝕜 𝕜' F
hc : c ≠ 0
⊢ (c • p).radius ≤ p.radius

Tactic:
radius_le_smul.trans_eq (congr_arg _ <| inv_smul_smul₀ hc p)

Premises used: inv_smul_smul₀, LE.le.trans_eq, FormalMultilinearSeries.radius_le_smul, congr_arg
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
𝕜' : Type u_5
c : 𝕜'
inst_5 : NormedDivisionRing 𝕜'
inst_6 : Module 𝕜' F
inst_7 : NormSMulClass 𝕜' F
inst_8 : SMulCommClass 𝕜 𝕜' F
hc : c ≠ 0
⊢ (c • p).radius ≤ p.radius

Tactic:
exact radius_le_smul.trans_eq (congr_arg _ <| inv_smul_smul₀ hc p)

Premises used: inv_smul_smul₀, LE.le.trans_eq, FormalMultilinearSeries.radius_le_smul, congr_arg
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
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 𝕜 F G
u : E →L[𝕜] F
n : ℕ
apply : ‖p n‖ * ∏ i : Fin n, ‖u‖ ≤ ‖p n‖ * ‖u‖ ^ n
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G)
      ((p n).compContinuousLinearMap (M₁ := fun (i : Fin n) ↦ E) (M₁' := fun (i : Fin n) ↦ F) fun (x : Fin n) ↦ u) ≤
    ‖p n‖ * ‖u‖ ^ n

Tactic:
apply le_trans (ContinuousMultilinearMap.norm_compContinuousLinearMap_le _ _)

Premises used: ContinuousMultilinearMap.norm_compContinuousLinearMap_le, le_trans
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
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 𝕜 F G
u : E →L[𝕜] F
n : ℕ
⊢ ‖p n‖ * ∏ i : Fin n, ‖u‖ ≤ ‖p n‖ * ‖u‖ ^ n

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
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 𝕜 F G
u : E →L[𝕜] F
n : ℕ
⊢ 0 ≤ ‖u‖

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
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 𝕜 F G
u : E →L[𝕜] F
n : ℕ
⊢ 0 ≤ ‖p n‖

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
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 𝕜 F G
u : E →L[𝕜] F
n : ℕ
rw : ENNReal.ofReal ‖p.compContinuousLinearMap u n‖ ≤ ENNReal.ofReal (‖p n‖ * ‖u‖ ^ n)
⊢ ‖p.compContinuousLinearMap u n‖ₑ ≤ ‖p n‖ₑ * ‖u‖ₑ ^ n

Tactic:
rw [← ofReal_norm, ← ofReal_norm, ← ofReal_norm,
    ← ENNReal.ofReal_pow (by simp), ← ENNReal.ofReal_mul (by simp)]

Premises used: ENNReal.ofReal_mul, ofReal_norm, ENNReal.ofReal_pow
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
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 𝕜 F G
u : E →L[𝕜] F
n : ℕ
h : ‖p.compContinuousLinearMap u n‖ ≤ ‖p n‖ * ‖u‖ ^ n
⊢ ENNReal.ofReal ‖p.compContinuousLinearMap u n‖ ≤ ENNReal.ofReal (‖p n‖ * ‖u‖ ^ n)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
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 𝕜 F G
u : E →L[𝕜] F
n : ℕ
⊢ ‖p.compContinuousLinearMap u n‖ ≤ ‖p n‖ * ‖u‖ ^ n

Tactic:
apply norm_compContinuousLinearMap_le

Premises used: FormalMultilinearSeries.norm_compContinuousLinearMap_le
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
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 𝕜 F G
u : E →L[𝕜] F
n : ℕ
⊢ ‖p.compContinuousLinearMap u n‖₊ ≤ ‖p n‖₊ * ‖u‖₊ ^ n

Tactic:
norm_compContinuousLinearMap_le p u n

Premises used: FormalMultilinearSeries.norm_compContinuousLinearMap_le
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
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 𝕜 F G
u : E →L[𝕜] F
inl : p.radius / enorm (E := E →L[𝕜] F) 0 ≤ radius.{u_1, u_2, u_4} (E := E) (p.compContinuousLinearMap 0)
inr : ∀ (h_zero : 0 < ‖u‖₊), p.radius / ‖u‖ₑ ≤ radius (p.compContinuousLinearMap u)
⊢ p.radius / ‖u‖ₑ ≤ radius (p.compContinuousLinearMap u)

Tactic:
obtain (rfl | h_zero) := eq_zero_or_nnnorm_pos u

Premises used: eq_zero_or_nnnorm_pos, rfl
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
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 𝕜 F G
⊢ p.radius / enorm (E := E →L[𝕜] F) 0 ≤ radius.{u_1, u_2, u_4} (E := E) (p.compContinuousLinearMap 0)

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
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 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
⊢ ‖u‖ₑ ≠ ∞

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
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 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
inr : p.radius ≤ radius (p.compContinuousLinearMap u) * ‖u‖ₑ
⊢ p.radius / ‖u‖ₑ ≤ radius (p.compContinuousLinearMap u)

Tactic:
rw [ENNReal.div_le_iff (by simpa using h_zero) (by simp)]

Premises used: ENNReal.div_le_iff
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
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 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
⊢ p.radius ≤ radius (p.compContinuousLinearMap u) * ‖u‖ₑ

Tactic:
le_of_forall_nnreal_lt fun r hr ↦ ?_

Premises used: ENNReal.le_of_forall_nnreal_lt
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
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 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
inr : ∀ (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) < p.radius), (↑r : ℝ≥0∞) ≤ radius (p.compContinuousLinearMap u) * ‖u‖ₑ
⊢ p.radius ≤ radius (p.compContinuousLinearMap u) * ‖u‖ₑ

Tactic:
refine le_of_forall_nnreal_lt fun r hr ↦ ?_

Premises used: ENNReal.le_of_forall_nnreal_lt