no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.264840
ι : Sort x
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m : α → β
m' : β → γ
s : Set α
t : Set β
h : Surjective m
⊢ Disjoint (comap m g₁) (comap m g₂) ↔ Disjoint g₁ g₂
rw [disjoint_iff, disjoint_iff, ← comap_inf, comap_surjective_eq_bot h]