no goals
α : Type u_1
β : Type u_2
γ : Type ?u.21450
ι : Sort ?u.21453
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
f : Filter α
g h : Set α → Filter β
⊢ (Filter.lift f fun x => g x ⊓ h x) = Filter.lift f g ⊓ Filter.lift f h
simp only [Filter.lift, iInf_inf_eq]