exact hS₁.uniq hS₂
case intro.intro.intro.intro.intro.intro.refl
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 n₁ n₂ nₘ₁ : M
left✝¹ : nₘ₁ ≤ n₁
hT₁ : Series U I L A (k / ‖I‖) nₘ₁
hS₁ : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ₁ n₁
left✝ : nₘ₁ ≤ n₂
hT₂ : Series U I L A (k / ‖I‖) nₘ₁
hS₂ : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ₁ n₂
⊢ n₁ = n₂
no goals