case right =>
  intro (And.intro (_ : a ≃ 0) (_ : Nonzero a))
  show False
  apply tri.atMostOne
  show AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
  have : Positive a ∨ Negative a := nonzero_iff_pos_or_neg.mp ‹Nonzero a›
  match ‹Positive a ∨ Negative a› with
  | Or.inl (_ : Positive a) =>
    exact AA.TwoOfThree.oneAndTwo ‹a ≃ 0› ‹Positive a›
  | Or.inr (_ : Negative a) =>
    exact AA.TwoOfThree.oneAndThree ‹a ≃ 0› ‹Negative 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