match ‹n > m ∨ n ≤ m› with
| Or.inl (_ : n > m) =>
  have : m < n := ‹n > m›
  have : lt m n := prelude_lt_iff_impl_lt.mp ‹m < n›
  exact this
| Or.inr (_ : n ≤ m) =>
  have : n = m ∨ n < m := Nat.eq_or_lt_of_le ‹n ≤ m›
  match ‹n = m ∨ n < m› with
  | Or.inl (_ : n = m) =>
    exact absurd ‹n = m› ‹¬(n = m)›
  | Or.inr (_ : n < m) =>
    exact absurd ‹n < m› ‹¬(n < m)›
n m : Nat
h✝¹ : ¬n < m
h✝ : ¬n = m
h : Ordering.gt = Ordering.gt
this✝¹ : ¬n < m
this✝ : ¬n = m
this : n > m ∨ n ≤ m
⊢ lt m n
no goals