-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
G : Realizer.{u_1, u_6} g
x : Set α
σ_1 : Type u_5
F : CFilter.{u_1, u_5} (Set α) σ_1
eq : F.toFilter = f
mk :
  ∀ (σ : Type u_6) (F_1 : CFilter.{u_1, u_6} (Set α) σ) (eq_1 : F_1.toFilter = g),
    Membership.mem (γ := Set (Set α))
        (sets
          (CFilter.toFilter
            {
              f :=
                fun
                  (x :
                    Prod.{u_5, u_6} { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ
                      { σ := σ, F := F_1, eq := eq_1 : Realizer.{u_1, u_6} g }.σ) ↦
                match (motive :=
                  Prod.{u_5, u_6} { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ
                      { σ := σ, F := F_1, eq := eq_1 : Realizer.{u_1, u_6} g }.σ →
                    Set α)
                  x with
                | (s, t) =>
                  { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s ∪
                    { σ := σ, F := F_1, eq := eq_1 : Realizer.{u_1, u_6} g }.F.f t,
              pt :=
                ({ σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.pt,
                  { σ := σ, F := F_1, eq := eq_1 : Realizer.{u_1, u_6} g }.F.pt),
              inf :=
                fun
                  (x x_1 :
                    Prod.{u_5, u_6} { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ
                      { σ := σ, F := F_1, eq := eq_1 : Realizer.{u_1, u_6} g }.σ) ↦
                match (motive :=
                  Prod.{u_5, u_6} { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ
                      { σ := σ, F := F_1, eq := eq_1 : Realizer.{u_1, u_6} g }.σ →
                    Prod.{u_5, u_6} { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ
                      { σ := σ, F := F_1, eq := eq_1 : Realizer.{u_1, u_6} g }.σ)
                  x with
                | (a, a') =>
                  match (motive :=
                    Prod.{u_5, u_6} { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ
                        { σ := σ, F := F_1, eq := eq_1 : Realizer.{u_1, u_6} g }.σ →
                      Prod.{u_5, u_6} { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ
                        { σ := σ, F := F_1, eq := eq_1 : Realizer.{u_1, u_6} g }.σ)
                    x_1 with
                  | (b, b') =>
                    ({ σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.inf a b,
                      { σ := σ, F := F_1, eq := eq_1 : Realizer.{u_1, u_6} g }.F.inf a' b'),
              inf_le_left := ⋯, inf_le_right := ⋯ :
              CFilter (Set α)
                (Prod.{u_5, u_6} { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ
                  { σ := σ, F := F_1, eq := eq_1 : Realizer.{u_1, u_6} g }.σ) }))
        x ↔
      x ∈ (f ⊔ g).sets
⊢ Membership.mem (γ := Set (Set α))
      (sets
        (CFilter.toFilter
          {
            f := fun (x : Prod.{u_5, u_6} { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ) ↦
              match (motive := Prod.{u_5, u_6} { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ → Set α)
                x with
              | (s, t) => { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s ∪ G.F.f t,
            pt := ({ σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.pt, G.F.pt),
            inf := fun (x x_1 : Prod.{u_5, u_6} { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ) ↦
              match (motive :=
                Prod.{u_5, u_6} { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ →
                  Prod.{u_5, u_6} { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ)
                x with
              | (a, a') =>
                match (motive :=
                  Prod.{u_5, u_6} { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ →
                    Prod.{u_5, u_6} { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ)
                  x_1 with
                | (b, b') => ({ σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.inf a b, G.F.inf a' b'),
            inf_le_left := ⋯, inf_le_right := ⋯ :
            CFilter (Set α) (Prod.{u_5, u_6} { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ) }))
      x ↔
    x ∈ (f ⊔ g).sets

Tactic:
cases G