have : NonzeroWithSign (a * b) 1 :=
  NonzeroWithSign.subst_sign ‹sgn a * sgn b ≃ 1› nws_ab_sgn
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a b : ℤ
inst✝ : Nonzero (a * b)
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
nws_ab_sgn : NonzeroWithSign (a * b) (sgn a * sgn b)
x✝ : sgn a ≃ sgn b
this✝ : Sqrt1 (sgn b) ∧ sgn a ≃ sgn b
this : sgn a * sgn b ≃ 1
⊢ Positive (a * b)
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a b : ℤ
inst✝ : Nonzero (a * b)
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
nws_ab_sgn : NonzeroWithSign (a * b) (sgn a * sgn b)
x✝ : sgn a ≃ sgn b
this✝¹ : Sqrt1 (sgn b) ∧ sgn a ≃ sgn b
this✝ : sgn a * sgn b ≃ 1
this : NonzeroWithSign (a * b) 1
⊢ Positive (a * b)