match this with
| AA.OneOfThree.first (_ : a ≃ 0) =>
  have : sgn a ≃ 0 := sgn_zero.mp ‹a ≃ 0›
  calc
    sgn (sgn a) ≃ _ := sgn_subst ‹sgn a ≃ 0›
    sgn (0 : ℤ) ≃ _ := sgn_subst (Rel.symm ‹a ≃ 0›)
    sgn a       ≃ _ := Rel.refl
| AA.OneOfThree.second (_ : Positive a) =>
  have : sgn a ≃ 1 := sgn_positive.mp ‹Positive a›
  calc
    sgn (sgn a) ≃ _ := sgn_subst ‹sgn a ≃ 1›
    sgn (1 : ℤ) ≃ _ := sgn_positive.mp one_positive
    1           ≃ _ := Rel.symm ‹sgn a ≃ 1›
    sgn a       ≃ _ := Rel.refl
| AA.OneOfThree.third (_ : Negative a) =>
  have : sgn a ≃ -1 := sgn_negative.mp ‹Negative a›
  calc
    sgn (sgn a)  ≃ _ := sgn_subst ‹sgn a ≃ -1›
    sgn (-1 : ℤ) ≃ _ := sgn_negative.mp neg_one_negative
    (-1)         ≃ _ := Rel.symm ‹sgn a ≃ -1›
    sgn a        ≃ _ := Rel.refl
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ sgn (sgn a) ≃ sgn a
no goals