Theorem: AnalysisI.Ch4.Sec1.neg_iff_ex (Lean4Analysis/Ch4/Ch4Sec1Integers.lean)

State before:
x : ℤ
⊢ Negative x ↔ ∃ n, Positive n ∧ x ≃ -coe n
Tactic:
apply Iff.intro
State after:
case mp
x : ℤ
⊢ Negative x → ∃ n, Positive n ∧ x ≃ -coe n

case mpr
x : ℤ
⊢ (∃ n, Positive n ∧ x ≃ -coe n) → Negative x

State before:
x : ℤ
⊢ Negative x → ∃ n, Positive n ∧ x ≃ -coe n
Tactic:
case mp =>
  intro (_ : Negative x)
  show ∃ (n : ℕ), Positive n ∧ x ≃ -(coe n)
  have (Integer.NonzeroWithSign.intro
        (n : ℕ) (_ : Positive n) (_ : x ≃ -1 * coe n)) :=
    Impl.sign_props.negative_iff_sign_neg1.mp ‹Negative x›
  exists n
  apply And.intro ‹Positive n›
  show x ≃ -(coe n)
  exact Rel.trans ‹x ≃ -1 * coe n› Integer.mul_neg_one
State after:
no goals

State before:
x : ℤ
⊢ (∃ n, Positive n ∧ x ≃ -coe n) → Negative x
Tactic:
case mpr =>
  intro
    (Exists.intro (n : ℕ) (And.intro (_ : Positive n) (_ : x ≃ -(coe n))))
  show Negative x
  apply Impl.sign_props.negative_iff_sign_neg1.mpr
  show Integer.NonzeroWithSign x (-1)
  apply Integer.NonzeroWithSign.intro n ‹Positive n›
  show x ≃ -1 * coe n
  exact Rel.trans ‹x ≃ -(coe n)› (Rel.symm Integer.mul_neg_one)
State after:
no goals

State before:
x : ℤ
⊢ Negative x → ∃ n, Positive n ∧ x ≃ -coe n
Tactic:
intro (_ : Negative x)
State after:
x : ℤ
x✝ : Negative x
⊢ ∃ n, Positive n ∧ x ≃ -coe n

State before:
x : ℤ
x✝ : Negative x
⊢ ∃ n, Positive n ∧ x ≃ -coe n
Tactic:
have (Integer.NonzeroWithSign.intro
      (n : ℕ) (_ : Positive n) (_ : x ≃ -1 * coe n)) :=
  Impl.sign_props.negative_iff_sign_neg1.mp ‹Negative x›
State after:
x : ℤ
x✝ : Negative x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ -1 * coe n
⊢ ∃ n, Positive n ∧ x ≃ -coe n

State before:
x : ℤ
x✝ : Negative x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ -1 * coe n
⊢ ∃ n, Positive n ∧ x ≃ -coe n
Tactic:
exists n
State after:
x : ℤ
x✝ : Negative x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ -1 * coe n
⊢ Positive n ∧ x ≃ -coe n

State before:
x : ℤ
x✝ : Negative x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ -1 * coe n
⊢ Positive n ∧ x ≃ -coe n
Tactic:
apply And.intro ‹Positive n›
State after:
x : ℤ
x✝ : Negative x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ -1 * coe n
⊢ x ≃ -coe n

State before:
x : ℤ
x✝ : Negative x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ -1 * coe n
⊢ x ≃ -coe n
Tactic:
exact Rel.trans ‹x ≃ -1 * coe n› Integer.mul_neg_one
State after:
no goals

State before:
x : ℤ
⊢ (∃ n, Positive n ∧ x ≃ -coe n) → Negative x
Tactic:
intro
  (Exists.intro (n : ℕ) (And.intro (_ : Positive n) (_ : x ≃ -(coe n))))
State after:
x : ℤ
n : ℕ
left✝ : Positive n
right✝ : x ≃ -coe n
⊢ Negative x

State before:
x : ℤ
n : ℕ
left✝ : Positive n
right✝ : x ≃ -coe n
⊢ Negative x
Tactic:
apply Impl.sign_props.negative_iff_sign_neg1.mpr
State after:
x : ℤ
n : ℕ
left✝ : Positive n
right✝ : x ≃ -coe n
⊢ Integer.NonzeroWithSign x (-1)

State before:
x : ℤ
n : ℕ
left✝ : Positive n
right✝ : x ≃ -coe n
⊢ Integer.NonzeroWithSign x (-1)
Tactic:
apply Integer.NonzeroWithSign.intro n ‹Positive n›
State after:
x : ℤ
n : ℕ
left✝ : Positive n
right✝ : x ≃ -coe n
⊢ x ≃ -1 * coe n

State before:
x : ℤ
n : ℕ
left✝ : Positive n
right✝ : x ≃ -coe n
⊢ x ≃ -1 * coe n
Tactic:
exact Rel.trans ‹x ≃ -(coe n)› (Rel.symm Integer.mul_neg_one)
State after:
no goals