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)›
n m : Nat
x✝ : n ≃ m
h✝ : n < m
⊢ False
no goals