match tri.atLeastOne with
| AA.OneOfThree.first (_ : a ≃ 0) =>
  exact Or.inl ‹a ≃ 0›
| AA.OneOfThree.second (_ : Positive a) =>
  have : Nonzero a := nonzero_iff_pos_or_neg.mpr (Or.inl ‹Positive a›)
  exact Or.inr ‹Nonzero a›
| AA.OneOfThree.third (_ : Negative a) =>
  have : Nonzero a := nonzero_iff_pos_or_neg.mpr (Or.inr ‹Negative a›)
  exact Or.inr ‹Nonzero a›
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ a ≃ 0 ∨ Nonzero a
no goals