Theorem: push_pop (Ray/Misc/Finset.lean)

State before:
N : Finset ℕ
⊢ push (pop N) = insert 0 N
Tactic:
rw [push, pop]
State after:
N : Finset ℕ
⊢ insert 0 (Finset.image (fun n => n + 1) (Finset.image (fun n => n - 1) (N.erase 0))) = insert 0 N

State before:
N : Finset ℕ
⊢ insert 0 (Finset.image (fun n => n + 1) (Finset.image (fun n => n - 1) (N.erase 0))) = insert 0 N
Tactic:
apply Finset.ext
State after:
case a
N : Finset ℕ
⊢ ∀ (a : ℕ), a ∈ insert 0 (Finset.image (fun n => n + 1) (Finset.image (fun n => n - 1) (N.erase 0))) ↔ a ∈ insert 0 N

State before:
case a
N : Finset ℕ
⊢ ∀ (a : ℕ), a ∈ insert 0 (Finset.image (fun n => n + 1) (Finset.image (fun n => n - 1) (N.erase 0))) ↔ a ∈ insert 0 N
Tactic:
simp
State after:
case a
N : Finset ℕ
⊢ ∀ (a : ℕ), (a = 0 ∨ ∃ a_1, (¬a_1 = 0 ∧ a_1 ∈ N) ∧ a_1 - 1 + 1 = a) ↔ a = 0 ∨ a ∈ N

State before:
case a
N : Finset ℕ
⊢ ∀ (a : ℕ), (a = 0 ∨ ∃ a_1, (¬a_1 = 0 ∧ a_1 ∈ N) ∧ a_1 - 1 + 1 = a) ↔ a = 0 ∨ a ∈ N
Tactic:
intro n
State after:
case a
N : Finset ℕ
n : ℕ
⊢ (n = 0 ∨ ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n) ↔ n = 0 ∨ n ∈ N

State before:
case a
N : Finset ℕ
n : ℕ
⊢ (n = 0 ∨ ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n) ↔ n = 0 ∨ n ∈ N
Tactic:
by_cases n0 : n = 0
State after:
case pos
N : Finset ℕ
n : ℕ
n0 : n = 0
⊢ (n = 0 ∨ ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n) ↔ n = 0 ∨ n ∈ N

case neg
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
⊢ (n = 0 ∨ ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n) ↔ n = 0 ∨ n ∈ N

State before:
case neg
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
⊢ (n = 0 ∨ ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n) ↔ n = 0 ∨ n ∈ N
Tactic:
simp_rw [or_iff_right n0]
State after:
case neg
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
⊢ (∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n) ↔ n ∈ N

State before:
case neg
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
⊢ (∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n) ↔ n ∈ N
Tactic:
constructor
State after:
case neg.mp
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
⊢ (∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n) → n ∈ N

case neg.mpr
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
⊢ n ∈ N → ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n

State before:
case pos
N : Finset ℕ
n : ℕ
n0 : n = 0
⊢ (n = 0 ∨ ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n) ↔ n = 0 ∨ n ∈ N
Tactic:
rw [n0]
State after:
case pos
N : Finset ℕ
n : ℕ
n0 : n = 0
⊢ (0 = 0 ∨ ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = 0) ↔ 0 = 0 ∨ 0 ∈ N

State before:
case pos
N : Finset ℕ
n : ℕ
n0 : n = 0
⊢ (0 = 0 ∨ ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = 0) ↔ 0 = 0 ∨ 0 ∈ N
Tactic:
simp
State after:
no goals

State before:
case neg.mp
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
⊢ (∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n) → n ∈ N
Tactic:
intro h
State after:
case neg.mp
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
h : ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n
⊢ n ∈ N

State before:
case neg.mp
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
h : ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n
⊢ n ∈ N
Tactic:
rcases h with ⟨x, ⟨x0, xN⟩, xn⟩
State after:
case neg.mp.intro.intro.intro
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
x : ℕ
xn : x - 1 + 1 = n
x0 : ¬x = 0
xN : x ∈ N
⊢ n ∈ N

State before:
case neg.mp.intro.intro.intro
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
x : ℕ
xn : x - 1 + 1 = n
x0 : ¬x = 0
xN : x ∈ N
⊢ n ∈ N
Tactic:
rw [Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr x0)] at xn
State after:
case neg.mp.intro.intro.intro
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
x : ℕ
xn : x = n
x0 : ¬x = 0
xN : x ∈ N
⊢ n ∈ N

State before:
case neg.mp.intro.intro.intro
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
x : ℕ
xn : x = n
x0 : ¬x = 0
xN : x ∈ N
⊢ n ∈ N
Tactic:
rwa [←xn]
State after:
no goals

State before:
case neg.mpr
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
⊢ n ∈ N → ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n
Tactic:
intro h
State after:
case neg.mpr
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
h : n ∈ N
⊢ ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n

State before:
case neg.mpr
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
h : n ∈ N
⊢ ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n
Tactic:
exists n
State after:
case neg.mpr
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
h : n ∈ N
⊢ (¬n = 0 ∧ n ∈ N) ∧ n - 1 + 1 = n

State before:
case neg.mpr
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
h : n ∈ N
⊢ (¬n = 0 ∧ n ∈ N) ∧ n - 1 + 1 = n
Tactic:
use ⟨n0,h⟩
State after:
case right
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
h : n ∈ N
⊢ n - 1 + 1 = n

State before:
case right
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
h : n ∈ N
⊢ n - 1 + 1 = n
Tactic:
exact Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr n0)
State after:
no goals