exact ⟨T, S, hT, hS, hTₛ, hTₑ, rfl⟩
case intro.intro.intro.intro.intro.intro.intro.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 k T : M
left✝² : T < U
hT : IsSeries U I L A (k / ‖I‖) T
hTₛ : T{L}[0] = 0
S : M
left✝¹ : S < U
hS : IsSegment L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) S
hTₑ : T{L}[k / ‖I‖] = S{L}[0]
left✝ : S{L}[0] ≤ S{L}[k % ‖I‖]
⊢ ∃ T S_1,
    IsSeries U I L A (k / ‖I‖) T ∧
      IsSegment L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) S_1 ∧
        T{L}[0] = 0 ∧ T{L}[k / ‖I‖] = S_1{L}[0] ∧ S_1{L}[k % ‖I‖] = S{L}[k % ‖I‖]
no goals