have : n ≃ 1 := Natural.sqrt1.mp ‹n * n ≃ 1›
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
n : ℕ
left✝ : Positive n
right✝ : a ≃ -coe n
this✝ : coe (n * n) ≃ 1
this : n * n ≃ 1
⊢ a ≃ -1
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
n : ℕ
left✝ : Positive n
right✝ : a ≃ -coe n
this✝¹ : coe (n * n) ≃ 1
this✝ : n * n ≃ 1
this : n ≃ 1
⊢ a ≃ -1