no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.256139
ι : Sort x
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m : α → β
m' : β → γ
s : Set α
t : Set β
⊢ comap m (g₁ ⊔ g₂) = comap m g₁ ⊔ comap m g₂
rw [sup_eq_iSup, comap_iSup, iSup_bool_eq, Bool.cond_true, Bool.cond_false]