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

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

case mpr
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ AltNegative x → Negative x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Negative x → AltNegative x
Tactic:
case mp =>
  intro (_ : Negative x)
  show AltNegative x
  have (Exists.intro (y : ℚ) (And.intro (_ : Positive y) (_ : x ≃ -y))) :=
    negative_iff_neg_positive.mp ‹Negative x›
  have
    (AltPositive.intro
      (a : ℤ) (b : ℤ)
      (_ : AP (Positive a)) (_ : AP (Positive b)) y_eqv_a_over_b)
    := alt_positive.mp ‹Positive y›
  have : y ≃ a / b := y_eqv_a_over_b
  have : x ≃ (-a) / b := calc
    x                ≃ _ := ‹x ≃ -y›
    (-y)             ≃ _ := Rational.neg_subst ‹y ≃ a / b›
    (-((a : ℚ) / b)) ≃ _ := Rational.neg_scompatL_div
    (-a : ℚ) / b     ≃ _ := Rational.eqv_refl
  exact AltNegative.mk this
State after:
no goals

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ AltNegative x → Negative x
Tactic:
case mpr =>
  intro (_ : AltNegative x)
  show Negative x
  have
    (AltNegative.intro
      (a : ℤ) (b : ℤ)
      (_ : AP (Positive a)) (_ : AP (Positive b)) x_eqv_neg_a_over_b)
    := ‹AltNegative x›
  have : x ≃ (-a) / b := x_eqv_neg_a_over_b
  have : AltPositive ((a : ℚ) / b) := AltPositive.mk Rational.eqv_refl
  have : Positive ((a : ℚ) / b) := alt_positive.mpr this
  have : x ≃ -((a : ℚ) / b) := calc
    x                ≃ _ := ‹x ≃ (-a) / b›
    (-a : ℚ) / b     ≃ _ := Rational.eqv_symm Rational.neg_scompatL_div
    (-((a : ℚ) / b)) ≃ _ := Rational.eqv_refl
  have : ∃ (y : ℚ), Positive y ∧ x ≃ -y :=
    Exists.intro ((a : ℚ) / b) (And.intro ‹Positive ((a : ℚ) / b)› this)
  have : Negative x := negative_iff_neg_positive.mpr this
  exact this
State after:
no goals

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

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
⊢ AltNegative x
Tactic:
have (Exists.intro (y : ℚ) (And.intro (_ : Positive y) (_ : x ≃ -y))) :=
  negative_iff_neg_positive.mp ‹Negative x›
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
⊢ AltNegative x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
⊢ AltNegative x
Tactic:
have
  (AltPositive.intro
    (a : ℤ) (b : ℤ)
    (_ : AP (Positive a)) (_ : AP (Positive b)) y_eqv_a_over_b)
  := alt_positive.mp ‹Positive y›
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
y_eqv_a_over_b : y ≃ Rational.from_integer a / Rational.from_integer b
⊢ AltNegative x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
y_eqv_a_over_b : y ≃ Rational.from_integer a / Rational.from_integer b
⊢ AltNegative x
Tactic:
have : y ≃ a / b := y_eqv_a_over_b
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
y_eqv_a_over_b this : y ≃ Rational.from_integer a / Rational.from_integer b
⊢ AltNegative x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
y_eqv_a_over_b this : y ≃ Rational.from_integer a / Rational.from_integer b
⊢ AltNegative x
Tactic:
have : x ≃ (-a) / b := calc
  x                ≃ _ := ‹x ≃ -y›
  (-y)             ≃ _ := Rational.neg_subst ‹y ≃ a / b›
  (-((a : ℚ) / b)) ≃ _ := Rational.neg_scompatL_div
  (-a : ℚ) / b     ≃ _ := Rational.eqv_refl
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
y_eqv_a_over_b this✝ : y ≃ Rational.from_integer a / Rational.from_integer b
this : x ≃ -Rational.from_integer a / Rational.from_integer b
⊢ AltNegative x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
y_eqv_a_over_b this✝ : y ≃ Rational.from_integer a / Rational.from_integer b
this : x ≃ -Rational.from_integer a / Rational.from_integer b
⊢ AltNegative x
Tactic:
exact AltNegative.mk this
State after:
no goals

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

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

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

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

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this✝ : x ≃ -Rational.from_integer a / Rational.from_integer b
this : AltPositive (Rational.from_integer a / Rational.from_integer b)
⊢ Negative x
Tactic:
have : Positive ((a : ℚ) / b) := alt_positive.mpr this
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this✝¹ : x ≃ -Rational.from_integer a / Rational.from_integer b
this✝ : AltPositive (Rational.from_integer a / Rational.from_integer b)
this : Positive (Rational.from_integer a / Rational.from_integer b)
⊢ Negative x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this✝¹ : x ≃ -Rational.from_integer a / Rational.from_integer b
this✝ : AltPositive (Rational.from_integer a / Rational.from_integer b)
this : Positive (Rational.from_integer a / Rational.from_integer b)
⊢ Negative x
Tactic:
have : x ≃ -((a : ℚ) / b) := calc
  x                ≃ _ := ‹x ≃ (-a) / b›
  (-a : ℚ) / b     ≃ _ := Rational.eqv_symm Rational.neg_scompatL_div
  (-((a : ℚ) / b)) ≃ _ := Rational.eqv_refl
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this✝² : x ≃ -Rational.from_integer a / Rational.from_integer b
this✝¹ : AltPositive (Rational.from_integer a / Rational.from_integer b)
this✝ : Positive (Rational.from_integer a / Rational.from_integer b)
this : x ≃ -(Rational.from_integer a / Rational.from_integer b)
⊢ Negative x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this✝² : x ≃ -Rational.from_integer a / Rational.from_integer b
this✝¹ : AltPositive (Rational.from_integer a / Rational.from_integer b)
this✝ : Positive (Rational.from_integer a / Rational.from_integer b)
this : x ≃ -(Rational.from_integer a / Rational.from_integer b)
⊢ Negative x
Tactic:
have : ∃ (y : ℚ), Positive y ∧ x ≃ -y :=
  Exists.intro ((a : ℚ) / b) (And.intro ‹Positive ((a : ℚ) / b)› this)
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this✝³ : x ≃ -Rational.from_integer a / Rational.from_integer b
this✝² : AltPositive (Rational.from_integer a / Rational.from_integer b)
this✝¹ : Positive (Rational.from_integer a / Rational.from_integer b)
this✝ : x ≃ -(Rational.from_integer a / Rational.from_integer b)
this : ∃ y, Positive y ∧ x ≃ -y
⊢ Negative x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this✝³ : x ≃ -Rational.from_integer a / Rational.from_integer b
this✝² : AltPositive (Rational.from_integer a / Rational.from_integer b)
this✝¹ : Positive (Rational.from_integer a / Rational.from_integer b)
this✝ : x ≃ -(Rational.from_integer a / Rational.from_integer b)
this : ∃ y, Positive y ∧ x ≃ -y
⊢ Negative x
Tactic:
have : Negative x := negative_iff_neg_positive.mpr this
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this✝⁴ : x ≃ -Rational.from_integer a / Rational.from_integer b
this✝³ : AltPositive (Rational.from_integer a / Rational.from_integer b)
this✝² : Positive (Rational.from_integer a / Rational.from_integer b)
this✝¹ : x ≃ -(Rational.from_integer a / Rational.from_integer b)
this✝ : ∃ y, Positive y ∧ x ≃ -y
this : Negative x
⊢ Negative x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this✝⁴ : x ≃ -Rational.from_integer a / Rational.from_integer b
this✝³ : AltPositive (Rational.from_integer a / Rational.from_integer b)
this✝² : Positive (Rational.from_integer a / Rational.from_integer b)
this✝¹ : x ≃ -(Rational.from_integer a / Rational.from_integer b)
this✝ : ∃ y, Positive y ∧ x ≃ -y
this : Negative x
⊢ Negative x
Tactic:
exact this
State after:
no goals