∀ {α : Type u_3} {β : Type u_1} (m : α → β) {f : Filter α} (F : f.Realizer),
  { f := fun s => m '' F.F.f s, pt := F.F.pt, inf := F.F.inf, inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter =
    Filter.map m f