simp [Eq.comm]
case h.h.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin 6 → M
T : M
a✝¹ : T < v 0
a✝ : IsSeries (v 0) (v 1) (v 2) (v 3) (v 4) T
⊢ T{v 2}[0] = 0 ∧ T{v 2}[v 4] = v 5 ↔ 0 = T{v 2}[0] ∧ v 5 = T{v 2}[v 4]
no goals