case mp =>
  intro (_ : Positive x)
  show AltPositive x
  have (Rational.AsRatio.intro a b (_ : Integer.Nonzero b) x_eqv) :=
    Rational.as_ratio x
  have : x ≃ a / b := x_eqv
  have : sgn a * sgn b ≃ 1 := calc
    sgn a * sgn b     ≃ _ := Rel.symm Rational.sgn_div_integers
    sgn ((a : ℚ) / b) ≃ _ := Rational.sgn_subst (Rel.symm ‹x ≃ a / b›)
    sgn x             ≃ _ := Rational.sgn_positive.mp ‹Positive x›
    1                 ≃ _ := Rel.refl
  have (And.intro (_ : Integer.Sqrt1 (sgn b)) (_ : sgn a ≃ sgn b)) :=
    Integer.mul_sqrt1_eqv.mp this
  have : sgn b ≃ 1 ∨ sgn b ≃ -1 :=
    Integer.sqrt1_cases.mp ‹Integer.Sqrt1 (sgn b)›
  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 : ℚ
⊢ Positive x → AltPositive x
no goals