case mp =>
  intro (h : compare n m = Ordering.eq)
  show n ≃ m
  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
      have : n ≃ m := ‹n = m›
      exact this
    case isFalse =>
      have : n ≠ m := by assumption
      contradiction
n m : Nat
⊢ compare n m = Ordering.eq → n ≃ m
no goals