simp only [hj, true_or, iff_true]
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₁ < ↑j₂
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ ↑j₁ < ↑j₂ ∨ j₁ = j₂ ∧ ↑i₁ < ↑i₂
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₁ < ↑j₂
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂