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

State before:
A : Type
f : Finset ℕ → A
l : Filter A
⊢ Filter.Tendsto (f ∘ push) atTop l ↔ Filter.Tendsto f atTop l
Tactic:
nth_rw 1 [← push_comap_atTop]
State after:
A : Type
f : Finset ℕ → A
l : Filter A
⊢ Filter.Tendsto (f ∘ push) (Filter.comap push atTop) l ↔ Filter.Tendsto f atTop l

State before:
A : Type
f : Finset ℕ → A
l : Filter A
⊢ Filter.Tendsto (f ∘ push) (Filter.comap push atTop) l ↔ Filter.Tendsto f atTop l
Tactic:
apply Filter.tendsto_comap'_iff
State after:
case h
A : Type
f : Finset ℕ → A
l : Filter A
⊢ Set.range push ∈ atTop

State before:
case h
A : Type
f : Finset ℕ → A
l : Filter A
⊢ Set.range push ∈ atTop
Tactic:
rw [push_range]
State after:
case h
A : Type
f : Finset ℕ → A
l : Filter A
⊢ {N | 0 ∈ N} ∈ atTop

State before:
case h
A : Type
f : Finset ℕ → A
l : Filter A
⊢ {N | 0 ∈ N} ∈ atTop
Tactic:
have h : {N : Finset ℕ | 0 ∈ N} = {N : Finset ℕ | {0} ≤ N} := by simp
State after:
case h
A : Type
f : Finset ℕ → A
l : Filter A
h : {N | 0 ∈ N} = {N | {0} ≤ N}
⊢ {N | 0 ∈ N} ∈ atTop

State before:
case h
A : Type
f : Finset ℕ → A
l : Filter A
h : {N | 0 ∈ N} = {N | {0} ≤ N}
⊢ {N | 0 ∈ N} ∈ atTop
Tactic:
rw [h]
State after:
case h
A : Type
f : Finset ℕ → A
l : Filter A
h : {N | 0 ∈ N} = {N | {0} ≤ N}
⊢ {N | {0} ≤ N} ∈ atTop

State before:
case h
A : Type
f : Finset ℕ → A
l : Filter A
h : {N | 0 ∈ N} = {N | {0} ≤ N}
⊢ {N | {0} ≤ N} ∈ atTop
Tactic:
exact Filter.mem_atTop _
State after:
no goals

State before:
A : Type
f : Finset ℕ → A
l : Filter A
⊢ {N | 0 ∈ N} = {N | {0} ≤ N}
Tactic:
simp
State after:
no goals