have (And.intro (_ : Integer.Sqrt1 (sgn b)) (_ : sgn a ≃ sgn b)) :=
  Integer.mul_sqrt1_eqv.mp this
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
a b : Integer.Impl.Difference ℕ
b_nonzero✝ : Nonzero b
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝ : x ≃ Rational.from_integer a / Rational.from_integer b
this : sgn a * sgn b ≃ 1
⊢ AltPositive x
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
a b : Integer.Impl.Difference ℕ
b_nonzero✝ : Nonzero b
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝ : x ≃ Rational.from_integer a / Rational.from_integer b
this : sgn a * sgn b ≃ 1
left✝ : Integer.Sqrt1 (sgn b)
right✝ : sgn a ≃ sgn b
⊢ AltPositive x