rcases HT with ⟨T, _, HT, Tₛ, rfl⟩
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
iter n n' : M
HT : Series U I L A iter n
HS : Segment U L A (‖I‖ * iter) ‖I‖ n n'
hiter : iter < ‖I‖
Hn : n ≤ ‖I‖ * iter
⊢ Series U I L A (iter + 1) n'
case intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
iter n' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
⊢ Series U I L A (iter + 1) n'