case mpr =>
  intro (_ : SameSign a b)
  show Positive ab
  have (SameSign.intro (s : ℤ) (_ : Sqrt1 s) nwsa nwsb) := ‹SameSign a b›
  have : NonzeroWithSign a s := nwsa
  have : NonzeroWithSign b s := nwsb
  have : s * s ≃ 1 := ‹Sqrt1 s›.elim
  have : NonzeroWithSign ab (s * s) :=
    mul_preserves_nonzeroWithSign nwsa nwsb
  have : NonzeroWithSign ab 1 :=
    NonzeroWithSign.subst_sign ‹s * s ≃ 1› ‹NonzeroWithSign ab (s * s)›
  have : Positive ab := positive_iff_sign_pos1.mpr ‹NonzeroWithSign ab 1›
  exact this
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
⊢ SameSign a b → Positive (a * b)
no goals