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

State before:
⊢ Filter.comap push atTop = atTop
Tactic:
apply Filter.comap_embedding_atTop
State after:
case hm

⊢ ∀ (b₁ b₂ : Finset ℕ), push b₁ ≤ push b₂ ↔ b₁ ≤ b₂

case hu

⊢ ∀ (c : Finset ℕ), ∃ b, c ≤ push b

State before:
case hm

⊢ ∀ (b₁ b₂ : Finset ℕ), push b₁ ≤ push b₂ ↔ b₁ ≤ b₂

case hu

⊢ ∀ (c : Finset ℕ), ∃ b, c ≤ push b
Tactic:
exact @push_le_push
State after:
case hu

⊢ ∀ (c : Finset ℕ), ∃ b, c ≤ push b

State before:
case hu

⊢ ∀ (c : Finset ℕ), ∃ b, c ≤ push b
Tactic:
intro N
State after:
case hu
N : Finset ℕ
⊢ ∃ b, N ≤ push b

State before:
case hu
N : Finset ℕ
⊢ ∃ b, N ≤ push b
Tactic:
exists pop N
State after:
case hu
N : Finset ℕ
⊢ N ≤ push (pop N)

State before:
case hu
N : Finset ℕ
⊢ N ≤ push (pop N)
Tactic:
rw [push_pop]
State after:
case hu
N : Finset ℕ
⊢ N ≤ insert 0 N

State before:
case hu
N : Finset ℕ
⊢ N ≤ insert 0 N
Tactic:
simp
State after:
no goals