calc
  _ ≃ sgn (2:ℤ)       := Rel.refl
  _ ≃ sgn (1 + 1 : ℤ) := sgn_subst (Rel.symm add_one_one)
  _ ≃ 1               := add_preserves_sign ‹sgn (1:ℤ) ≃ 1› ‹sgn (1:ℤ) ≃ 1›
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
this : sgn 1 ≃ 1
⊢ sgn 2 ≃ 1
no goals