have : Positive a := positive_iff_sign_pos1.mpr ‹NonzeroWithSign a 1›
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝¹ : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝ : s₂ ≃ 1 ∨ s₂ ≃ -1
this : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
left✝ : NonzeroWithSign a 1
right✝ : NonzeroWithSign a (-1)
⊢ s₁ ≃ s₂
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝² : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝¹ : s₂ ≃ 1 ∨ s₂ ≃ -1
this✝ : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
left✝ : NonzeroWithSign a 1
right✝ : NonzeroWithSign a (-1)
this : Positive a
⊢ s₁ ≃ s₂