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