if hj : j₁.1 < j₂.1 then
  simp only [hj, true_or, iff_true]
  exact rlexProd_lt_of_snd i₁ i₂ hj
else
  simp only [hj, false_or]
  rewrite [Nat.not_lt] at hj
  cases Nat.eq_or_lt_of_le hj with
  | inl heq =>
    cases Fin.eq_of_val_eq heq
    simp only [true_and]
    exact Nat.add_lt_add_iff_right _ i₁.1 i₂.1
  | inr hlt =>
    have : j₁ ≠ j₂ := fun h =>
      Nat.lt_irrefl _ (h ▸ hlt)
    simp only [this, false_and, iff_false, Nat.not_lt]
    apply Nat.le_of_lt
    exact rlexProd_lt_of_snd i₂ i₁ hlt
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ ↑j₁ < ↑j₂ ∨ j₁ = j₂ ∧ ↑i₁ < ↑i₂
no goals