match ‹n = m ∨ n < m› with
| Or.inl (_ : n = m) =>
  have : n ≠ m := ‹n ≄ m›
  exact absurd ‹n = m› ‹n ≠ m›
| Or.inr (_ : n < m) =>
  exact ‹n < m›
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
this✝ : n ≤ m
this : n = m ∨ n < m
⊢ n < m
no goals