no goals
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.37925
f f₁ f₂ : Filter α
h✝ h₁ h₂ g : Set α → Set β
h : Set β → Filter γ
hg : Monotone g
hh : Monotone h
⊢ (Filter.lift f fun s => Filter.lift (𝓟 (g s)) h) = Filter.lift f fun s => h (g s)
simp only [lift_principal, hh, eq_self_iff_true]