match this with
| AA.OneOfThree.first (_ : p.numerator ≃ 0) =>
  have : sgn p ≃ 0 := calc
    sgn p           ≃ _ := Rel.refl
    sgn p.numerator ≃ _ := Integer.sgn_zero.mp ‹p.numerator ≃ 0›
    0               ≃ _ := Rel.refl
  exact AA.OneOfThree.first this
| AA.OneOfThree.second (_ : Positive p.numerator) =>
  have : sgn p ≃ 1 := calc
    sgn p           ≃ _ := Rel.refl
    sgn p.numerator ≃ _ := Integer.sgn_positive.mp ‹Positive p.numerator›
    1               ≃ _ := Rel.refl
  exact AA.OneOfThree.second this
| AA.OneOfThree.third (_ : Negative p.numerator) =>
  have : sgn p ≃ -1 := calc
    sgn p           ≃ _ := Rel.refl
    sgn p.numerator ≃ _ := Integer.sgn_negative.mp ‹Negative p.numerator›
    (-1)            ≃ _ := Rel.refl
  exact AA.OneOfThree.third this
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
no goals