case mpr =>
  intro (_ : sgn a ≃ sgn b)
  show Positive (a * b)
  have : Sqrt1 (sgn b) ∧ sgn a ≃ sgn b :=
    And.intro ‹Sqrt1 (sgn b)› ‹sgn a ≃ sgn b›
  have : sgn a * sgn b ≃ 1 := mul_sqrt1_eqv.mpr this
  have : NonzeroWithSign (a * b) 1 :=
    NonzeroWithSign.subst_sign ‹sgn a * sgn b ≃ 1› nws_ab_sgn
  have : Positive (a * b) := positive_iff_sign_pos1.mpr this
  exact this
ℕ : 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)
⊢ sgn a ≃ sgn b → Positive (a * b)
no goals