awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
x : Set α
σ_1 : Type u_5
F : CFilter.{u_2, u_5} (Set β) σ_1
⊢ Membership.mem (γ := Set (Set α))
      (sets
        (CFilter.toFilter
          {
            f := fun (s : { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_2, u_5} F.toFilter }.σ) ↦
              m ⁻¹' { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_2, u_5} F.toFilter }.F.f s,
            pt := { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_2, u_5} F.toFilter }.F.pt,
            inf := { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_2, u_5} F.toFilter }.F.inf, inf_le_left := ⋯,
            inf_le_right := ⋯ :
            CFilter.{u_1, u_5} (Set α) { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_2, u_5} F.toFilter }.σ }))
      x ↔
    x ∈ (comap m F.toFilter).sets

Tactic:
⟨fun ⟨s, h⟩ ↦ ⟨_, ⟨s, Subset.refl _⟩, h⟩,
        fun ⟨_, ⟨s, h⟩, h₂⟩ ↦ ⟨s, Subset.trans (preimage_mono h) h₂⟩⟩

Premises used: Filter.Realizer.mk, CFilter.toFilter, CFilter.inf, Set.Subset.refl, Set.Subset.trans, _private.0.Filter.Realizer.comap.match_2, Membership.mem, Filter.sets, Set.preimage_mono, Set.preimage, Filter.Realizer.F, And.intro, Iff.intro, Exists.intro, Eq.refl, CFilter.inf_le_left, CFilter.mk, CFilter.pt, _private.0.Filter.Realizer.comap.match_1, CFilter.inf_le_right, Filter.comap, CFilter.f
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
x : Set α
σ_1 : Type u_5
F : CFilter.{u_2, u_5} (Set β) σ_1
⊢ Membership.mem (γ := Set (Set α))
      (sets
        (CFilter.toFilter
          {
            f := fun (s : { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_2, u_5} F.toFilter }.σ) ↦
              m ⁻¹' { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_2, u_5} F.toFilter }.F.f s,
            pt := { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_2, u_5} F.toFilter }.F.pt,
            inf := { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_2, u_5} F.toFilter }.F.inf, inf_le_left := ⋯,
            inf_le_right := ⋯ :
            CFilter.{u_1, u_5} (Set α) { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_2, u_5} F.toFilter }.σ }))
      x ↔
    x ∈ (comap m F.toFilter).sets

Tactic:
exact ⟨fun ⟨s, h⟩ ↦ ⟨_, ⟨s, Subset.refl _⟩, h⟩,
        fun ⟨_, ⟨s, h⟩, h₂⟩ ↦ ⟨s, Subset.trans (preimage_mono h) h₂⟩⟩
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
F : Realizer.{u_1, u_5} f
G : Realizer.{u_1, u_6} g
x : Set α
mk :
  ∀ (σ : Type u_5) (F : CFilter.{u_1, u_5} (Set α) σ) (eq : F.toFilter = f),
    Membership.mem (γ := Set (Set α))
        (sets
          (CFilter.toFilter
            {
              f := fun (x : Prod.{u_5, u_6} { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ) ↦
                match (motive := Prod.{u_5, u_6} { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ → Set α)
                  x with
                | (s, t) => { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s ∪ G.F.f t,
              pt := ({ σ := σ, 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} { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ) ↦
                match (motive :=
                  Prod.{u_5, u_6} { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ →
                    Prod.{u_5, u_6} { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ)
                  x with
                | (a, a') =>
                  match (motive :=
                    Prod.{u_5, u_6} { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ →
                      Prod.{u_5, u_6} { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ)
                    x_1 with
                  | (b, b') => ({ σ := σ, 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} { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ) }))
        x ↔
      x ∈ (f ⊔ g).sets
⊢ Membership.mem (γ := Set (Set α))
      (sets
        (CFilter.toFilter
          {
            f := fun (x : Prod.{u_5, u_6} F.σ G.σ) ↦
              match (motive := Prod.{u_5, u_6} F.σ G.σ → Set α) x with
              | (s, t) => F.F.f s ∪ G.F.f t,
            pt := (F.F.pt, G.F.pt),
            inf := fun (x x_1 : Prod.{u_5, u_6} F.σ G.σ) ↦
              match (motive := Prod.{u_5, u_6} F.σ G.σ → Prod.{u_5, u_6} F.σ G.σ) x with
              | (a, a') =>
                match (motive := Prod.{u_5, u_6} F.σ G.σ → Prod.{u_5, u_6} F.σ G.σ) x_1 with
                | (b, b') => (F.F.inf a b, G.F.inf a' b'),
            inf_le_left := ⋯, inf_le_right := ⋯ : CFilter (Set α) (Prod.{u_5, u_6} F.σ G.σ) }))
      x ↔
    x ∈ (f ⊔ g).sets

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

Tactic:
simp [CFilter.toFilter]

Premises used: CFilter.toFilter
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
F : Realizer.{u_1, u_5} f
G : Realizer.{u_1, u_6} g
mk :
  ∀ (σ : Type u_5) (F : CFilter.{u_1, u_5} (Set α) σ) (eq : F.toFilter = f),
    CFilter.toFilter
        {
          f := fun (x : Prod.{u_5, u_6} { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ) ↦
            match (motive := Prod.{u_5, u_6} { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ → Set α) x with
            | (s, t) => { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.F.f s ∩ G.F.f t,
          pt := ({ σ := σ, 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} { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ) ↦
            match (motive :=
              Prod.{u_5, u_6} { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ →
                Prod.{u_5, u_6} { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ)
              x with
            | (a, a') =>
              match (motive :=
                Prod.{u_5, u_6} { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ →
                  Prod.{u_5, u_6} { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ)
                x_1 with
              | (b, b') => ({ σ := σ, 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} { σ := σ, F := F, eq := eq : Realizer.{u_1, u_5} f }.σ G.σ) } =
      f ⊓ g
⊢ CFilter.toFilter
      {
        f := fun (x : Prod.{u_5, u_6} F.σ G.σ) ↦
          match (motive := Prod.{u_5, u_6} F.σ G.σ → Set α) x with
          | (s, t) => F.F.f s ∩ G.F.f t,
        pt := (F.F.pt, G.F.pt),
        inf := fun (x x_1 : Prod.{u_5, u_6} F.σ G.σ) ↦
          match (motive := Prod.{u_5, u_6} F.σ G.σ → Prod.{u_5, u_6} F.σ G.σ) x with
          | (a, a') =>
            match (motive := Prod.{u_5, u_6} F.σ G.σ → Prod.{u_5, u_6} F.σ G.σ) x_1 with
            | (b, b') => (F.F.inf a b, G.F.inf a' b'),
        inf_le_left := ⋯, inf_le_right := ⋯ : CFilter (Set α) (Prod.{u_5, u_6} F.σ G.σ) } =
    f ⊓ g

Tactic:
cases F
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ_1 : Type u_5
F : CFilter.{u_1, u_5} (Set α) σ_1
σ_2 : Type u_6
F_1 : CFilter.{u_1, u_6} (Set α) σ_2
mk :
  { sets := {a : Set α | ∃ (a_1 : σ_1) (b : σ_2), F.f a_1 ∩ F_1.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯,
      inter_sets := ⋯ : Filter α } =
    { sets := {a : Set α | ∃ (b : σ_1), F.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } ⊓
      { sets := {a : Set α | ∃ (b : σ_2), F_1.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
⊢ CFilter.toFilter
      {
        f :=
          fun
            (x :
              Prod.{u_5, u_6} { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.σ
                { σ := σ_2, F := F_1, eq := ⋯ : Realizer.{u_1, u_6} F_1.toFilter }.σ) ↦
          match (motive :=
            Prod.{u_5, u_6} { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.σ
                { σ := σ_2, F := F_1, eq := ⋯ : Realizer.{u_1, u_6} F_1.toFilter }.σ →
              Set α)
            x with
          | (s, t) =>
            { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.F.f s ∩
              { σ := σ_2, F := F_1, eq := ⋯ : Realizer.{u_1, u_6} F_1.toFilter }.F.f t,
        pt :=
          ({ σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.F.pt,
            { σ := σ_2, F := F_1, eq := ⋯ : Realizer.{u_1, u_6} F_1.toFilter }.F.pt),
        inf :=
          fun
            (x x_1 :
              Prod.{u_5, u_6} { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.σ
                { σ := σ_2, F := F_1, eq := ⋯ : Realizer.{u_1, u_6} F_1.toFilter }.σ) ↦
          match (motive :=
            Prod.{u_5, u_6} { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.σ
                { σ := σ_2, F := F_1, eq := ⋯ : Realizer.{u_1, u_6} F_1.toFilter }.σ →
              Prod.{u_5, u_6} { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.σ
                { σ := σ_2, F := F_1, eq := ⋯ : Realizer.{u_1, u_6} F_1.toFilter }.σ)
            x with
          | (a, a') =>
            match (motive :=
              Prod.{u_5, u_6} { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.σ
                  { σ := σ_2, F := F_1, eq := ⋯ : Realizer.{u_1, u_6} F_1.toFilter }.σ →
                Prod.{u_5, u_6} { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.σ
                  { σ := σ_2, F := F_1, eq := ⋯ : Realizer.{u_1, u_6} F_1.toFilter }.σ)
              x_1 with
            | (b, b') =>
              ({ σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.F.inf a b,
                { σ := σ_2, F := F_1, eq := ⋯ : Realizer.{u_1, u_6} F_1.toFilter }.F.inf a' b'),
        inf_le_left := ⋯, inf_le_right := ⋯ :
        CFilter (Set α)
          (Prod.{u_5, u_6} { σ := σ_1, F := F, eq := ⋯ : Realizer.{u_1, u_5} F.toFilter }.σ
            { σ := σ_2, F := F_1, eq := ⋯ : Realizer.{u_1, u_6} F_1.toFilter }.σ) } =
    F.toFilter ⊓ F_1.toFilter

Tactic:
simp only [CFilter.toFilter, Prod.exists]

Premises used: CFilter.toFilter, Prod.exists
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ_1 : Type u_5
F : CFilter.{u_1, u_5} (Set α) σ_1
σ_2 : Type u_6
F_1 : CFilter.{u_1, u_6} (Set α) σ_2
mk :
  ∀ (s : Set α),
    s ∈
        { sets := {a : Set α | ∃ (a_1 : σ_1) (b : σ_2), F.f a_1 ∩ F_1.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯,
          inter_sets := ⋯ : Filter α } ↔
      s ∈
        { sets := {a : Set α | ∃ (b : σ_1), F.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ :
            Filter α } ⊓
          { sets := {a : Set α | ∃ (b : σ_2), F_1.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ :
            Filter α }
⊢ { sets := {a : Set α | ∃ (a_1 : σ_1) (b : σ_2), F.f a_1 ∩ F_1.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯,
      inter_sets := ⋯ : Filter α } =
    { sets := {a : Set α | ∃ (b : σ_1), F.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } ⊓
      { sets := {a : Set α | ∃ (b : σ_2), F_1.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

Tactic:
ext
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ_1 : Type u_5
F : CFilter.{u_1, u_5} (Set α) σ_1
σ_2 : Type u_6
F_1 : CFilter.{u_1, u_6} (Set α) σ_2
s : Set α
mk :
  s ∈
      { sets := {a : Set α | ∃ (a_1 : σ_1) (b : σ_2), F.f a_1 ∩ F_1.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯,
        inter_sets := ⋯ : Filter α } →
    s ∈
      { sets := {a : Set α | ∃ (b : σ_1), F.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ :
          Filter α } ⊓
        { sets := {a : Set α | ∃ (b : σ_2), F_1.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ :
          Filter α }
mk₁ :
  s ∈
      { sets := {a : Set α | ∃ (b : σ_1), F.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ :
          Filter α } ⊓
        { sets := {a : Set α | ∃ (b : σ_2), F_1.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ :
          Filter α } →
    s ∈
      { sets := {a : Set α | ∃ (a_1 : σ_1) (b : σ_2), F.f a_1 ∩ F_1.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯,
        inter_sets := ⋯ : Filter α }
⊢ s ∈
      { sets := {a : Set α | ∃ (a_1 : σ_1) (b : σ_2), F.f a_1 ∩ F_1.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯,
        inter_sets := ⋯ : Filter α } ↔
    s ∈
      { sets := {a : Set α | ∃ (b : σ_1), F.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ :
          Filter α } ⊓
        { sets := {a : Set α | ∃ (b : σ_2), F_1.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ :
          Filter α }

Tactic:
constructor
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ_1 : Type u_5
F : CFilter.{u_1, u_5} (Set α) σ_1
σ_2 : Type u_6
F_1 : CFilter.{u_1, u_6} (Set α) σ_2
s_1 : Set α
s : σ_1
t : σ_2
h : F.f s ∩ F_1.f t ⊆ s_1
apply :
  F.f s ∈
    { sets := {a : Set α | ∃ (b : σ_1), F.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ : Filter α }
apply₁ :
  F_1.f t ∈
    { sets := {a : Set α | ∃ (b : σ_2), F_1.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ :
      Filter α }
⊢ s_1 ∈
    { sets := {a : Set α | ∃ (b : σ_1), F.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ :
        Filter α } ⊓
      { sets := {a : Set α | ∃ (b : σ_2), F_1.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ :
        Filter α }

Tactic:
apply mem_inf_of_inter _ _ h

Premises used: Filter.mem_inf_of_inter
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ_1 : Type u_5
F : CFilter.{u_1, u_5} (Set α) σ_1
σ_2 : Type u_6
F_1 : CFilter.{u_1, u_6} (Set α) σ_2
s_1 : Set α
s : σ_1
t : σ_2
h : F.f s ∩ F_1.f t ⊆ s_1
w : σ_1
h₁ : F.f s ⊆ F.f s
⊢ F.f s ∈
    { sets := {a : Set α | ∃ (b : σ_1), F.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ : Filter α }

Tactic:
use s
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ_1 : Type u_5
F : CFilter.{u_1, u_5} (Set α) σ_1
σ_2 : Type u_6
F_1 : CFilter.{u_1, u_6} (Set α) σ_2
s_1 : Set α
s : σ_1
t : σ_2
h : F.f s ∩ F_1.f t ⊆ s_1
w : σ_2
h₁ : F_1.f t ⊆ F_1.f t
⊢ F_1.f t ∈
    { sets := {a : Set α | ∃ (b : σ_2), F_1.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ :
      Filter α }

Tactic:
use t
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ_1 : Type u_5
F : CFilter.{u_1, u_5} (Set α) σ_1
σ_2 : Type u_6
F_1 : CFilter.{u_1, u_6} (Set α) σ_2
w : Set α
a : σ_1
ha : F.f a ⊆ w
w_1 : Set α
b : σ_2
hb : F_1.f b ⊆ w_1
⊢ w ∩ w_1 ∈
    { sets := {a : Set α | ∃ (a_1 : σ_1) (b : σ_2), F.f a_1 ∩ F_1.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯,
      inter_sets := ⋯ : Filter α }

Tactic:
⟨a, b, inter_subset_inter ha hb⟩

Premises used: Set.Mem, setOf, Set.inter_subset_inter, Exists.intro
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ_1 : Type u_5
F : CFilter.{u_1, u_5} (Set α) σ_1
σ_2 : Type u_6
F_1 : CFilter.{u_1, u_6} (Set α) σ_2
w : Set α
a : σ_1
ha : F.f a ⊆ w
w_1 : Set α
b : σ_2
hb : F_1.f b ⊆ w_1
⊢ w ∩ w_1 ∈
    { sets := {a : Set α | ∃ (a_1 : σ_1) (b : σ_2), F.f a_1 ∩ F_1.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯,
      inter_sets := ⋯ : Filter α }

Tactic:
exact ⟨a, b, inter_subset_inter ha hb⟩
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst : DecidableEq α
x : Set α
h : Membership.mem (γ := Set (Set α)) (sets cofinite) x
⊢ CFilter.f
      { f := fun (s : Finset α) ↦ {a : α | a ∉ s}, pt := ∅, inf := fun (x1 x2 : Finset α) ↦ x1 ∪ x2, inf_le_left := ⋯,
        inf_le_right := ⋯ }
      (Finite.toFinset (s := xᶜ) h) ⊆
    x

Tactic:
simp
-- Module: Mathlib.Data.Analysis.Filter
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f_1 : Filter α
m : α → Filter β
F : Realizer.{u_1, u_5} f_1
G : (i : α) → Realizer.{u_2, u_6} (m i)
x : (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ)
s : F.σ
f : (i : α) → i ∈ F.F.f s → (G i).σ
i : α
h : i ∈ F.F.f s
⊢ i ∈ F.F.f s

Tactic:
assumption
-- 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 x_1 : (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ)
x_2 : β
simp :
  ∀ (x_3 : α)
    (x_4 :
      x_3 ∈
        F.F.f
          (F.F.inf (x.fst (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ))
            (x_1.fst (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ))))
    (h :
      x_2 ∈
        (G x_3).F.f
          ((G x_3).F.inf (x.snd (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ) x_3 ⋯)
            (x_1.snd (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ) x_3 ⋯))),
    ∃ (i : α) (i_1 : i ∈ F.F.f (x.fst (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ))),
      x_2 ∈ (G i).F.f (x.snd (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ) i i_1)
⊢ Membership.mem (γ := Set β)
      (match (motive := (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ) → Set β)
          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 ⋯) with
        | ⟨s, f_1⟩ => ⋃ (i : α), ⋃ (h : i ∈ F.F.f s), (G i).F.f (f_1 i h) :
        Set β)
      x_2 →
    Membership.mem (γ := Set β)
      (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) :
        Set β)
      x_2

Tactic:
simp only [mem_iUnion, forall_exists_index]

Premises used: Set.mem_iUnion, forall_exists_index
-- 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 x_1 : (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ)
x_2 : β
⊢ ∀ (x_3 : α)
    (x_4 :
      x_3 ∈
        F.F.f
          (F.F.inf (x.fst (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ))
            (x_1.fst (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ))))
    (h :
      x_2 ∈
        (G x_3).F.f
          ((G x_3).F.inf (x.snd (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ) x_3 ⋯)
            (x_1.snd (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ) x_3 ⋯))),
    ∃ (i : α) (i_1 : i ∈ F.F.f (x.fst (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ))),
      x_2 ∈ (G i).F.f (x.snd (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ) i i_1)

Tactic:
fun i h₁ h₂ ↦ ⟨i, F.F.inf_le_left _ _ h₁, (G i).F.inf_le_left _ _ h₂⟩

Premises used: Iff.mpr, CFilter.inf, Iff.of_eq, Membership.mem, Sigma.fst, Filter.Realizer.F, Exists.intro, Eq.refl, CFilter.inf_le_left, Sigma.snd, CFilter.inf_le_right, CFilter.f
-- 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 x_1 : (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ)
x_2 : β
⊢ ∀ (x_3 : α)
    (x_4 :
      x_3 ∈
        F.F.f
          (F.F.inf (x.fst (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ))
            (x_1.fst (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ))))
    (h :
      x_2 ∈
        (G x_3).F.f
          ((G x_3).F.inf (x.snd (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ) x_3 ⋯)
            (x_1.snd (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ) x_3 ⋯))),
    ∃ (i : α) (i_1 : i ∈ F.F.f (x.fst (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ))),
      x_2 ∈ (G i).F.f (x.snd (β := fun (s : F.σ) ↦ (i : α) → i ∈ F.F.f s → (G i).σ) i i_1)

Tactic:
exact fun i h₁ h₂ ↦ ⟨i, F.F.inf_le_left _ _ h₁, (G i).F.inf_le_left _ _ h₂⟩