no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.252749
ι : Sort x
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m : α → β
m' : β → γ
s : Set α
t : Set β
⊢ comap m (g ⊓ 𝓟 (range m)) = comap m g
simpa only [le_principal_iff, comap_inf, comap_principal, preimage_range, principal_univ,
  inf_eq_left] using le_top