∀ {α : Type u_1} {f g : Filter α} (F : f.Realizer) (G : g.Realizer),
  {
        f := fun x =>
          match x with
          | (s, t) => F.F.f s ∪ G.F.f t,
        pt := (F.F.pt, G.F.pt),
        inf := fun x x_1 =>
          match x with
          | (a, a') =>
            match x_1 with
            | (b, b') => (F.F.inf a b, G.F.inf a' b'),
        inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter =
    f ⊔ g