no goals
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.12988
f f₁ f₂ : Filter α
g g₁ g₂ : Set α → Filter β
m : β → γ
hg : Monotone g
this : Monotone (map m ∘ g)
s : Set γ
⊢ s ∈ map m (Filter.lift f g) ↔ s ∈ Filter.lift f (map m ∘ g)
simp only [mem_lift_sets hg, mem_lift_sets this, exists_prop, mem_map, Function.comp_apply]