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