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

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Negative x ↔ ∃ y, Positive y ∧ x ≃ -y
Tactic:
apply Iff.intro
State after:
case mp
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Negative x → ∃ y, Positive y ∧ x ≃ -y

case mpr
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ (∃ y, Positive y ∧ x ≃ -y) → Negative x

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Negative x → ∃ y, Positive y ∧ x ≃ -y
Tactic:
case mp =>
  intro (_ : Negative x)
  show ∃ (y : ℚ), Positive y ∧ x ≃ -y
  have : sgn x ≃ -1 := Rational.sgn_negative.mp ‹Negative x›
  have : sgn (-x) ≃ 1 := calc
    sgn (-x) ≃ _ := Rational.sgn_compat_neg
    (-sgn x) ≃ _ := AA.subst₁ ‹sgn x ≃ -1›
    (-(-1))  ≃ _ := Integer.neg_involutive
    1        ≃ _ := Rel.refl
  have : Positive (-x) := Rational.sgn_positive.mpr ‹sgn (-x) ≃ 1›
  have : x ≃ -(-x) := Rational.eqv_symm Rational.neg_involutive
  exact Exists.intro (-x) (And.intro ‹Positive (-x)› ‹x ≃ -(-x)›)
State after:
no goals

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ (∃ y, Positive y ∧ x ≃ -y) → Negative x
Tactic:
case mpr =>
  intro (Exists.intro (y : ℚ) (And.intro (_ : Positive y) (_ : x ≃ -y)))
  show Negative x
  have : sgn y ≃ 1 := Rational.sgn_positive.mp ‹Positive y›
  have : sgn x ≃ -1 := calc
    sgn x      ≃ _ := Rational.sgn_subst ‹x ≃ -y›
    sgn (-y)   ≃ _ := Rational.sgn_compat_neg
    (-(sgn y)) ≃ _ := AA.subst₁ ‹sgn y ≃ 1›
    (-1)       ≃ _ := Rel.refl
  have : Negative x := Rational.sgn_negative.mpr this
  exact this
State after:
no goals

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Negative x → ∃ y, Positive y ∧ x ≃ -y
Tactic:
intro (_ : Negative x)
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
⊢ ∃ y, Positive y ∧ x ≃ -y

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
⊢ ∃ y, Positive y ∧ x ≃ -y
Tactic:
have : sgn x ≃ -1 := Rational.sgn_negative.mp ‹Negative x›
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
this : sgn x ≃ -1
⊢ ∃ y, Positive y ∧ x ≃ -y

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
this : sgn x ≃ -1
⊢ ∃ y, Positive y ∧ x ≃ -y
Tactic:
have : sgn (-x) ≃ 1 := calc
  sgn (-x) ≃ _ := Rational.sgn_compat_neg
  (-sgn x) ≃ _ := AA.subst₁ ‹sgn x ≃ -1›
  (-(-1))  ≃ _ := Integer.neg_involutive
  1        ≃ _ := Rel.refl
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
this✝ : sgn x ≃ -1
this : sgn (-x) ≃ 1
⊢ ∃ y, Positive y ∧ x ≃ -y

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
this✝ : sgn x ≃ -1
this : sgn (-x) ≃ 1
⊢ ∃ y, Positive y ∧ x ≃ -y
Tactic:
have : Positive (-x) := Rational.sgn_positive.mpr ‹sgn (-x) ≃ 1›
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
this✝¹ : sgn x ≃ -1
this✝ : sgn (-x) ≃ 1
this : Positive (-x)
⊢ ∃ y, Positive y ∧ x ≃ -y

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
this✝¹ : sgn x ≃ -1
this✝ : sgn (-x) ≃ 1
this : Positive (-x)
⊢ ∃ y, Positive y ∧ x ≃ -y
Tactic:
have : x ≃ -(-x) := Rational.eqv_symm Rational.neg_involutive
State after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
this✝² : sgn x ≃ -1
this✝¹ : sgn (-x) ≃ 1
this✝ : Positive (-x)
this : x ≃ - -x
⊢ ∃ y, Positive y ∧ x ≃ -y

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
this✝² : sgn x ≃ -1
this✝¹ : sgn (-x) ≃ 1
this✝ : Positive (-x)
this : x ≃ - -x
⊢ ∃ y, Positive y ∧ x ≃ -y
Tactic:
exact Exists.intro (-x) (And.intro ‹Positive (-x)› ‹x ≃ -(-x)›)
State after:
no goals

State before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ (∃ y, Positive y ∧ x ≃ -y) → Negative x
Tactic:
intro (Exists.intro (y : ℚ) (And.intro (_ : Positive y) (_ : x ≃ -y)))
State after:
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
⊢ Negative x

State before:
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
⊢ Negative x
Tactic:
have : sgn y ≃ 1 := Rational.sgn_positive.mp ‹Positive y›
State after:
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
this : sgn y ≃ 1
⊢ Negative x

State before:
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
this : sgn y ≃ 1
⊢ Negative x
Tactic:
have : sgn x ≃ -1 := calc
  sgn x      ≃ _ := Rational.sgn_subst ‹x ≃ -y›
  sgn (-y)   ≃ _ := Rational.sgn_compat_neg
  (-(sgn y)) ≃ _ := AA.subst₁ ‹sgn y ≃ 1›
  (-1)       ≃ _ := Rel.refl
State after:
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
this✝ : sgn y ≃ 1
this : sgn x ≃ -1
⊢ Negative x

State before:
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
this✝ : sgn y ≃ 1
this : sgn x ≃ -1
⊢ Negative x
Tactic:
have : Negative x := Rational.sgn_negative.mpr this
State after:
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
this✝¹ : sgn y ≃ 1
this✝ : sgn x ≃ -1
this : Negative x
⊢ Negative x

State before:
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
this✝¹ : sgn y ≃ 1
this✝ : sgn x ≃ -1
this : Negative x
⊢ Negative x
Tactic:
exact this
State after:
no goals