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