Theorem: AnalysisI.Ch4.Sec2.alt_positive (Lean4Analysis/Ch4/Ch4Sec2Rationals.lean)

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Positive x ↔ AltPositive x
Tactic:
apply Iff.intro
State after:
case mp
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Positive x → AltPositive x

case mpr
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ AltPositive x → Positive x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Positive x → AltPositive x
Tactic:
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
State after:
no goals

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ AltPositive x → Positive x
Tactic:
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
State after:
no goals

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Positive x → AltPositive x
Tactic:
intro (_ : Positive x)
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
⊢ AltPositive x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
⊢ AltPositive x
Tactic:
have (Rational.AsRatio.intro a b (_ : Integer.Nonzero b) x_eqv) :=
  Rational.as_ratio x
State after:
ℚ : 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
⊢ AltPositive x

State before:
ℚ : 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
⊢ AltPositive x
Tactic:
have : x ≃ a / b := x_eqv
State after:
ℚ : 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
⊢ AltPositive x

State before:
ℚ : 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
⊢ AltPositive x
Tactic:
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
State after:
ℚ : 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

State before:
ℚ : 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
Tactic:
have (And.intro (_ : Integer.Sqrt1 (sgn b)) (_ : sgn a ≃ sgn b)) :=
  Integer.mul_sqrt1_eqv.mp this
State after:
ℚ : 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

State before:
ℚ : 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
Tactic:
have : sgn b ≃ 1 ∨ sgn b ≃ -1 :=
  Integer.sqrt1_cases.mp ‹Integer.Sqrt1 (sgn b)›
State after:
ℚ : 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

State before:
ℚ : 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
Tactic:
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
State after:
no goals

State before:
ℚ : 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
h✝ : sgn b ≃ 1
⊢ AltPositive x
Tactic:
have : sgn a ≃ 1 := Rel.trans ‹sgn a ≃ sgn b› ‹sgn b ≃ 1›
State after:
ℚ : 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
h✝ : sgn b ≃ 1
this : sgn a ≃ 1
⊢ AltPositive x

State before:
ℚ : 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
h✝ : sgn b ≃ 1
this : sgn a ≃ 1
⊢ AltPositive x
Tactic:
have : AP (Positive a) := AP.mk (Integer.sgn_positive.mpr ‹sgn a ≃ 1›)
State after:
ℚ : 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
h✝ : sgn b ≃ 1
this✝ : sgn a ≃ 1
this : AP (Positive a)
⊢ AltPositive x

State before:
ℚ : 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
h✝ : sgn b ≃ 1
this✝ : sgn a ≃ 1
this : AP (Positive a)
⊢ AltPositive x
Tactic:
have : AP (Positive b) := AP.mk (Integer.sgn_positive.mpr ‹sgn b ≃ 1›)
State after:
ℚ : 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
h✝ : sgn b ≃ 1
this✝¹ : sgn a ≃ 1
this✝ : AP (Positive a)
this : AP (Positive b)
⊢ AltPositive x

State before:
ℚ : 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
h✝ : sgn b ≃ 1
this✝¹ : sgn a ≃ 1
this✝ : AP (Positive a)
this : AP (Positive b)
⊢ AltPositive x
Tactic:
exact AltPositive.mk ‹x ≃ a / b›
State after:
no goals

State before:
ℚ : 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
h✝ : sgn b ≃ -1
⊢ AltPositive x
Tactic:
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
State after:
ℚ : 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
h✝ : sgn b ≃ -1
this : sgn (-b) ≃ 1
⊢ AltPositive x

State before:
ℚ : 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
h✝ : sgn b ≃ -1
this : sgn (-b) ≃ 1
⊢ AltPositive x
Tactic:
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
State after:
ℚ : 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
h✝ : sgn b ≃ -1
this✝ : sgn (-b) ≃ 1
this : sgn (-a) ≃ 1
⊢ AltPositive x

State before:
ℚ : 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
h✝ : sgn b ≃ -1
this✝ : sgn (-b) ≃ 1
this : sgn (-a) ≃ 1
⊢ AltPositive x
Tactic:
have : Positive (-a) := Integer.sgn_positive.mpr ‹sgn (-a) ≃ 1›
State after:
ℚ : 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
h✝ : sgn b ≃ -1
this✝¹ : sgn (-b) ≃ 1
this✝ : sgn (-a) ≃ 1
this : Positive (-a)
⊢ AltPositive x

State before:
ℚ : 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
h✝ : sgn b ≃ -1
this✝¹ : sgn (-b) ≃ 1
this✝ : sgn (-a) ≃ 1
this : Positive (-a)
⊢ AltPositive x
Tactic:
have : Positive (-b) := Integer.sgn_positive.mpr ‹sgn (-b) ≃ 1›
State after:
ℚ : 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
h✝ : sgn b ≃ -1
this✝² : sgn (-b) ≃ 1
this✝¹ : sgn (-a) ≃ 1
this✝ : Positive (-a)
this : Positive (-b)
⊢ AltPositive x

State before:
ℚ : 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
h✝ : sgn b ≃ -1
this✝² : sgn (-b) ≃ 1
this✝¹ : sgn (-a) ≃ 1
this✝ : Positive (-a)
this : Positive (-b)
⊢ AltPositive x
Tactic:
have : AP (Positive (-a)) := AP.mk ‹Positive (-a)›
State after:
ℚ : 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
h✝ : sgn b ≃ -1
this✝³ : sgn (-b) ≃ 1
this✝² : sgn (-a) ≃ 1
this✝¹ : Positive (-a)
this✝ : Positive (-b)
this : AP (Positive (-a))
⊢ AltPositive x

State before:
ℚ : 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
h✝ : sgn b ≃ -1
this✝³ : sgn (-b) ≃ 1
this✝² : sgn (-a) ≃ 1
this✝¹ : Positive (-a)
this✝ : Positive (-b)
this : AP (Positive (-a))
⊢ AltPositive x
Tactic:
have : AP (Positive (-b)) := AP.mk ‹Positive (-b)›
State after:
ℚ : 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
h✝ : sgn b ≃ -1
this✝⁴ : sgn (-b) ≃ 1
this✝³ : sgn (-a) ≃ 1
this✝² : Positive (-a)
this✝¹ : Positive (-b)
this✝ : AP (Positive (-a))
this : AP (Positive (-b))
⊢ AltPositive x

State before:
ℚ : 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
h✝ : sgn b ≃ -1
this✝⁴ : sgn (-b) ≃ 1
this✝³ : sgn (-a) ≃ 1
this✝² : Positive (-a)
this✝¹ : Positive (-b)
this✝ : AP (Positive (-a))
this : AP (Positive (-b))
⊢ AltPositive x
Tactic:
have neg_eqv {z : ℤ} : -(z : ℚ) ≃ ((-z : ℤ) : ℚ) :=
  Rational.eqv_symm Rational.neg_compat_from_integer
State after:
ℚ : 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
h✝ : sgn b ≃ -1
this✝⁴ : sgn (-b) ≃ 1
this✝³ : sgn (-a) ≃ 1
this✝² : Positive (-a)
this✝¹ : Positive (-b)
this✝ : AP (Positive (-a))
this : AP (Positive (-b))
neg_eqv : ∀ {z : ℤ}, -Rational.from_integer z ≃ Rational.from_integer (-z)
⊢ AltPositive x

State before:
ℚ : 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
h✝ : sgn b ≃ -1
this✝⁴ : sgn (-b) ≃ 1
this✝³ : sgn (-a) ≃ 1
this✝² : Positive (-a)
this✝¹ : Positive (-b)
this✝ : AP (Positive (-a))
this : AP (Positive (-b))
neg_eqv : ∀ {z : ℤ}, -Rational.from_integer z ≃ Rational.from_integer (-z)
⊢ AltPositive x
Tactic:
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
State after:
ℚ : 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
h✝ : sgn b ≃ -1
this✝⁵ : sgn (-b) ≃ 1
this✝⁴ : sgn (-a) ≃ 1
this✝³ : Positive (-a)
this✝² : Positive (-b)
this✝¹ : AP (Positive (-a))
this✝ : AP (Positive (-b))
neg_eqv : ∀ {z : ℤ}, -Rational.from_integer z ≃ Rational.from_integer (-z)
this : x ≃ Rational.from_integer (-a) / Rational.from_integer (-b)
⊢ AltPositive x

State before:
ℚ : 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
h✝ : sgn b ≃ -1
this✝⁵ : sgn (-b) ≃ 1
this✝⁴ : sgn (-a) ≃ 1
this✝³ : Positive (-a)
this✝² : Positive (-b)
this✝¹ : AP (Positive (-a))
this✝ : AP (Positive (-b))
neg_eqv : ∀ {z : ℤ}, -Rational.from_integer z ≃ Rational.from_integer (-z)
this : x ≃ Rational.from_integer (-a) / Rational.from_integer (-b)
⊢ AltPositive x
Tactic:
exact AltPositive.mk this
State after:
no goals

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ AltPositive x → Positive x
Tactic:
intro (_ : AltPositive x)
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
⊢ Positive x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
⊢ Positive x
Tactic:
have (AltPositive.intro (a : ℤ) (b : ℤ) a_pos b_pos x_eqv) :=
  ‹AltPositive x›
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
⊢ Positive x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
⊢ Positive x
Tactic:
have : AP (Positive a) := a_pos
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this : AP (Positive a)
⊢ Positive x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this : AP (Positive a)
⊢ Positive x
Tactic:
have : sgn a ≃ 1 := Integer.sgn_positive.mp this.ev
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝ : AP (Positive a)
this : sgn a ≃ 1
⊢ Positive x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝ : AP (Positive a)
this : sgn a ≃ 1
⊢ Positive x
Tactic:
have : AP (Positive b) := b_pos
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝¹ : AP (Positive a)
this✝ : sgn a ≃ 1
this : AP (Positive b)
⊢ Positive x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝¹ : AP (Positive a)
this✝ : sgn a ≃ 1
this : AP (Positive b)
⊢ Positive x
Tactic:
have : sgn b ≃ 1 := Integer.sgn_positive.mp this.ev
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝² : AP (Positive a)
this✝¹ : sgn a ≃ 1
this✝ : AP (Positive b)
this : sgn b ≃ 1
⊢ Positive x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝² : AP (Positive a)
this✝¹ : sgn a ≃ 1
this✝ : AP (Positive b)
this : sgn b ≃ 1
⊢ Positive x
Tactic:
have : x ≃ a / b := x_eqv
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝³ : AP (Positive a)
this✝² : sgn a ≃ 1
this✝¹ : AP (Positive b)
this✝ : sgn b ≃ 1
this : x ≃ Rational.from_integer a / Rational.from_integer b
⊢ Positive x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝³ : AP (Positive a)
this✝² : sgn a ≃ 1
this✝¹ : AP (Positive b)
this✝ : sgn b ≃ 1
this : x ≃ Rational.from_integer a / Rational.from_integer b
⊢ Positive x
Tactic:
have : sgn a ≃ sgn b := Rel.trans ‹sgn a ≃ 1› (Rel.symm ‹sgn b ≃ 1›)
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁴ : AP (Positive a)
this✝³ : sgn a ≃ 1
this✝² : AP (Positive b)
this✝¹ : sgn b ≃ 1
this✝ : x ≃ Rational.from_integer a / Rational.from_integer b
this : sgn a ≃ sgn b
⊢ Positive x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁴ : AP (Positive a)
this✝³ : sgn a ≃ 1
this✝² : AP (Positive b)
this✝¹ : sgn b ≃ 1
this✝ : x ≃ Rational.from_integer a / Rational.from_integer b
this : sgn a ≃ sgn b
⊢ Positive x
Tactic:
have : Integer.Nonzero b := Integer.nonzero_from_positive_inst
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁵ : AP (Positive a)
this✝⁴ : sgn a ≃ 1
this✝³ : AP (Positive b)
this✝² : sgn b ≃ 1
this✝¹ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝ : sgn a ≃ sgn b
this : Nonzero b
⊢ Positive x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁵ : AP (Positive a)
this✝⁴ : sgn a ≃ 1
this✝³ : AP (Positive b)
this✝² : sgn b ≃ 1
this✝¹ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝ : sgn a ≃ sgn b
this : Nonzero b
⊢ Positive x
Tactic:
have : Integer.Sqrt1 (sgn b) := Integer.sgn_nonzero.mp this
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁶ : AP (Positive a)
this✝⁵ : sgn a ≃ 1
this✝⁴ : AP (Positive b)
this✝³ : sgn b ≃ 1
this✝² : x ≃ Rational.from_integer a / Rational.from_integer b
this✝¹ : sgn a ≃ sgn b
this✝ : Nonzero b
this : Integer.Sqrt1 (sgn b)
⊢ Positive x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁶ : AP (Positive a)
this✝⁵ : sgn a ≃ 1
this✝⁴ : AP (Positive b)
this✝³ : sgn b ≃ 1
this✝² : x ≃ Rational.from_integer a / Rational.from_integer b
this✝¹ : sgn a ≃ sgn b
this✝ : Nonzero b
this : Integer.Sqrt1 (sgn b)
⊢ Positive x
Tactic:
have : sgn a * sgn b ≃ 1 :=
  Integer.mul_sqrt1_eqv.mpr (And.intro this ‹sgn a ≃ sgn b›)
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁷ : AP (Positive a)
this✝⁶ : sgn a ≃ 1
this✝⁵ : AP (Positive b)
this✝⁴ : sgn b ≃ 1
this✝³ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝² : sgn a ≃ sgn b
this✝¹ : Nonzero b
this✝ : Integer.Sqrt1 (sgn b)
this : sgn a * sgn b ≃ 1
⊢ Positive x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁷ : AP (Positive a)
this✝⁶ : sgn a ≃ 1
this✝⁵ : AP (Positive b)
this✝⁴ : sgn b ≃ 1
this✝³ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝² : sgn a ≃ sgn b
this✝¹ : Nonzero b
this✝ : Integer.Sqrt1 (sgn b)
this : sgn a * sgn b ≃ 1
⊢ Positive x
Tactic:
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
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁸ : AP (Positive a)
this✝⁷ : sgn a ≃ 1
this✝⁶ : AP (Positive b)
this✝⁵ : sgn b ≃ 1
this✝⁴ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝³ : sgn a ≃ sgn b
this✝² : Nonzero b
this✝¹ : Integer.Sqrt1 (sgn b)
this✝ : sgn a * sgn b ≃ 1
this : sgn x ≃ 1
⊢ Positive x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁸ : AP (Positive a)
this✝⁷ : sgn a ≃ 1
this✝⁶ : AP (Positive b)
this✝⁵ : sgn b ≃ 1
this✝⁴ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝³ : sgn a ≃ sgn b
this✝² : Nonzero b
this✝¹ : Integer.Sqrt1 (sgn b)
this✝ : sgn a * sgn b ≃ 1
this : sgn x ≃ 1
⊢ Positive x
Tactic:
have : Positive x := Rational.sgn_positive.mpr this
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁹ : AP (Positive a)
this✝⁸ : sgn a ≃ 1
this✝⁷ : AP (Positive b)
this✝⁶ : sgn b ≃ 1
this✝⁵ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁴ : sgn a ≃ sgn b
this✝³ : Nonzero b
this✝² : Integer.Sqrt1 (sgn b)
this✝¹ : sgn a * sgn b ≃ 1
this✝ : sgn x ≃ 1
this : Positive x
⊢ Positive x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁹ : AP (Positive a)
this✝⁸ : sgn a ≃ 1
this✝⁷ : AP (Positive b)
this✝⁶ : sgn b ≃ 1
this✝⁵ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁴ : sgn a ≃ sgn b
this✝³ : Nonzero b
this✝² : Integer.Sqrt1 (sgn b)
this✝¹ : sgn a * sgn b ≃ 1
this✝ : sgn x ≃ 1
this : Positive x
⊢ Positive x
Tactic:
exact this
State after:
no goals