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
this :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
h : ∃ (i : ℝ≥0) (i_1 : ℝ) (_ : ∀ (n : ℕ), ‖p n‖ * (↑i : ℝ) ^ n ≤ i_1), (↑r : ℝ≥0∞) < (↑i : ℝ≥0∞)
rcases :
  ∀ (t : ℝ≥0) (C : ℝ) (hC : ∀ (n : ℕ), ‖p n‖ * (↑t : ℝ) ^ n ≤ C) (rt : (↑r : ℝ≥0∞) < (↑t : ℝ≥0∞)),
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
⊢ ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n

Tactic:
rcases h with ⟨t, C, hC, rt⟩
-- 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
this :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * (↑t : ℝ) ^ n ≤ C
rt : (↑r : ℝ≥0∞) < (↑t : ℝ≥0∞)
⊢ (↑r : ℝ) < (↑t : ℝ)

Tactic:
rw [ENNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at rt

Premises used: ENNReal.coe_lt_coe, NNReal.coe_lt_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
this :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * (↑t : ℝ) ^ n ≤ C
rt : (↑r : ℝ) < (↑t : ℝ)
⊢ 0 < (↑t : ℝ)

Tactic:
have : 0 < (t : ℝ) := r.coe_nonneg.trans_lt rt
-- 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
this_1 :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * (↑t : ℝ) ^ n ≤ C
rt : (↑r : ℝ) < (↑t : ℝ)
this : 0 < (↑t : ℝ)
⊢ (↑r : ℝ) / (↑t : ℝ) < 1

Tactic:
rw [← div_lt_one this] at rt

Premises used: div_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
r : ℝ≥0
this_1 :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * (↑t : ℝ) ^ n ≤ C
rt : (↑r : ℝ) < (↑t : ℝ)
this : 0 < (↑t : ℝ)
rt₁ : (↑r : ℝ) / (↑t : ℝ) < 1
⊢ 0 < (↑t : ℝ)

Tactic:
rw [← div_lt_one this] at rt

Premises used: div_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
r : ℝ≥0
this_1 :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * (↑t : ℝ) ^ n ≤ C
rt : (↑r : ℝ) / (↑t : ℝ) < 1
this : 0 < (↑t : ℝ)
⊢ ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n

Tactic:
⟨_, rt, C, Or.inr zero_lt_one, fun n => ?_⟩

Premises used: zero_lt_one, And.intro, Exists.intro, Or.inr
-- 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
this_1 :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * (↑t : ℝ) ^ n ≤ C
rt : (↑r : ℝ) / (↑t : ℝ) < 1
this : 0 < (↑t : ℝ)
refine : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * ((↑r : ℝ) / (↑t : ℝ)) ^ n
⊢ ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n

Tactic:
refine ⟨_, rt, C, Or.inr zero_lt_one, 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
r : ℝ≥0
this_1 :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * (↑t : ℝ) ^ n ≤ C
rt : (↑r : ℝ) / (↑t : ℝ) < 1
this : 0 < (↑t : ℝ)
n : ℕ
⊢ |‖p n‖ * (↑r : ℝ) ^ n| = ‖p n‖ * (↑t : ℝ) ^ n * ((↑r : ℝ) / (↑t : ℝ)) ^ n

Tactic:
simp [field, abs_mul, div_pow]

Premises used: abs_mul, 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
this_1 :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * (↑t : ℝ) ^ n ≤ C
rt : (↑r : ℝ) / (↑t : ℝ) < 1
this : 0 < (↑t : ℝ)
n : ℕ
hbc : ‖p n‖ * (↑t : ℝ) ^ n ≤ C
⊢ ‖p n‖ * (↑t : ℝ) ^ n * ((↑r : ℝ) / (↑t : ℝ)) ^ n ≤ C * ((↑r : ℝ) / (↑t : ℝ)) ^ 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 : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this_1 :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * (↑t : ℝ) ^ n ≤ C
rt : (↑r : ℝ) / (↑t : ℝ) < 1
this : 0 < (↑t : ℝ)
n : ℕ
⊢ ‖p n‖ * (↑t : ℝ) ^ n ≤ C

Tactic:
apply hC
-- 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
this_1 :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * (↑t : ℝ) ^ n ≤ C
rt : (↑r : ℝ) / (↑t : ℝ) < 1
this : 0 < (↑t : ℝ)
n : ℕ
n₁ : |‖p n‖ * (↑r : ℝ) ^ n| = ‖p n‖ * (↑t : ℝ) ^ n * ((↑r : ℝ) / (↑t : ℝ)) ^ n
n₂ : ‖p n‖ * (↑t : ℝ) ^ n * ((↑r : ℝ) / (↑t : ℝ)) ^ n ≤ C * ((↑r : ℝ) / (↑t : ℝ)) ^ n
⊢ |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * ((↑r : ℝ) / (↑t : ℝ)) ^ n

Tactic:
calc
    |‖p n‖ * (r : ℝ) ^ n| = ‖p n‖ * (t : ℝ) ^ n * (r / t : ℝ) ^ n := by
      simp [field, abs_mul, div_pow]
    _ ≤ C * (r / t : ℝ) ^ n := by gcongr; apply hC

Premises used: HDiv.hDiv, NNReal.toReal
-- 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
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1

Tactic:
let ⟨_, ha, hp⟩ := p.isLittleO_of_lt_radius h
  hp.trans <| (isLittleO_pow_pow_of_lt_left ha.1.le ha.2).congr (fun _ => rfl) one_pow

Premises used: one_pow, Norm.norm, HMul.hMul, LT.lt.le, Filter.atTop, HPow.hPow, And.right, And.left, FormalMultilinearSeries.isLittleO_of_lt_radius, isLittleO_pow_pow_of_lt_left, Asymptotics.IsLittleO.congr, Asymptotics.IsLittleO, _private.0.FormalMultilinearSeries.isLittleO_one_of_lt_radius.match_1, OfNat.ofNat, NNReal.toReal, rfl, Asymptotics.IsLittleO.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
⊢ ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n

Tactic:
have := ((TFAE_exists_lt_isLittleO_pow (fun n => ‖p n‖ * (r : ℝ) ^ n) 1).out 1 5).mp
    (p.isLittleO_of_lt_radius h)
-- 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
this : ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
rcases :
  ∀ (a : ℝ) (ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a) (C : ℝ) (hC : C > 0)
    (H : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n),
    ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C * a ^ n
⊢ ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C * a ^ n

Tactic:
rcases this with ⟨a, ha, C, hC, H⟩
-- 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 : ℝ
hC : C > 0
H : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
⊢ ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C * a ^ n

Tactic:
⟨a, ha, C, hC, fun n => (le_abs_self _).trans (H n)⟩

Premises used: Norm.norm, le_abs_self, HMul.hMul, HPow.hPow, And.intro, Exists.intro, LE.le.trans, NNReal.toReal
-- 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 : ℝ
hC : C > 0
H : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
⊢ ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C * a ^ n

Tactic:
exact ⟨a, ha, C, hC, fun n => (le_abs_self _).trans (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 : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h₀ : r ≠ 0
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a
hp : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x
⊢ (∃ (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

Tactic:
have := ((TFAE_exists_lt_isLittleO_pow (fun n => ‖p n‖ * (r : ℝ) ^ n) 1).out 2 5)
-- 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
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a
hp : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x
this :
  (∃ (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
rcases :
  ∀ (a : ℝ) (ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a) (C : ℝ) (hC : C > 0)
    (hp : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n), (↑r : ℝ≥0∞) < p.radius
⊢ (↑r : ℝ≥0∞) < p.radius

Tactic:
rcases this.mp ⟨a, ha, hp⟩ with ⟨a, ha, C, hC, hp⟩

Premises used: And.intro, Exists.intro, 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
r : ℝ≥0
h₀ : r ≠ 0
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 :
  (∃ (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
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
rw :
  ∀ (h₀ : 0 < (↑r : ℝ)) {a : ℝ} (ha : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a)
    (hp : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x)
    (this :
      (∃ (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)
    (a : ℝ) (ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a) (C : ℝ) (hC : C > 0)
    (hp : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n), (↑r : ℝ≥0∞) < p.radius
⊢ (↑r : ℝ≥0∞) < p.radius

Tactic:
rw [← pos_iff_ne_zero, ← NNReal.coe_pos] at h₀

Premises used: NNReal.coe_pos, pos_iff_ne_zero
-- 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 :
  (∃ (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
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
⊢ 0 ≤ a

Tactic:
ha.1.le

Premises used: LT.lt.le, And.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
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 :
  (∃ (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
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
lift :
  ∀ (a : ℝ≥0) (ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) (↑a : ℝ))
    (hp : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * (↑a : ℝ) ^ n), (↑r : ℝ≥0∞) < p.radius
⊢ (↑r : ℝ≥0∞) < p.radius

Tactic:
lift a to ℝ≥0 using ha.1.le

Premises used: LT.lt.le, And.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
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 :
  (∃ (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
⊢ (↑r : ℝ) < (↑r : ℝ) / (↑a : ℝ)

Tactic:
simpa only [div_one] using (div_lt_div_iff_of_pos_left h₀ zero_lt_one ha.1).2 ha.2

Premises used: Iff.mpr, div_lt_div_iff_of_pos_left, zero_lt_one, And.right, And.left, div_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
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 :
  (∃ (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
⊢ (↑r : ℝ) < (↑r : ℝ) / (↑a : ℝ)

Tactic:
have : (r : ℝ) < r / a := by
    simpa only [div_one] using (div_lt_div_iff_of_pos_left h₀ zero_lt_one ha.1).2 ha.2
-- 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 : ℝ) < (↑r : ℝ) / (↑a : ℝ)
⊢ r < r / a

Tactic:
norm_cast at this
-- 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 < r / a
⊢ (↑r : ℝ≥0∞) < (↑(r / a) : ℝ≥0∞)

Tactic:
rw [← ENNReal.coe_lt_coe] at this

Premises used: ENNReal.coe_lt_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₀ : 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∞)
⊢ (↑r : ℝ≥0∞) < p.radius

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

Premises used: FormalMultilinearSeries.le_radius_of_bound, LT.lt.trans_le