case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1515814
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x y : E
r R : ℝ≥0
hr : ↑r < radius p
k : ℕ
r' : ℝ≥0
h0 : 0 < r'
hr' : ↑r + ↑r' < radius p
⊢ Summable fun s => ‖p (k + s.fst)‖₊ * r ^ s.fst
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1515814
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x y : E
r R : ℝ≥0
hr : ↑r < radius p
k : ℕ
⊢ Summable fun s => ‖p (k + s.fst)‖₊ * r ^ s.fst
rcases ENNReal.lt_iff_exists_add_pos_lt.1 hr with ⟨r', h0, hr'⟩
no goals
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1515814
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x y : E
r R : ℝ≥0
hr : ↑r < radius p
k : ℕ
r' : ℝ≥0
h0 : 0 < r'
hr' : ↑r + ↑r' < radius p
⊢ Summable fun s => ‖p (k + s.fst)‖₊ * r ^ s.fst
simpa only [mul_inv_cancel_right₀ (pow_pos h0 _).ne'] using
  ((NNReal.summable_sigma.1 (p.changeOriginSeries_summable_aux₁ hr')).1 k).mul_right (r' ^ k)⁻¹