no goals
α : Type u_1
β : Type u_2
γ : Type ?u.36150
ι : Sort ?u.36153
f f₁ f₂ : Filter α
h h₁ h₂ : Set α → Set β
a : α
hh : Monotone h
⊢ Filter.lift' (pure a) h = 𝓟 (h {a})
rw [← principal_singleton, lift'_principal hh]