match this with
| Or.inl (_ : sgn b ≃ 1) =>
  have : sgn a ≃ 1 := Rel.trans ‹sgn a ≃ sgn b› ‹sgn b ≃ 1›
  have : AP (Positive a) := AP.mk (Integer.sgn_positive.mpr ‹sgn a ≃ 1›)
  have : AP (Positive b) := AP.mk (Integer.sgn_positive.mpr ‹sgn b ≃ 1›)
  exact AltPositive.mk ‹x ≃ a / b›
| Or.inr (_ : sgn b ≃ -1) =>
  have : sgn (-b) ≃ 1 := calc
    sgn (-b)   ≃ _ := Integer.sgn_compat_neg
    (-(sgn b)) ≃ _ := AA.subst₁ ‹sgn b ≃ -1›
    (-(-1))    ≃ _ := Integer.neg_involutive
    1          ≃ _ := Rel.refl
  have : sgn (-a) ≃ 1 := calc
    sgn (-a)   ≃ _ := Integer.sgn_compat_neg
    (-(sgn a)) ≃ _ := AA.subst₁ ‹sgn a ≃ sgn b›
    (-(sgn b)) ≃ _ := Rel.symm Integer.sgn_compat_neg
    sgn (-b)   ≃ _ := ‹sgn (-b) ≃ 1›
    1          ≃ _ := Rel.refl
  have : Positive (-a) := Integer.sgn_positive.mpr ‹sgn (-a) ≃ 1›
  have : Positive (-b) := Integer.sgn_positive.mpr ‹sgn (-b) ≃ 1›
  have : AP (Positive (-a)) := AP.mk ‹Positive (-a)›
  have : AP (Positive (-b)) := AP.mk ‹Positive (-b)›
  have neg_eqv {z : ℤ} : -(z : ℚ) ≃ ((-z : ℤ) : ℚ) :=
    Rational.eqv_symm Rational.neg_compat_from_integer
  have : x ≃ ((-a : ℤ) : ℚ) / ((-b : ℤ) : ℚ) := calc
    x                               ≃ _ := ‹x ≃ a / b›
    (a : ℚ) / b                     ≃ _ := Rel.symm Rational.div_neg_cancel
    (-(a : ℚ)) / (-(b : ℚ))         ≃ _ := Rational.div_substL neg_eqv
    ((-a : ℤ) : ℚ) / (-b : ℚ)       ≃ _ := Rational.div_substR neg_eqv
    ((-a : ℤ) : ℚ) / ((-b : ℤ) : ℚ) ≃ _ := Rational.eqv_refl
  exact AltPositive.mk 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
left✝ : Integer.Sqrt1 (sgn b)
right✝ : sgn a ≃ sgn b
this : sgn b ≃ 1 ∨ sgn b ≃ -1
⊢ AltPositive x
no goals