case mp =>
  intro (h : compare n m = Ordering.gt)
  show lt m n
  simp [compare, Ord.compare, compareOfLessAndEq] at h
  split at h
  case isTrue =>
    have : n < m := by assumption
    contradiction
  case isFalse =>
    split at h
    case isTrue =>
      have : n = m := by assumption
      contradiction
    case isFalse =>
      have : ¬(n < m) := by assumption
      have : ¬(n = m) := by assumption
      have : n > m ∨ n ≤ m := Nat.lt_or_ge m n
      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
⊢ compare n m = Ordering.gt → lt m n
no goals