case mpr =>
  intro (_ : lt n m)
  show compare n m = Ordering.lt
  simp only [compare, Ord.compare, compareOfLessAndEq]
  split
  case isTrue =>
    show Ordering.lt = Ordering.lt
    rfl
  case isFalse =>
    have : ¬(n < m) := by assumption
    have : n < m := prelude_lt_iff_impl_lt.mpr ‹lt n m›
    exact absurd ‹n < m› ‹¬(n < m)›
n m : Nat
⊢ lt n m → compare n m = Ordering.lt
no goals