calc
  sgn a₁ ≃ _ := sgn_zero.mp ‹a₁ ≃ 0›
  0      ≃ _ := Rel.symm (sgn_zero.mp ‹a₂ ≃ 0›)
  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₁)
a✝ : a₁ ≃ 0
this : a₂ ≃ 0
⊢ sgn a₁ ≃ sgn a₂
no goals