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
x✝ : n ≃ m
h✝ : ¬n < m
⊢ (if n = m then Ordering.eq else Ordering.gt) = Ordering.eq
no goals