-- Module: Mathlib.Data.Analysis.Filter
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
subst :
  Membership.mem (γ := Set (Set β))
      (sets
        (CFilter.toFilter (σ :=
          (s : { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.σ) ×
            ((i : α) → i ∈ { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.F.f s → (G i).σ))
          {
            f :=
              fun
                (x :
                  (s : { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.σ) ×
                    ((i : α) → i ∈ { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.F.f s → (G i).σ)) ↦
              match (motive :=
                (s : { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.σ) ×
                    ((i : α) → i ∈ { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.F.f s → (G i).σ) →
                  Set β)
                x with
              | ⟨s, f⟩ =>
                ⋃ (i : α),
                  ⋃ (h : i ∈ { σ := σ_1, F := F, eq := ⋯ : 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 := ⋯ : Realizer.{u_1, u_5} F.toFilter }.σ) ↦
                (i : α) → i ∈ { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.F.f s → (G i).σ)
                { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.F.pt
                fun (i : α)
                  (x :
                    i ∈
                      { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.F.f
                        { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.F.pt) ↦
                (G i).F.pt,
            inf :=
              fun
                (x x_1 :
                  (s : { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.σ) ×
                    ((i : α) → i ∈ { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.F.f s → (G i).σ)) ↦
              match (motive :=
                (s : { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.σ) ×
                    ((i : α) → i ∈ { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.F.f s → (G i).σ) →
                  (s : { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.σ) ×
                    ((i : α) → i ∈ { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.F.f s → (G i).σ))
                x with
              | ⟨a, f⟩ =>
                match (motive :=
                  (s : { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.σ) ×
                      ((i : α) → i ∈ { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.F.f s → (G i).σ) →
                    (s : { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.σ) ×
                      ((i : α) → i ∈ { σ := σ_1, F := F, eq := ⋯ : 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 := ⋯ : Realizer.{u_1, u_5} F.toFilter }.σ) ↦
                    (i : α) → i ∈ { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.F.f s → (G i).σ)
                    ({ σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.F.inf a b)
                    fun (i : α)
                      (h :
                        i ∈
                          { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.F.f
                            ({ σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.F.inf a b)) ↦
                    (G i).F.inf (f i ⋯) (f' i ⋯),
            inf_le_left := ⋯, inf_le_right := ⋯ }))
      x ↔
    x ∈ (F.toFilter.bind m).sets
⊢ 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

Tactic:
subst f