-- Lean 4 proof step from Mathlib.Data.Analysis.Filter (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
G : (i : α) → Realizer.{u_2, u_6} (m i)
x : Set β
σ_1 : Type u_5
F : CFilter.{u_1, u_5} (Set α) σ_1
eq : F.toFilter = f
⊢ Membership.mem (γ := Set (Set β))
      (sets
        (CFilter.toFilter (σ :=
          (s : { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ) ×
            ((i : α) → i ∈ { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s → (G i).σ))
          {
            f :=
              fun
                (x :
                  (s : { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ) ×
                    ((i : α) → i ∈ { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s → (G i).σ)) ↦
              match (motive :=
                (s : { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ) ×
                    ((i : α) → i ∈ { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s → (G i).σ) →
                  Set β)
                x with
              | ⟨s, f_1⟩ =>
                ⋃ (i : α),
                  ⋃ (h : i ∈ { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s), (G i).F.f (f_1 i h),
            pt :=
              Sigma.mk (β := fun (s : { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ) ↦
                (i : α) → i ∈ { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s → (G i).σ)
                { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.pt
                fun (i : α)
                  (x :
                    i ∈
                      { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f
                        { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.pt) ↦
                (G i).F.pt,
            inf :=
              fun
                (x x_1 :
                  (s : { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ) ×
                    ((i : α) → i ∈ { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s → (G i).σ)) ↦
              match (motive :=
                (s : { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ) ×
                    ((i : α) → i ∈ { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s → (G i).σ) →
                  (s : { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ) ×
                    ((i : α) → i ∈ { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s → (G i).σ))
                x with
              | ⟨a, f_1⟩ =>
                match (motive :=
                  (s : { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ) ×
                      ((i : α) → i ∈ { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s → (G i).σ) →
                    (s : { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ) ×
                      ((i : α) → i ∈ { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s → (G i).σ))
                  x_1 with
                | ⟨b, f'⟩ =>
                  Sigma.mk (β := fun (s : { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ) ↦
                    (i : α) → i ∈ { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s → (G i).σ)
                    ({ σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.inf a b)
                    fun (i : α)
                      (h :
                        i ∈
                          { σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f
                            ({ σ := σ_1, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.inf a b)) ↦
                    (G i).F.inf (f_1 i ⋯) (f' i ⋯),
            inf_le_left := ⋯, inf_le_right := ⋯ }))
      x ↔
    x ∈ (f.bind m).sets
have subst : Membership.mem (γ := Set (Set β))
    (sets
      (CFilter.toFilter (σ :=
        (s : { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.σ) ×
          ((i : α) → i ∈ { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.F.f s → (G i).σ))
        {
          f :=
            fun
              (x :
                (s : { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.σ) ×
                  ((i : α) → i ∈ { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.F.f s → (G i).σ)) ↦
            match (motive :=
              (s : { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.σ) ×
                  ((i : α) → i ∈ { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.F.f s → (G i).σ) →
                Set β)
              x with
            | ⟨s, f⟩ =>
              ⋃ (i : α),
                ⋃ (h : i ∈ { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.F.f s), (G i).F.f (f i h),
          pt :=
            Sigma.mk (β := fun (s : { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.σ) ↦
              (i : α) → i ∈ { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.F.f s → (G i).σ)
              { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.F.pt
              fun (i : α)
                (x :
                  i ∈
                    { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.F.f
                      { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.F.pt) ↦
              (G i).F.pt,
          inf :=
            fun
              (x x_1 :
                (s : { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.σ) ×
                  ((i : α) → i ∈ { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.F.f s → (G i).σ)) ↦
            match (motive :=
              (s : { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.σ) ×
                  ((i : α) → i ∈ { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.F.f s → (G i).σ) →
                (s : { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.σ) ×
                  ((i : α) → i ∈ { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.F.f s → (G i).σ))
              x with
            | ⟨a, f⟩ =>
              match (motive :=
                (s : { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.σ) ×
                    ((i : α) → i ∈ { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.F.f s → (G i).σ) →
                  (s : { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.σ) ×
                    ((i : α) → i ∈ { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.F.f s → (G i).σ))
                x_1 with
              | ⟨b, f'⟩ =>
                Sigma.mk (β := fun (s : { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.σ) ↦
                  (i : α) → i ∈ { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.F.f s → (G i).σ)
                  ({ σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.F.inf a b)
                  fun (i : α)
                    (h :
                      i ∈
                        { σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.F.f
                          ({ σ := σ_1, F := F, eq := sorry : Realizer.{u_1, u_5} F.toFilter }.F.inf a b)) ↦
                  (G i).F.inf (f i sorry) (f' i sorry),
          inf_le_left := sorry, inf_le_right := sorry }))
    x ↔
  x ∈ (F.toFilter.bind m).sets
Tactic: subst f
Cleared hypotheses: f, eq