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

State before:
⊢ Set.range push = {N | 0 ∈ N}
Tactic:
rw [Set.range]
State after:
⊢ {x | ∃ y, push y = x} = {N | 0 ∈ N}

State before:
⊢ {x | ∃ y, push y = x} = {N | 0 ∈ N}
Tactic:
apply Set.ext
State after:
case h

⊢ ∀ (x : Finset ℕ), x ∈ {x | ∃ y, push y = x} ↔ x ∈ {N | 0 ∈ N}

State before:
case h

⊢ ∀ (x : Finset ℕ), x ∈ {x | ∃ y, push y = x} ↔ x ∈ {N | 0 ∈ N}
Tactic:
simp
State after:
case h

⊢ ∀ (x : Finset ℕ), (∃ y, push y = x) ↔ 0 ∈ x

State before:
case h

⊢ ∀ (x : Finset ℕ), (∃ y, push y = x) ↔ 0 ∈ x
Tactic:
intro N
State after:
case h
N : Finset ℕ
⊢ (∃ y, push y = N) ↔ 0 ∈ N

State before:
case h
N : Finset ℕ
⊢ (∃ y, push y = N) ↔ 0 ∈ N
Tactic:
constructor
State after:
case h.mp
N : Finset ℕ
⊢ (∃ y, push y = N) → 0 ∈ N

case h.mpr
N : Finset ℕ
⊢ 0 ∈ N → ∃ y, push y = N

State before:
case h.mp
N : Finset ℕ
⊢ (∃ y, push y = N) → 0 ∈ N
Tactic:
intro h
State after:
case h.mp
N : Finset ℕ
h : ∃ y, push y = N
⊢ 0 ∈ N

State before:
case h.mp
N : Finset ℕ
h : ∃ y, push y = N
⊢ 0 ∈ N
Tactic:
rcases h with ⟨M, H⟩
State after:
case h.mp.intro
N M : Finset ℕ
H : push M = N
⊢ 0 ∈ N

State before:
case h.mp.intro
N M : Finset ℕ
H : push M = N
⊢ 0 ∈ N
Tactic:
rw [push] at H
State after:
case h.mp.intro
N M : Finset ℕ
H : insert 0 (Finset.image (fun n => n + 1) M) = N
⊢ 0 ∈ N

State before:
case h.mp.intro
N M : Finset ℕ
H : insert 0 (Finset.image (fun n => n + 1) M) = N
⊢ 0 ∈ N
Tactic:
rw [← H]
State after:
case h.mp.intro
N M : Finset ℕ
H : insert 0 (Finset.image (fun n => n + 1) M) = N
⊢ 0 ∈ insert 0 (Finset.image (fun n => n + 1) M)

State before:
case h.mp.intro
N M : Finset ℕ
H : insert 0 (Finset.image (fun n => n + 1) M) = N
⊢ 0 ∈ insert 0 (Finset.image (fun n => n + 1) M)
Tactic:
exact Finset.mem_insert_self 0 _
State after:
no goals

State before:
case h.mpr
N : Finset ℕ
⊢ 0 ∈ N → ∃ y, push y = N
Tactic:
intro N0
State after:
case h.mpr
N : Finset ℕ
N0 : 0 ∈ N
⊢ ∃ y, push y = N

State before:
case h.mpr
N : Finset ℕ
N0 : 0 ∈ N
⊢ ∃ y, push y = N
Tactic:
exists pop N
State after:
case h.mpr
N : Finset ℕ
N0 : 0 ∈ N
⊢ push (pop N) = N

State before:
case h.mpr
N : Finset ℕ
N0 : 0 ∈ N
⊢ push (pop N) = N
Tactic:
rw [push_pop]
State after:
case h.mpr
N : Finset ℕ
N0 : 0 ∈ N
⊢ insert 0 N = N

State before:
case h.mpr
N : Finset ℕ
N0 : 0 ∈ N
⊢ insert 0 N = N
Tactic:
exact Finset.insert_eq_of_mem N0
State after:
no goals