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