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
r : ℝ≥0
h₀ : 0 < (↑r : ℝ)
a_1 : ℝ
ha_1 : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a_1
hp_1 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a_1 ^ x
this_1 :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a ∧
        IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
C : ℝ
hC : C > 0
a : ℝ≥0
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) (↑a : ℝ)
hp : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * (↑a : ℝ) ^ n
this : (↑r : ℝ≥0∞) < (↑(r / a) : ℝ≥0∞)
refine : ∀ (n : ℕ), ‖p n‖ * (↑(r / a) : ℝ) ^ n ≤ C
⊢ (↑r : ℝ≥0∞) < p.radius

Tactic:
refine this.trans_le (p.le_radius_of_bound C fun n => ?_)

Premises used: FormalMultilinearSeries.le_radius_of_bound, LT.lt.trans_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 : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h₀ : 0 < (↑r : ℝ)
a_1 : ℝ
ha_1 : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a_1
hp_1 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a_1 ^ x
this_1 :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a ∧
        IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
C : ℝ
hC : C > 0
a : ℝ≥0
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) (↑a : ℝ)
hp : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * (↑a : ℝ) ^ n
this : (↑r : ℝ≥0∞) < (↑(r / a) : ℝ≥0∞)
n : ℕ
rw : ‖p n‖ * (↑r : ℝ) ^ n ≤ C * (↑a : ℝ) ^ n
⊢ ‖p n‖ * (↑(r / a) : ℝ) ^ n ≤ C

Tactic:
rw [NNReal.coe_div, div_pow, ← mul_div_assoc, div_le_iff₀ (pow_pos ha.1 n)]

Premises used: div_le_iff₀, pow_pos, NNReal.coe_div, mul_div_assoc, And.left, div_pow
-- 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
r : ℝ≥0
h₀ : 0 < (↑r : ℝ)
a_1 : ℝ
ha_1 : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a_1
hp_1 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a_1 ^ x
this_1 :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a ∧
        IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
C : ℝ
hC : C > 0
a : ℝ≥0
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) (↑a : ℝ)
hp : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * (↑a : ℝ) ^ n
this : (↑r : ℝ≥0∞) < (↑(r / a) : ℝ≥0∞)
n : ℕ
⊢ ‖p n‖ * (↑r : ℝ) ^ n ≤ C * (↑a : ℝ) ^ n

Tactic:
(le_abs_self _).trans (hp n)

Premises used: le_abs_self, 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
r : ℝ≥0
h₀ : 0 < (↑r : ℝ)
a_1 : ℝ
ha_1 : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a_1
hp_1 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a_1 ^ x
this_1 :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a ∧
        IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
C : ℝ
hC : C > 0
a : ℝ≥0
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) (↑a : ℝ)
hp : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * (↑a : ℝ) ^ n
this : (↑r : ℝ≥0∞) < (↑(r / a) : ℝ≥0∞)
n : ℕ
⊢ ‖p n‖ * (↑r : ℝ) ^ n ≤ C * (↑a : ℝ) ^ n

Tactic:
exact (le_abs_self _).trans (hp n)

Premises used: le_abs_self, 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
r : ℝ≥0
h : (↑r : ℝ≥0∞) < p.radius
⊢ ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C

Tactic:
let ⟨_, ha, C, hC, h⟩ := p.norm_mul_pow_le_mul_pow_of_lt_radius h
  ⟨C, hC, fun n => (h n).trans <| mul_le_of_le_one_right hC.lt.le (pow_le_one₀ ha.1.le ha.2.le)⟩

Premises used: GT.gt.lt, Exists, mul_le_of_le_one_right, LT.lt.le, GT.gt, _private.0.FormalMultilinearSeries.norm_mul_pow_le_of_lt_radius.match_1, And, FormalMultilinearSeries.norm_mul_pow_le_mul_pow_of_lt_radius, And.right, And.left, And.intro, Exists.intro, LE.le.trans, OfNat.ofNat, pow_le_one₀
-- 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
r : ℝ≥0
h0 : 0 < r
h : (↑r : ℝ≥0∞) < p.radius
⊢ ∃ C > 0, ∀ (n : ℕ), ‖p n‖ ≤ C / (↑r : ℝ) ^ n

Tactic:
let ⟨C, hC, hp⟩ := p.norm_mul_pow_le_of_lt_radius h
  ⟨C, hC, fun n => Iff.mpr (le_div_iff₀ (pow_pos h0 _)) (hp n)⟩

Premises used: Iff.mpr, pow_pos, Exists, GT.gt, And, And.intro, Exists.intro, le_div_iff₀, OfNat.ofNat, _private.0.FormalMultilinearSeries.norm_le_div_pow_of_pos_of_lt_radius.match_1, 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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : (↑r : ℝ≥0∞) < p.radius
⊢ ∃ C > 0, ∀ (n : ℕ), ‖p n‖₊ * r ^ n ≤ C

Tactic:
let ⟨C, hC, hp⟩ := p.norm_mul_pow_le_of_lt_radius h
  ⟨⟨C, hC.lt.le⟩, hC, mod_cast hp⟩

Premises used: GT.gt.lt, cast, Exists, LT.lt.le, Subtype.mk, GT.gt, And, And.intro, Exists.intro, Eq.refl, OfNat.ofNat, _private.0.FormalMultilinearSeries.norm_le_div_pow_of_pos_of_lt_radius.match_1, 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
r : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) atTop (𝓝 l)
⊢ (↑r : ℝ≥0∞) ≤ p.radius

Tactic:
p.le_radius_of_isBigO (h.isBigO_one _)

Premises used: Filter.Tendsto.isBigO_one, FormalMultilinearSeries.le_radius_of_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
r : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
hs : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n
⊢ (↑r : ℝ≥0∞) ≤ p.radius

Tactic:
p.le_radius_of_tendsto hs.tendsto_atTop_zero

Premises used: Summable.tendsto_atTop_zero, FormalMultilinearSeries.le_radius_of_tendsto
-- 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
x : E
h : p.radius < (↑‖x‖₊ : ℝ≥0∞)
⊢ ¬Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * ‖x‖ ^ n

Tactic:
fun hs => not_le_of_gt h (p.le_radius_of_summable_norm hs)

Premises used: FormalMultilinearSeries.le_radius_of_summable_norm, not_le_of_gt, Not
-- 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
r : ℝ≥0
h : (↑r : ℝ≥0∞) < p.radius
obtain :
  ∀ (a : ℝ) (ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a) (C : ℝ) (hp : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C * a ^ n),
    Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n

Tactic:
obtain ⟨a, ha : a ∈ Ioo (0 : ℝ) 1, C, - : 0 < C, hp⟩ := p.norm_mul_pow_le_mul_pow_of_lt_radius h

Premises used: FormalMultilinearSeries.norm_mul_pow_le_mul_pow_of_lt_radius, OfNat.ofNat, Set.Ioo
-- 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
r : ℝ≥0
h : (↑r : ℝ≥0∞) < p.radius
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hp : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C * a ^ n
x : ℕ
⊢ 0 ≤ ‖p x‖ * (↑r : ℝ) ^ x

Tactic:
positivity
-- 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
r : ℝ≥0
h : (↑r : ℝ≥0∞) < p.radius
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hp : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C * a ^ n
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n

Tactic:
exact .of_nonneg_of_le (fun _ ↦ by positivity)
    hp ((summable_geometric_of_lt_one ha.1.le ha.2).mul_left _)
-- 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
x : E
hx : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) x
⊢ ‖x‖ₑ < p.radius

Tactic:
rw [mem_eball_zero_iff] at hx

Premises used: mem_eball_zero_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 : FormalMultilinearSeries 𝕜 E F
x : E
hx : ‖x‖ₑ < p.radius
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ norm.{u_3} (E := F) ((p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ x : F)

Tactic:
.of_nonneg_of_le
    (fun _ ↦ norm_nonneg _) (fun n ↦ ((p n).le_opNorm _).trans_eq ?_) (p.summable_norm_mul_pow hx)

Premises used: LE.le.trans_eq, ContinuousMultilinearMap.le_opNorm, Summable.of_nonneg_of_le, FormalMultilinearSeries.summable_norm_mul_pow, DFunLike.coe, norm_nonneg
-- 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
x : E
hx : ‖x‖ₑ < p.radius
refine : ∀ (n : ℕ), ‖p n‖ * ∏ i : Fin n, ‖x‖ = ‖p n‖ * (↑‖x‖₊ : ℝ) ^ n
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ norm.{u_3} (E := F) ((p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ x : F)

Tactic:
refine .of_nonneg_of_le
    (fun _ ↦ norm_nonneg _) (fun n ↦ ((p n).le_opNorm _).trans_eq ?_) (p.summable_norm_mul_pow hx)
-- 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
x : E
hx : ‖x‖ₑ < p.radius
n : ℕ
⊢ ‖p n‖ * ∏ i : Fin n, ‖x‖ = ‖p n‖ * (↑‖x‖₊ : ℝ) ^ n

Tactic:
simp
-- 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
r : ℝ≥0
h : (↑r : ℝ≥0∞) < p.radius
rw : Summable (α := ℝ) fun (a : ℕ) ↦ (↑(‖p a‖₊ * r ^ a) : ℝ)
⊢ Summable (α := ℝ≥0) fun (n : ℕ) ↦ ‖p n‖₊ * r ^ n

Tactic:
rw [← NNReal.summable_coe]

Premises used: NNReal.summable_coe
-- 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
r : ℝ≥0
h : (↑r : ℝ≥0∞) < p.radius
⊢ Summable (α := ℝ) fun (a : ℕ) ↦ ‖p a‖ * (↑r : ℝ) ^ a

Tactic:
p.summable_norm_mul_pow h

Premises used: FormalMultilinearSeries.summable_norm_mul_pow
-- 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
r : ℝ≥0
h : (↑r : ℝ≥0∞) < p.radius
⊢ Summable (α := ℝ) fun (a : ℕ) ↦ ‖p a‖ * (↑r : ℝ) ^ a

Tactic:
exact p.summable_norm_mul_pow h

Premises used: FormalMultilinearSeries.summable_norm_mul_pow
-- 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
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x : E
hx : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) x
⊢ Summable.{u_3, 0} (α := F) fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ x

Tactic:
(p.summable_norm_apply hx).of_norm

Premises used: Summable.of_norm, FormalMultilinearSeries.summable_norm_apply
-- 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
hs : ∀ (r : ℝ≥0), Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n
⊢ p.radius = ∞

Tactic:
ENNReal.eq_top_of_forall_nnreal_le fun r => p.le_radius_of_summable_norm (hs r)

Premises used: ENNReal.eq_top_of_forall_nnreal_le, FormalMultilinearSeries.le_radius_of_summable_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 : FormalMultilinearSeries 𝕜 E F
mp : p.radius = ∞ → ∀ (r : ℝ≥0), Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n
mpr : (∀ (r : ℝ≥0), Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) → p.radius = ∞
⊢ p.radius = ∞ ↔ ∀ (r : ℝ≥0), Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n

Tactic:
constructor
-- 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 : p.radius = ∞
r : ℝ≥0
mp :
  ∀ (a : ℝ) (ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a) (C : ℝ) (hp : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C * a ^ n),
    Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n

Tactic:
obtain ⟨a, ha : a ∈ Ioo (0 : ℝ) 1, C, - : 0 < C, hp⟩ := p.norm_mul_pow_le_mul_pow_of_lt_radius
      (show (r : ℝ≥0∞) < p.radius from h.symm ▸ ENNReal.coe_lt_top)

Premises used: Eq.rec, FormalMultilinearSeries.norm_mul_pow_le_mul_pow_of_lt_radius, OfNat.ofNat, Eq.symm, Set.Ioo, ENNReal.coe_lt_top
-- 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 : p.radius = ∞
r : ℝ≥0
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hp : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C * a ^ n
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n

Tactic:
.of_norm_bounded
      (g := fun n ↦ (C : ℝ) * a ^ n) ((summable_geometric_of_lt_one ha.1.le ha.2).mul_left _)
      fun n ↦ ?_

Premises used: LT.lt.le, Summable.mul_left, And.right, And.left, Summable.of_norm_bounded, summable_geometric_of_lt_one
-- 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 : p.radius = ∞
r : ℝ≥0
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hp : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C * a ^ n
mp : ∀ (n : ℕ), ‖‖p n‖ * (↑r : ℝ) ^ n‖ ≤ (fun (n : ℕ) ↦ C * a ^ n) n
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n

Tactic:
refine .of_norm_bounded
      (g := fun n ↦ (C : ℝ) * a ^ n) ((summable_geometric_of_lt_one ha.1.le ha.2).mul_left _)
      fun 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 : p.radius = ∞
r : ℝ≥0
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hp : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C * a ^ n
n : ℕ
⊢ ‖p n‖ * (↑r : ℝ) ^ n ≤ C * a ^ n

Tactic:
specialize hp 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 : p.radius = ∞
r : ℝ≥0
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
n : ℕ
hp : ‖p n‖ * (↑r : ℝ) ^ n ≤ C * a ^ n
⊢ 0 ≤ ‖p n‖ * (↑r : ℝ) ^ n

Tactic:
positivity
-- 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 : p.radius = ∞
r : ℝ≥0
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
n : ℕ
hp : ‖p n‖ * (↑r : ℝ) ^ n ≤ C * a ^ n
mp mp₁ mp₂ mp₃ : ‖p n‖ * (↑r : ℝ) ^ n ≤ (fun (n : ℕ) ↦ C * a ^ n) n
⊢ ‖‖p n‖ * (↑r : ℝ) ^ n‖ ≤ (fun (n : ℕ) ↦ C * a ^ n) n

Tactic:
rwa [Real.norm_of_nonneg (by positivity)]

Premises used: Real.norm_of_nonneg
-- 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
⊢ (∀ (r : ℝ≥0), Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) → p.radius = ∞

Tactic:
p.radius_eq_top_of_summable_norm

Premises used: FormalMultilinearSeries.radius_eq_top_of_summable_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 : FormalMultilinearSeries 𝕜 E F
⊢ (∀ (r : ℝ≥0), Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) → p.radius = ∞

Tactic:
exact p.radius_eq_top_of_summable_norm

Premises used: FormalMultilinearSeries.radius_eq_top_of_summable_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 : FormalMultilinearSeries 𝕜 E F
h : 0 < p.radius
rcases :
  ∀ (r : ℝ≥0) (r0 : 0 < (↑r : ℝ≥0∞)) (rlt : (↑r : ℝ≥0∞) < p.radius),
    ∃ (C : ℝ) (r : ℝ) (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
⊢ ∃ (C : ℝ) (r : ℝ) (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n

Tactic:
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 h with ⟨r, r0, rlt⟩

Premises used: ENNReal.lt_iff_exists_nnreal_btwn, Iff.mp
-- 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
⊢ 0 < (↑r : ℝ)

Tactic:
simp [ENNReal.coe_pos.1 r0]

Premises used: ENNReal.coe_pos, Iff.mp
-- 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
⊢ 0 < (↑r : ℝ)

Tactic:
have rpos : 0 < (r : ℝ) := by simp [ENNReal.coe_pos.1 r0]
-- 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 : ℝ)
rcases :
  ∀ (C : ℝ) (Cpos : C > 0) (hCp : ∀ (n : ℕ), ‖p n‖ ≤ C / (↑r : ℝ) ^ n),
    ∃ (C : ℝ) (r : ℝ) (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
⊢ ∃ (C : ℝ) (r : ℝ) (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n

Tactic:
rcases norm_le_div_pow_of_pos_of_lt_radius p rpos rlt with ⟨C, Cpos, hCp⟩

Premises used: FormalMultilinearSeries.norm_le_div_pow_of_pos_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
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
⊢ 0 < (↑r : ℝ)⁻¹

Tactic:
simp only [inv_pos, rpos]

Premises used: inv_pos
-- 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
refine : ∀ (n : ℕ), ‖p n‖ ≤ C * (↑r : ℝ)⁻¹ ^ n
⊢ ∃ (C : ℝ) (r : ℝ) (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n

Tactic:
refine ⟨C, r⁻¹, Cpos, by simp only [inv_pos, rpos], fun 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 : ℕ
rw : ‖p n‖ ≤ C / (↑r : ℝ) ^ n
⊢ ‖p n‖ ≤ C * (↑r : ℝ)⁻¹ ^ n

Tactic:
rw [inv_pow, ← div_eq_mul_inv]

Premises used: inv_pow, div_eq_mul_inv