no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.283383
ι : Sort x
m : α → β
hm : Injective m
f₁ f₂ : Filter α
⊢ Disjoint (map m f₁) (map m f₂) ↔ Disjoint f₁ f₂
simp only [disjoint_iff, ← map_inf hm, map_eq_bot_iff]