exact absurd ‹(-1 : ℤ) ≃ 1› ‹(-1 : ℤ) ≄ 1›
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
x✝¹ : a * b ≃ -1
x✝ : a ≃ b
this✝ : -1 ≃ 1
this : -1 ≄ 1
⊢ False
no goals