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

State before:
x : ℤ
⊢ Positive x ↔ ∃ n, Positive n ∧ x ≃ coe n
Tactic:
have mul_ident := Impl.multiplication.mul_identity (ℕ := ℕ)
State after:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
⊢ Positive x ↔ ∃ n, Positive n ∧ x ≃ coe n

State before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
⊢ Positive x ↔ ∃ n, Positive n ∧ x ≃ coe n
Tactic:
apply Iff.intro
State after:
case mp
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
⊢ Positive x → ∃ n, Positive n ∧ x ≃ coe n

case mpr
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
⊢ (∃ n, Positive n ∧ x ≃ coe n) → Positive x

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

State before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
⊢ (∃ n, Positive n ∧ x ≃ coe n) → Positive x
Tactic:
case mpr =>
  intro (Exists.intro (n : ℕ) (And.intro (_ : Positive n) (_ : x ≃ coe n)))
  show Positive x
  apply Impl.sign_props.positive_iff_sign_pos1.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 AA.identL)
State after:
no goals

State before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
⊢ Positive x → ∃ n, Positive n ∧ x ≃ coe n
Tactic:
intro (_ : Positive x)
State after:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
x✝ : Positive x
⊢ ∃ n, Positive n ∧ x ≃ coe n

State before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
x✝ : Positive x
⊢ ∃ n, Positive n ∧ x ≃ coe n
Tactic:
have (Integer.NonzeroWithSign.intro
      (n : ℕ) (_ : Positive n) (_ : x ≃ 1 * coe n)) :=
  Impl.sign_props.positive_iff_sign_pos1.mp ‹Positive x›
State after:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
x✝ : Positive x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ 1 * coe n
⊢ ∃ n, Positive n ∧ x ≃ coe n

State before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
x✝ : Positive x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ 1 * coe n
⊢ ∃ n, Positive n ∧ x ≃ coe n
Tactic:
exists n
State after:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
x✝ : Positive x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ 1 * coe n
⊢ Positive n ∧ x ≃ coe n

State before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
x✝ : Positive x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ 1 * coe n
⊢ Positive n ∧ x ≃ coe n
Tactic:
apply And.intro ‹Positive n›
State after:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
x✝ : Positive x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ 1 * coe n
⊢ x ≃ coe n

State before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
x✝ : Positive x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ 1 * coe n
⊢ x ≃ coe n
Tactic:
exact Rel.trans ‹x ≃ 1 * coe n› AA.identL
State after:
no goals

State before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
⊢ (∃ n, Positive n ∧ x ≃ coe n) → Positive x
Tactic:
intro (Exists.intro (n : ℕ) (And.intro (_ : Positive n) (_ : x ≃ coe n)))
State after:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
n : ℕ
left✝ : Positive n
right✝ : x ≃ coe n
⊢ Positive x

State before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
n : ℕ
left✝ : Positive n
right✝ : x ≃ coe n
⊢ Positive x
Tactic:
apply Impl.sign_props.positive_iff_sign_pos1.mpr
State after:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
n : ℕ
left✝ : Positive n
right✝ : x ≃ coe n
⊢ Integer.NonzeroWithSign x 1

State before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
n : ℕ
left✝ : Positive n
right✝ : x ≃ coe n
⊢ Integer.NonzeroWithSign x 1
Tactic:
apply Integer.NonzeroWithSign.intro n ‹Positive n›
State after:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
n : ℕ
left✝ : Positive n
right✝ : x ≃ coe n
⊢ x ≃ 1 * coe n

State before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
n : ℕ
left✝ : Positive n
right✝ : x ≃ coe n
⊢ x ≃ 1 * coe n
Tactic:
exact Rel.trans ‹x ≃ coe n› (Rel.symm AA.identL)
State after:
no goals