match abTri.atLeastOne with
| AA.OneOfThree.first (_ : a - b ≃ 0) =>
  have : a ≃ b := zero_diff_iff_eqv.mp ‹a - b ≃ 0›
  exact AA.OneOfThree.second ‹a ≃ b›
| AA.OneOfThree.second (_ : Positive (a - b)) =>
  have : a > b := gt_iff_pos_diff.mpr ‹Positive (a - b)›
  exact AA.OneOfThree.third ‹a > b›
| AA.OneOfThree.third (_ : Negative (a - b)) =>
  have : a < b := lt_iff_neg_diff.mpr ‹Negative (a - b)›
  exact AA.OneOfThree.first ‹a < b›
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)
no goals