have : (-1 : ℤ) ≃ 1 := calc
  (-1 : ℤ) ≃ _ := Rel.symm ‹a * b ≃ -1›
  a * b    ≃ _ := AA.substL ‹a ≃ b›
  b * b    ≃ _ := ‹Sqrt1 b›.elim
  1        ≃ _ := Rel.refl
ℕ : 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
⊢ False
ℕ : 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
⊢ False