-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
F : Realizer.{u_1, u_5} f
G : (i : α) → Realizer.{u_2, u_6} (m i)
x : Set β
obtain :
  ∀ (σ : Type u_5) (F : CFilter.{u_1, u_5} (Set α) σ) (eq : F.toFilter = f),
    Membership.mem (γ := Set (Set β))
        (sets
          (CFilter.toFilter (σ :=
            (s : { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ) ×
              ((i : α) → i ∈ { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s → (G i).σ))
            {
              f :=
                fun
                  (x :
                    (s : { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ) ×
                      ((i : α) → i ∈ { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s → (G i).σ)) ↦
                match (motive :=
                  (s : { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ) ×
                      ((i : α) → i ∈ { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s → (G i).σ) →
                    Set β)
                  x with
                | ⟨s, f_1⟩ =>
                  ⋃ (i : α),
                    ⋃ (h : i ∈ { σ := σ, 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 : { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ) ↦
                  (i : α) → i ∈ { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s → (G i).σ)
                  { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.pt
                  fun (i : α)
                    (x :
                      i ∈
                        { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f
                          { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.pt) ↦
                  (G i).F.pt,
              inf :=
                fun
                  (x x_1 :
                    (s : { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ) ×
                      ((i : α) → i ∈ { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s → (G i).σ)) ↦
                match (motive :=
                  (s : { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ) ×
                      ((i : α) → i ∈ { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s → (G i).σ) →
                    (s : { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ) ×
                      ((i : α) → i ∈ { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s → (G i).σ))
                  x with
                | ⟨a, f_1⟩ =>
                  match (motive :=
                    (s : { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ) ×
                        ((i : α) → i ∈ { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s → (G i).σ) →
                      (s : { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ) ×
                        ((i : α) → i ∈ { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s → (G i).σ))
                    x_1 with
                  | ⟨b, f'⟩ =>
                    Sigma.mk (β := fun (s : { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ) ↦
                      (i : α) → i ∈ { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s → (G i).σ)
                      ({ σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.inf a b)
                      fun (i : α)
                        (h :
                          i ∈
                            { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f
                              ({ σ := σ, 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
⊢ Membership.mem (γ := Set (Set β))
      (sets
        (CFilter.toFilter (σ := (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ))
          {
            f := fun (x : (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ)) ↦
              match (motive := (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ) → Set β) x with
              | ⟨s, f_1⟩ => ⋃ (i : α), ⋃ (h : i ∈ F.F.f s), (G i).F.f (f_1 i h),
            pt :=
              Sigma.mk (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ) F.F.pt
                fun (i : α) (x : i ∈ F.F.f F.F.pt) ↦ (G i).F.pt,
            inf := fun (x x_1 : (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ)) ↦
              match (motive :=
                (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ) → (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ)) x with
              | ⟨a, f_1⟩ =>
                match (motive :=
                  (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ) → (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ))
                  x_1 with
                | ⟨b, f'⟩ =>
                  Sigma.mk (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ) (F.F.inf a b)
                    fun (i : α) (h : i ∈ F.F.f (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:
obtain ⟨_, F, _⟩ := F