have : Positive b := positive_iff_sign_pos1.mpr ‹NonzeroWithSign b 1›
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝³ : NonzeroWithSign a s
this✝² : NonzeroWithSign b s
x✝ : Positive a
this✝¹ : NonzeroWithSign a 1
this✝ : s ≃ 1
this : NonzeroWithSign b 1
⊢ Positive b
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝⁴ : NonzeroWithSign a s
this✝³ : NonzeroWithSign b s
x✝ : Positive a
this✝² : NonzeroWithSign a 1
this✝¹ : s ≃ 1
this✝ : NonzeroWithSign b 1
this : Positive b
⊢ Positive b