Theorem: Romania1998P12.int_dichotomy (Compfiles/Romania1998P12.lean)

State before:
z : ℤ
⊢ ∃ n, ↑n = z ∨ -↑n = z
Tactic:
cases' z with z z
State after:
case ofNat
z : ℕ
⊢ ∃ n, ↑n = Int.ofNat z ∨ -↑n = Int.ofNat z

case negSucc
z : ℕ
⊢ ∃ n, ↑n = Int.negSucc z ∨ -↑n = Int.negSucc z

State before:
case ofNat
z : ℕ
⊢ ∃ n, ↑n = Int.ofNat z ∨ -↑n = Int.ofNat z
Tactic:
use z
State after:
case h
z : ℕ
⊢ ↑z = Int.ofNat z ∨ -↑z = Int.ofNat z

State before:
case h
z : ℕ
⊢ ↑z = Int.ofNat z ∨ -↑z = Int.ofNat z
Tactic:
left
State after:
case h.h
z : ℕ
⊢ ↑z = Int.ofNat z

State before:
case h.h
z : ℕ
⊢ ↑z = Int.ofNat z
Tactic:
simp only [Int.ofNat_eq_coe]
State after:
no goals

State before:
case negSucc
z : ℕ
⊢ ∃ n, ↑n = Int.negSucc z ∨ -↑n = Int.negSucc z
Tactic:
use z + 1
State after:
case h
z : ℕ
⊢ ↑(z + 1) = Int.negSucc z ∨ -↑(z + 1) = Int.negSucc z

State before:
case h
z : ℕ
⊢ ↑(z + 1) = Int.negSucc z ∨ -↑(z + 1) = Int.negSucc z
Tactic:
right
State after:
case h.h
z : ℕ
⊢ -↑(z + 1) = Int.negSucc z

State before:
case h.h
z : ℕ
⊢ -↑(z + 1) = Int.negSucc z
Tactic:
rfl
State after:
no goals