-- Lean 4 proof step from Mathlib.Data.Analysis.Filter (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
x : Set α
σ_1 : Type u_5
F : CFilter.{u_1, u_5} (Set α) σ_1
eq : F.toFilter = f
σ_2 : Type u_6
F_1 : CFilter.{u_1, u_6} (Set α) σ_2
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 }.σ
                    { σ := σ_2, 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 }.σ
                    { σ := σ_2, 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 ∪
                  { σ := σ_2, 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,
                { σ := σ_2, 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 }.σ
                    { σ := σ_2, 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 }.σ
                    { σ := σ_2, 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 }.σ
                    { σ := σ_2, 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 }.σ
                      { σ := σ_2, 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 }.σ
                      { σ := σ_2, 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,
                    { σ := σ_2, 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 }.σ
                { σ := σ_2, F := F_1, eq := eq_1 : Realizer.{u_1, u_6} g }.σ) }))
      x ↔
    x ∈ (f ⊔ g).sets
have mk : Membership.mem (γ := Set (Set α))
    (sets
      (CFilter.toFilter
        {
          f :=
            fun
              (x :
                Prod.{u_5, u_6} { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.σ
                  { σ := σ_2, F := F_1, eq := sorry : Realizer.{u_1, u_6} F_1.toFilter }.σ) ↦
            match (motive :=
              Prod.{u_5, u_6} { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.σ
                  { σ := σ_2, F := F_1, eq := sorry : Realizer.{u_1, u_6} F_1.toFilter }.σ →
                Set α)
              x with
            | (s, t) =>
              { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.F.f s ∪
                { σ := σ_2, F := F_1, eq := sorry : Realizer.{u_1, u_6} F_1.toFilter }.F.f t,
          pt :=
            ({ σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.F.pt,
              { σ := σ_2, F := F_1, eq := sorry : Realizer.{u_1, u_6} F_1.toFilter }.F.pt),
          inf :=
            fun
              (x x_1 :
                Prod.{u_5, u_6} { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.σ
                  { σ := σ_2, F := F_1, eq := sorry : Realizer.{u_1, u_6} F_1.toFilter }.σ) ↦
            match (motive :=
              Prod.{u_5, u_6} { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.σ
                  { σ := σ_2, F := F_1, eq := sorry : Realizer.{u_1, u_6} F_1.toFilter }.σ →
                Prod.{u_5, u_6} { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.σ
                  { σ := σ_2, F := F_1, eq := sorry : Realizer.{u_1, u_6} F_1.toFilter }.σ)
              x with
            | (a, a') =>
              match (motive :=
                Prod.{u_5, u_6} { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.σ
                    { σ := σ_2, F := F_1, eq := sorry : Realizer.{u_1, u_6} F_1.toFilter }.σ →
                  Prod.{u_5, u_6} { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.σ
                    { σ := σ_2, F := F_1, eq := sorry : Realizer.{u_1, u_6} F_1.toFilter }.σ)
                x_1 with
              | (b, b') =>
                ({ σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.F.inf a b,
                  { σ := σ_2, F := F_1, eq := sorry : Realizer.{u_1, u_6} F_1.toFilter }.F.inf a' b'),
          inf_le_left := sorry, inf_le_right := sorry :
          CFilter (Set α)
            (Prod.{u_5, u_6} { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.σ
              { σ := σ_2, F := F_1, eq := sorry : Realizer.{u_1, u_6} F_1.toFilter }.σ) }))
    x ↔
  x ∈ (F.toFilter ⊔ F_1.toFilter).sets
Tactic: substs f g
Cleared hypotheses: f, g, eq, eq_1