case mpr =>
  intro (_ : AltPositive x)
  show Positive x
  have (AltPositive.intro (a : ℤ) (b : ℤ) a_pos b_pos x_eqv) :=
    ‹AltPositive x›
  have : AP (Positive a) := a_pos
  have : sgn a ≃ 1 := Integer.sgn_positive.mp this.ev
  have : AP (Positive b) := b_pos
  have : sgn b ≃ 1 := Integer.sgn_positive.mp this.ev
  have : x ≃ a / b := x_eqv
  have : sgn a ≃ sgn b := Rel.trans ‹sgn a ≃ 1› (Rel.symm ‹sgn b ≃ 1›)
  have : Integer.Nonzero b := Integer.nonzero_from_positive_inst
  have : Integer.Sqrt1 (sgn b) := Integer.sgn_nonzero.mp this
  have : sgn a * sgn b ≃ 1 :=
    Integer.mul_sqrt1_eqv.mpr (And.intro this ‹sgn a ≃ sgn b›)
  have : sgn x ≃ 1 := calc
    sgn x                   ≃ _ := Rational.sgn_subst ‹x ≃ a / b›
    sgn ((a : ℚ) / (b : ℚ)) ≃ _ := Rational.sgn_div_integers
    sgn a * sgn b           ≃ _ := ‹sgn a * sgn b ≃ 1›
    1                       ≃ _ := Rel.refl
  have : Positive x := Rational.sgn_positive.mpr this
  exact this
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ AltPositive x → Positive x
no goals