𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.141980
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < radius p
this : ∃ a, a ∈ Ioo 0 1 ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
⊢ ∃ a, a ∈ Ioo 0 1 ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.141980
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < radius p
⊢ ∃ a, a ∈ Ioo 0 1 ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n
have := ((TFAE_exists_lt_isLittleO_pow (fun n => ‖p n‖ * (r : ℝ) ^ n) 1).out 1 5).mp
  (p.isLittleO_of_lt_radius h)
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.141980
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < radius p
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : C > 0
H : ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
⊢ ∃ a, a ∈ Ioo 0 1 ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.141980
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < radius p
this : ∃ a, a ∈ Ioo 0 1 ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
⊢ ∃ a, a ∈ Ioo 0 1 ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n
rcases this with ⟨a, ha, C, hC, H⟩
no goals
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.141980
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < radius p
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : C > 0
H : ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
⊢ ∃ a, a ∈ Ioo 0 1 ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n
exact ⟨a, ha, C, hC, fun n => (le_abs_self _).trans (H n)⟩