no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.261626
ι : Sort x
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s✝ : Set α
t : Set β
f g : Filter α
m : α → β
s : Set α
hsf : s ∈ f
hsg : s ∈ g
hm : InjOn m s
⊢ map m f = map m g ↔ f = g
simp only [le_antisymm_iff, map_le_map_iff_of_injOn hsf hsg hm,
  map_le_map_iff_of_injOn hsg hsf hm]