no goals
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.32727
f f₁ f₂ : Filter α
h h₁ h₂ : Set α → Set β
m : β → γ
hh : Monotone h
⊢ Filter.lift f (map m ∘ 𝓟 ∘ h) = Filter.lift' f (image m ∘ h)
simp only [comp, Filter.lift', map_principal]