[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : PartialOrder α
F : CFilter α σ
E : σ ≃ τ
f : σ → α
p : σ
g : σ → σ → σ
h₁ : ∀ (a b : σ), f (g a b) ≤ f a
h₂ : ∀ (a b : σ), f (g a b) ≤ f b
a b : τ
⊢ (fun a => f (↑E.symm a)) ((fun a b => ↑E (g (↑E.symm a) (↑E.symm b))) a b) ≤ (fun a => f (↑E.symm a)) a
[PROOFSTEP]
simpa using h₁ (E.symm a) (E.symm b)
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : PartialOrder α
F : CFilter α σ
E : σ ≃ τ
f : σ → α
p : σ
g : σ → σ → σ
h₁ : ∀ (a b : σ), f (g a b) ≤ f a
h₂ : ∀ (a b : σ), f (g a b) ≤ f b
a b : τ
⊢ (fun a => f (↑E.symm a)) ((fun a b => ↑E (g (↑E.symm a) (↑E.symm b))) a b) ≤ (fun a => f (↑E.symm a)) b
[PROOFSTEP]
simpa using h₂ (E.symm a) (E.symm b)
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : PartialOrder α
F✝ : CFilter α σ
E : σ ≃ τ
F : CFilter α σ
a : τ
⊢ f (ofEquiv E F) a = f F (↑E.symm a)
[PROOFSTEP]
cases F
[GOAL]
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : PartialOrder α
F : CFilter α σ
E : σ ≃ τ
a : τ
f✝ : σ → α
pt✝ : σ
inf✝ : σ → σ → σ
inf_le_left✝ : ∀ (a b : σ), f✝ (inf✝ a b) ≤ f✝ a
inf_le_right✝ : ∀ (a b : σ), f✝ (inf✝ a b) ≤ f✝ b
⊢ f (ofEquiv E { f := f✝, pt := pt✝, inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝ }) a =
    f { f := f✝, pt := pt✝, inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝ } (↑E.symm a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : Realizer f
a : Set α
⊢ a ∈ f ↔ ∃ b, CFilter.f F.F b ⊆ a
[PROOFSTEP]
cases F
[GOAL]
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
a : Set α
σ✝ : Type u_5
F✝ : CFilter (Set α) σ✝
eq✝ : CFilter.toFilter F✝ = f
⊢ a ∈ f ↔ ∃ b, CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F b ⊆ a
[PROOFSTEP]
subst f
[GOAL]
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
a : Set α
σ✝ : Type u_5
F✝ : CFilter (Set α) σ✝
⊢ a ∈ CFilter.toFilter F✝ ↔
    ∃ b, CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F b ⊆ a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
x✝ : Set α
⊢ x✝ ∈
      (CFilter.toFilter
          { f := Subtype.val, pt := { val := univ, property := (_ : univ ∈ f) },
            inf := fun x x_1 =>
              match x with
              | { val := val, property := h₁ } =>
                match x_1 with
                | { val := val_1, property := h₂ } => { val := val ∩ val_1, property := (_ : val ∩ val_1 ∈ f) },
            inf_le_left :=
              (_ :
                ∀ (x x_1 : ↑f.sets),
                  ↑((fun x x_2 =>
                          match x with
                          | { val := val, property := h₁ } =>
                            match x_2 with
                            | { val := val_1, property := h₂ } =>
                              { val := val ∩ val_1, property := (_ : val ∩ val_1 ∈ f) })
                        x x_1) ≤
                    ↑x),
            inf_le_right :=
              (_ :
                ∀ (x x_1 : ↑f.sets),
                  ↑((fun x x_2 =>
                          match x with
                          | { val := val, property := h₁ } =>
                            match x_2 with
                            | { val := val_1, property := h₂ } =>
                              { val := val ∩ val_1, property := (_ : val ∩ val_1 ∈ f) })
                        x x_1) ≤
                    ↑x_1) }).sets ↔
    x✝ ∈ f.sets
[PROOFSTEP]
simp [exists_mem_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : Realizer f
E : F.σ ≃ τ
⊢ CFilter.toFilter (CFilter.ofEquiv E F.F) = f
[PROOFSTEP]
refine' Eq.trans _ F.eq
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : Realizer f
E : F.σ ≃ τ
⊢ CFilter.toFilter (CFilter.ofEquiv E F.F) = CFilter.toFilter F.F
[PROOFSTEP]
exact filter_eq (Set.ext fun _ ↦ ⟨fun ⟨s, h⟩ ↦ ⟨E.symm s, by simpa using h⟩, fun ⟨t, h⟩ ↦ ⟨E t, by simp [h]⟩⟩)
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : Realizer f
E : F.σ ≃ τ
x✝¹ : Set α
x✝ : x✝¹ ∈ (CFilter.toFilter (CFilter.ofEquiv E F.F)).sets
s : τ
h : CFilter.f (CFilter.ofEquiv E F.F) s ⊆ x✝¹
⊢ CFilter.f F.F (↑E.symm s) ⊆ x✝¹
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : Realizer f
E : F.σ ≃ τ
x✝¹ : Set α
x✝ : x✝¹ ∈ (CFilter.toFilter F.F).sets
t : F.σ
h : CFilter.f F.F t ⊆ x✝¹
⊢ CFilter.f (CFilter.ofEquiv E F.F) (↑E t) ⊆ x✝¹
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter α
F : Realizer f
x✝ : Set β
⊢ x✝ ∈
      (CFilter.toFilter
          { f := fun s => m '' CFilter.f F.F s, pt := F.F.pt, inf := F.F.inf,
            inf_le_left := (_ : ∀ (x x_1 : F.σ), m '' CFilter.f F.F (CFilter.inf F.F x x_1) ⊆ m '' CFilter.f F.F x),
            inf_le_right :=
              (_ : ∀ (x x_1 : F.σ), m '' CFilter.f F.F (CFilter.inf F.F x x_1) ⊆ m '' CFilter.f F.F x_1) }).sets ↔
    x✝ ∈ (map m f).sets
[PROOFSTEP]
simp only [CFilter.toFilter, image_subset_iff, mem_setOf_eq, Filter.mem_sets, mem_map]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter α
F : Realizer f
x✝ : Set β
⊢ (∃ b, CFilter.f F.F b ⊆ m ⁻¹' x✝) ↔ m ⁻¹' x✝ ∈ f
[PROOFSTEP]
rw [F.mem_sets]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter β
F : Realizer f
x✝ : Set α
⊢ x✝ ∈
      (CFilter.toFilter
          { f := fun s => m ⁻¹' CFilter.f F.F s, pt := F.F.pt, inf := F.F.inf,
            inf_le_left := (_ : ∀ (x x_1 : F.σ), m ⁻¹' CFilter.f F.F (CFilter.inf F.F x x_1) ⊆ m ⁻¹' CFilter.f F.F x),
            inf_le_right :=
              (_ : ∀ (x x_1 : F.σ), m ⁻¹' CFilter.f F.F (CFilter.inf F.F x x_1) ⊆ m ⁻¹' CFilter.f F.F x_1) }).sets ↔
    x✝ ∈ (comap m f).sets
[PROOFSTEP]
cases F
[GOAL]
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter β
x✝ : Set α
σ✝ : Type ?u.20076
F✝ : CFilter (Set β) σ✝
eq✝ : CFilter.toFilter F✝ = f
⊢ x✝ ∈
      (CFilter.toFilter
          { f := fun s => m ⁻¹' CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F s,
            pt := { σ := σ✝, F := F✝, eq := eq✝ }.F.pt, inf := { σ := σ✝, F := F✝, eq := eq✝ }.F.inf,
            inf_le_left :=
              (_ :
                ∀ (x x_1 : { σ := σ✝, F := F✝, eq := eq✝ }.σ),
                  m ⁻¹'
                      CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F
                        (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F x x_1) ⊆
                    m ⁻¹' CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F x),
            inf_le_right :=
              (_ :
                ∀ (x x_1 : { σ := σ✝, F := F✝, eq := eq✝ }.σ),
                  m ⁻¹'
                      CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F
                        (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F x x_1) ⊆
                    m ⁻¹' CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F x_1) }).sets ↔
    x✝ ∈ (comap m f).sets
[PROOFSTEP]
subst f
[GOAL]
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
x✝ : Set α
σ✝ : Type ?u.20076
F✝ : CFilter (Set β) σ✝
⊢ x✝ ∈
      (CFilter.toFilter
          {
            f := fun s =>
              m ⁻¹' CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F s,
            pt := { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F.pt,
            inf := { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F.inf,
            inf_le_left :=
              (_ :
                ∀ (x x_1 : { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.σ),
                  m ⁻¹'
                      CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F
                        (CFilter.inf { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F x
                          x_1) ⊆
                    m ⁻¹' CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F x),
            inf_le_right :=
              (_ :
                ∀ (x x_1 : { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.σ),
                  m ⁻¹'
                      CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F
                        (CFilter.inf { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F x
                          x_1) ⊆
                    m ⁻¹'
                      CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F
                        x_1) }).sets ↔
    x✝ ∈ (comap m (CFilter.toFilter F✝)).sets
[PROOFSTEP]
exact ⟨fun ⟨s, h⟩ ↦ ⟨_, ⟨s, Subset.refl _⟩, h⟩, fun ⟨_, ⟨s, h⟩, h₂⟩ ↦ ⟨s, Subset.trans (preimage_mono h) h₂⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
F : Realizer f
G : Realizer g
x✝ : Set α
⊢ x✝ ∈
      (CFilter.toFilter
          {
            f := fun x =>
              match x with
              | (s, t) => CFilter.f F.F s ∪ CFilter.f G.F t,
            pt := (F.F.pt, G.F.pt),
            inf := fun x x_1 =>
              match x with
              | (a, a') =>
                match x_1 with
                | (b, b') => (CFilter.inf F.F a b, CFilter.inf G.F a' b'),
            inf_le_left :=
              (_ :
                ∀ (x x_1 : F.σ × G.σ),
                  CFilter.f F.F (CFilter.inf F.F x.fst x_1.fst) ∪ CFilter.f G.F (CFilter.inf G.F x.snd x_1.snd) ⊆
                    CFilter.f F.F x.fst ∪ CFilter.f G.F x.snd),
            inf_le_right :=
              (_ :
                ∀ (x x_1 : F.σ × G.σ),
                  CFilter.f F.F (CFilter.inf F.F x.fst x_1.fst) ∪ CFilter.f G.F (CFilter.inf G.F x.snd x_1.snd) ⊆
                    CFilter.f F.F x_1.fst ∪ CFilter.f G.F x_1.snd) }).sets ↔
    x✝ ∈ (f ⊔ g).sets
[PROOFSTEP]
cases F
[GOAL]
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
G : Realizer g
x✝ : Set α
σ✝ : Type ?u.22357
F✝ : CFilter (Set α) σ✝
eq✝ : CFilter.toFilter F✝ = f
⊢ x✝ ∈
      (CFilter.toFilter
          {
            f := fun x =>
              match x with
              | (s, t) => CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F s ∪ CFilter.f G.F t,
            pt := ({ σ := σ✝, F := F✝, eq := eq✝ }.F.pt, G.F.pt),
            inf := fun x x_1 =>
              match x with
              | (a, a') =>
                match x_1 with
                | (b, b') => (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F a b, CFilter.inf G.F a' b'),
            inf_le_left :=
              (_ :
                ∀ (x x_1 : { σ := σ✝, F := F✝, eq := eq✝ }.σ × G.σ),
                  CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F
                        (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F x.fst x_1.fst) ∪
                      CFilter.f G.F (CFilter.inf G.F x.snd x_1.snd) ⊆
                    CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F x.fst ∪ CFilter.f G.F x.snd),
            inf_le_right :=
              (_ :
                ∀ (x x_1 : { σ := σ✝, F := F✝, eq := eq✝ }.σ × G.σ),
                  CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F
                        (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F x.fst x_1.fst) ∪
                      CFilter.f G.F (CFilter.inf G.F x.snd x_1.snd) ⊆
                    CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F x_1.fst ∪ CFilter.f G.F x_1.snd) }).sets ↔
    x✝ ∈ (f ⊔ g).sets
[PROOFSTEP]
cases G
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
x✝ : Set α
σ✝¹ : Type ?u.22357
F✝¹ : CFilter (Set α) σ✝¹
eq✝¹ : CFilter.toFilter F✝¹ = f
σ✝ : Type ?u.22412
F✝ : CFilter (Set α) σ✝
eq✝ : CFilter.toFilter F✝ = g
⊢ x✝ ∈
      (CFilter.toFilter
          {
            f := fun x =>
              match x with
              | (s, t) =>
                CFilter.f { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F s ∪ CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F t,
            pt := ({ σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F.pt, { σ := σ✝, F := F✝, eq := eq✝ }.F.pt),
            inf := fun x x_1 =>
              match x with
              | (a, a') =>
                match x_1 with
                | (b, b') =>
                  (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F a b,
                    CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F a' b'),
            inf_le_left :=
              (_ :
                ∀ (x x_1 : { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.σ × { σ := σ✝, F := F✝, eq := eq✝ }.σ),
                  CFilter.f { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F
                        (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F x.fst x_1.fst) ∪
                      CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F
                        (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F x.snd x_1.snd) ⊆
                    CFilter.f { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F x.fst ∪
                      CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F x.snd),
            inf_le_right :=
              (_ :
                ∀ (x x_1 : { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.σ × { σ := σ✝, F := F✝, eq := eq✝ }.σ),
                  CFilter.f { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F
                        (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F x.fst x_1.fst) ∪
                      CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F
                        (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F x.snd x_1.snd) ⊆
                    CFilter.f { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F x_1.fst ∪
                      CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F x_1.snd) }).sets ↔
    x✝ ∈ (f ⊔ g).sets
[PROOFSTEP]
substs f g
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
x✝ : Set α
σ✝¹ : Type ?u.22357
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.22412
F✝ : CFilter (Set α) σ✝
⊢ x✝ ∈
      (CFilter.toFilter
          {
            f := fun x =>
              match x with
              | (s, t) =>
                CFilter.f { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F s ∪
                  CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F t,
            pt :=
              ({ σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F.pt,
                { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F.pt),
            inf := fun x x_1 =>
              match x with
              | (a, a') =>
                match x_1 with
                | (b, b') =>
                  (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F a b,
                    CFilter.inf { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F a' b'),
            inf_le_left :=
              (_ :
                ∀
                  (x x_1 :
                    { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.σ ×
                      { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.σ),
                  CFilter.f { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F
                        (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F
                          x.fst x_1.fst) ∪
                      CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F
                        (CFilter.inf { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F x.snd
                          x_1.snd) ⊆
                    CFilter.f { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F x.fst ∪
                      CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F x.snd),
            inf_le_right :=
              (_ :
                ∀
                  (x x_1 :
                    { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.σ ×
                      { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.σ),
                  CFilter.f { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F
                        (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F
                          x.fst x_1.fst) ∪
                      CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F
                        (CFilter.inf { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F x.snd
                          x_1.snd) ⊆
                    CFilter.f { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F
                        x_1.fst ∪
                      CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F
                        x_1.snd) }).sets ↔
    x✝ ∈ (CFilter.toFilter F✝¹ ⊔ CFilter.toFilter F✝).sets
[PROOFSTEP]
simp [CFilter.toFilter]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
F : Realizer f
G : Realizer g
⊢ CFilter.toFilter
      {
        f := fun x =>
          match x with
          | (s, t) => CFilter.f F.F s ∩ CFilter.f G.F t,
        pt := (F.F.pt, G.F.pt),
        inf := fun x x_1 =>
          match x with
          | (a, a') =>
            match x_1 with
            | (b, b') => (CFilter.inf F.F a b, CFilter.inf G.F a' b'),
        inf_le_left :=
          (_ :
            ∀ (x x_1 : F.σ × G.σ),
              CFilter.f F.F (CFilter.inf F.F x.fst x_1.fst) ∩ CFilter.f G.F (CFilter.inf G.F x.snd x_1.snd) ⊆
                CFilter.f F.F x.fst ∩ CFilter.f G.F x.snd),
        inf_le_right :=
          (_ :
            ∀ (x x_1 : F.σ × G.σ),
              CFilter.f F.F (CFilter.inf F.F x.fst x_1.fst) ∩ CFilter.f G.F (CFilter.inf G.F x.snd x_1.snd) ⊆
                CFilter.f F.F x_1.fst ∩ CFilter.f G.F x_1.snd) } =
    f ⊓ g
[PROOFSTEP]
cases F
[GOAL]
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
G : Realizer g
σ✝ : Type ?u.34651
F✝ : CFilter (Set α) σ✝
eq✝ : CFilter.toFilter F✝ = f
⊢ CFilter.toFilter
      {
        f := fun x =>
          match x with
          | (s, t) => CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F s ∩ CFilter.f G.F t,
        pt := ({ σ := σ✝, F := F✝, eq := eq✝ }.F.pt, G.F.pt),
        inf := fun x x_1 =>
          match x with
          | (a, a') =>
            match x_1 with
            | (b, b') => (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F a b, CFilter.inf G.F a' b'),
        inf_le_left :=
          (_ :
            ∀ (x x_1 : { σ := σ✝, F := F✝, eq := eq✝ }.σ × G.σ),
              CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F
                    (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F x.fst x_1.fst) ∩
                  CFilter.f G.F (CFilter.inf G.F x.snd x_1.snd) ⊆
                CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F x.fst ∩ CFilter.f G.F x.snd),
        inf_le_right :=
          (_ :
            ∀ (x x_1 : { σ := σ✝, F := F✝, eq := eq✝ }.σ × G.σ),
              CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F
                    (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F x.fst x_1.fst) ∩
                  CFilter.f G.F (CFilter.inf G.F x.snd x_1.snd) ⊆
                CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F x_1.fst ∩ CFilter.f G.F x_1.snd) } =
    f ⊓ g
[PROOFSTEP]
cases G
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
σ✝¹ : Type ?u.34651
F✝¹ : CFilter (Set α) σ✝¹
eq✝¹ : CFilter.toFilter F✝¹ = f
σ✝ : Type ?u.34706
F✝ : CFilter (Set α) σ✝
eq✝ : CFilter.toFilter F✝ = g
⊢ CFilter.toFilter
      {
        f := fun x =>
          match x with
          | (s, t) => CFilter.f { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F s ∩ CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F t,
        pt := ({ σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F.pt, { σ := σ✝, F := F✝, eq := eq✝ }.F.pt),
        inf := fun x x_1 =>
          match x with
          | (a, a') =>
            match x_1 with
            | (b, b') =>
              (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F a b,
                CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F a' b'),
        inf_le_left :=
          (_ :
            ∀ (x x_1 : { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.σ × { σ := σ✝, F := F✝, eq := eq✝ }.σ),
              CFilter.f { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F
                    (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F x.fst x_1.fst) ∩
                  CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F
                    (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F x.snd x_1.snd) ⊆
                CFilter.f { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F x.fst ∩
                  CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F x.snd),
        inf_le_right :=
          (_ :
            ∀ (x x_1 : { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.σ × { σ := σ✝, F := F✝, eq := eq✝ }.σ),
              CFilter.f { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F
                    (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F x.fst x_1.fst) ∩
                  CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F
                    (CFilter.inf { σ := σ✝, F := F✝, eq := eq✝ }.F x.snd x_1.snd) ⊆
                CFilter.f { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F x_1.fst ∩
                  CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F x_1.snd) } =
    f ⊓ g
[PROOFSTEP]
substs f g
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.34651
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.34706
F✝ : CFilter (Set α) σ✝
⊢ CFilter.toFilter
      {
        f := fun x =>
          match x with
          | (s, t) =>
            CFilter.f { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F s ∩
              CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F t,
        pt :=
          ({ σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F.pt,
            { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F.pt),
        inf := fun x x_1 =>
          match x with
          | (a, a') =>
            match x_1 with
            | (b, b') =>
              (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F a b,
                CFilter.inf { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F a' b'),
        inf_le_left :=
          (_ :
            ∀
              (x x_1 :
                { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.σ ×
                  { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.σ),
              CFilter.f { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F
                    (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F x.fst
                      x_1.fst) ∩
                  CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F
                    (CFilter.inf { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F x.snd
                      x_1.snd) ⊆
                CFilter.f { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F x.fst ∩
                  CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F x.snd),
        inf_le_right :=
          (_ :
            ∀
              (x x_1 :
                { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.σ ×
                  { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.σ),
              CFilter.f { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F
                    (CFilter.inf { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F x.fst
                      x_1.fst) ∩
                  CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F
                    (CFilter.inf { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F x.snd
                      x_1.snd) ⊆
                CFilter.f { σ := σ✝¹, F := F✝¹, eq := (_ : CFilter.toFilter F✝¹ = CFilter.toFilter F✝¹) }.F x_1.fst ∩
                  CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F x_1.snd) } =
    CFilter.toFilter F✝¹ ⊓ CFilter.toFilter F✝
[PROOFSTEP]
simp only [CFilter.toFilter, Prod.exists]
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.34651
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.34706
F✝ : CFilter (Set α) σ✝
⊢ { sets := {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a},
      univ_sets := (_ : univ ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}),
      sets_of_superset :=
        (_ :
          ∀ {x y : Set α},
            x ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
              x ⊆ y → y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}),
      inter_sets :=
        (_ :
          ∀ {x y : Set α},
            x ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
              y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
                x ∩ y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}) } =
    { sets := {a | ∃ b, CFilter.f F✝¹ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝¹ b ⊆ univ),
        sets_of_superset :=
          (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}),
        inter_sets :=
          (_ :
            ∀ {x y : Set α},
              x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} →
                y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}) } ⊓
      { sets := {a | ∃ b, CFilter.f F✝ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝ b ⊆ univ),
        sets_of_superset :=
          (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}),
        inter_sets :=
          (_ :
            ∀ {x y : Set α},
              x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} →
                y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}) }
[PROOFSTEP]
ext
[GOAL]
case mk.mk.a
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.34651
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.34706
F✝ : CFilter (Set α) σ✝
s✝ : Set α
⊢ s✝ ∈
      { sets := {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a},
        univ_sets := (_ : univ ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}),
        sets_of_superset :=
          (_ :
            ∀ {x y : Set α},
              x ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
                x ⊆ y → y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}),
        inter_sets :=
          (_ :
            ∀ {x y : Set α},
              x ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
                y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
                  x ∩ y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}) } ↔
    s✝ ∈
      { sets := {a | ∃ b, CFilter.f F✝¹ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝¹ b ⊆ univ),
          sets_of_superset :=
            (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}),
          inter_sets :=
            (_ :
              ∀ {x y : Set α},
                x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} →
                  y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}) } ⊓
        { sets := {a | ∃ b, CFilter.f F✝ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝ b ⊆ univ),
          sets_of_superset :=
            (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}),
          inter_sets :=
            (_ :
              ∀ {x y : Set α},
                x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} →
                  y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}) }
[PROOFSTEP]
constructor
[GOAL]
case mk.mk.a.mp
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.34651
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.34706
F✝ : CFilter (Set α) σ✝
s✝ : Set α
⊢ s✝ ∈
      { sets := {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a},
        univ_sets := (_ : univ ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}),
        sets_of_superset :=
          (_ :
            ∀ {x y : Set α},
              x ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
                x ⊆ y → y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}),
        inter_sets :=
          (_ :
            ∀ {x y : Set α},
              x ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
                y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
                  x ∩ y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}) } →
    s✝ ∈
      { sets := {a | ∃ b, CFilter.f F✝¹ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝¹ b ⊆ univ),
          sets_of_superset :=
            (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}),
          inter_sets :=
            (_ :
              ∀ {x y : Set α},
                x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} →
                  y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}) } ⊓
        { sets := {a | ∃ b, CFilter.f F✝ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝ b ⊆ univ),
          sets_of_superset :=
            (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}),
          inter_sets :=
            (_ :
              ∀ {x y : Set α},
                x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} →
                  y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}) }
[PROOFSTEP]
rintro ⟨s, t, h⟩
[GOAL]
case mk.mk.a.mp.intro.intro
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.34651
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.34706
F✝ : CFilter (Set α) σ✝
s✝ : Set α
s : σ✝¹
t : σ✝
h : CFilter.f F✝¹ s ∩ CFilter.f F✝ t ⊆ s✝
⊢ s✝ ∈
    { sets := {a | ∃ b, CFilter.f F✝¹ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝¹ b ⊆ univ),
        sets_of_superset :=
          (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}),
        inter_sets :=
          (_ :
            ∀ {x y : Set α},
              x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} →
                y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}) } ⊓
      { sets := {a | ∃ b, CFilter.f F✝ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝ b ⊆ univ),
        sets_of_superset :=
          (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}),
        inter_sets :=
          (_ :
            ∀ {x y : Set α},
              x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} →
                y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}) }
[PROOFSTEP]
apply mem_inf_of_inter _ _ h
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.34651
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.34706
F✝ : CFilter (Set α) σ✝
s✝ : Set α
s : σ✝¹
t : σ✝
h : CFilter.f F✝¹ s ∩ CFilter.f F✝ t ⊆ s✝
⊢ CFilter.f F✝¹ s ∈
    { sets := {a | ∃ b, CFilter.f F✝¹ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝¹ b ⊆ univ),
      sets_of_superset :=
        (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}),
      inter_sets :=
        (_ :
          ∀ {x y : Set α},
            x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} →
              y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}) }
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.34651
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.34706
F✝ : CFilter (Set α) σ✝
s✝ : Set α
s : σ✝¹
t : σ✝
h : CFilter.f F✝¹ s ∩ CFilter.f F✝ t ⊆ s✝
⊢ CFilter.f F✝ t ∈
    { sets := {a | ∃ b, CFilter.f F✝ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝ b ⊆ univ),
      sets_of_superset :=
        (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}),
      inter_sets :=
        (_ :
          ∀ {x y : Set α},
            x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} →
              y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}) }
[PROOFSTEP]
use s
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.34651
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.34706
F✝ : CFilter (Set α) σ✝
s✝ : Set α
s : σ✝¹
t : σ✝
h : CFilter.f F✝¹ s ∩ CFilter.f F✝ t ⊆ s✝
⊢ CFilter.f F✝ t ∈
    { sets := {a | ∃ b, CFilter.f F✝ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝ b ⊆ univ),
      sets_of_superset :=
        (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}),
      inter_sets :=
        (_ :
          ∀ {x y : Set α},
            x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} →
              y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}) }
[PROOFSTEP]
use t
[GOAL]
case mk.mk.a.mpr
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.34651
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.34706
F✝ : CFilter (Set α) σ✝
s✝ : Set α
⊢ s✝ ∈
      { sets := {a | ∃ b, CFilter.f F✝¹ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝¹ b ⊆ univ),
          sets_of_superset :=
            (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}),
          inter_sets :=
            (_ :
              ∀ {x y : Set α},
                x ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} →
                  y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝¹ b ⊆ a}) } ⊓
        { sets := {a | ∃ b, CFilter.f F✝ b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F✝ b ⊆ univ),
          sets_of_superset :=
            (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}),
          inter_sets :=
            (_ :
              ∀ {x y : Set α},
                x ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} →
                  y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F✝ b ⊆ a}) } →
    s✝ ∈
      { sets := {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a},
        univ_sets := (_ : univ ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}),
        sets_of_superset :=
          (_ :
            ∀ {x y : Set α},
              x ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
                x ⊆ y → y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}),
        inter_sets :=
          (_ :
            ∀ {x y : Set α},
              x ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
                y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
                  x ∩ y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}) }
[PROOFSTEP]
rintro ⟨_, ⟨a, ha⟩, _, ⟨b, hb⟩, rfl⟩
[GOAL]
case mk.mk.a.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.34651
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.34706
F✝ : CFilter (Set α) σ✝
w✝¹ : Set α
a : σ✝¹
ha : CFilter.f F✝¹ a ⊆ w✝¹
w✝ : Set α
b : σ✝
hb : CFilter.f F✝ b ⊆ w✝
⊢ w✝¹ ∩ w✝ ∈
    { sets := {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a},
      univ_sets := (_ : univ ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}),
      sets_of_superset :=
        (_ :
          ∀ {x y : Set α},
            x ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
              x ⊆ y → y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}),
      inter_sets :=
        (_ :
          ∀ {x y : Set α},
            x ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
              y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a} →
                x ∩ y ∈ {a | ∃ a_1 b, CFilter.f F✝¹ a_1 ∩ CFilter.f F✝ b ⊆ a}) }
[PROOFSTEP]
exact ⟨a, b, inter_subset_inter ha hb⟩
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : DecidableEq α
x✝ : Set α
h : x✝ ∈ cofinite.sets
⊢ CFilter.f
      { f := fun s => {a | ¬a ∈ s}, pt := ∅, inf := fun x x_1 => x ∪ x_1,
        inf_le_left := (_ : ∀ (x x_1 : Finset α) (x_2 : α), ¬x_2 ∈ (fun x x_3 => x ∪ x_3) x x_1 → ¬x_2 ∈ x),
        inf_le_right := (_ : ∀ (x x_1 : Finset α) (x_2 : α), ¬x_2 ∈ (fun x x_3 => x ∪ x_3) x x_1 → ¬x_2 ∈ x_1) }
      (Finite.toFinset h) ⊆
    x✝
[PROOFSTEP]
simp [Subset.rfl]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f✝ : Filter α
m : α → Filter β
F : Realizer f✝
G : (i : α) → Realizer (m i)
x✝ : (s : F.σ) × ((i : α) → i ∈ CFilter.f F.F s → (G i).σ)
s : F.σ
f : (i : α) → i ∈ CFilter.f F.F s → (G i).σ
i : α
h✝ : i ∈ CFilter.f F.F s
⊢ i ∈ CFilter.f F.F s
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
F : Realizer f
G : (i : α) → Realizer (m i)
x✝² x✝¹ : (s : F.σ) × ((i : α) → i ∈ CFilter.f F.F s → (G i).σ)
x✝ : β
⊢ x✝ ∈
      (fun x =>
          match x with
          | { fst := s, snd := f_1 } => ⋃ (i : α) (h : i ∈ CFilter.f F.F s), CFilter.f (G i).F (f_1 i h))
        ((fun x x_1 =>
            match x with
            | { fst := a, snd := f_1 } =>
              match x_1 with
              | { fst := b, snd := f' } =>
                { fst := CFilter.inf F.F a b,
                  snd := fun i h =>
                    CFilter.inf (G i).F (f_1 i (_ : i ∈ CFilter.f F.F a)) (f' i (_ : i ∈ CFilter.f F.F b)) })
          x✝² x✝¹) →
    x✝ ∈
      (fun x =>
          match x with
          | { fst := s, snd := f_1 } => ⋃ (i : α) (h : i ∈ CFilter.f F.F s), CFilter.f (G i).F (f_1 i h))
        x✝²
[PROOFSTEP]
simp only [mem_iUnion, forall_exists_index]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
F : Realizer f
G : (i : α) → Realizer (m i)
x✝² x✝¹ : (s : F.σ) × ((i : α) → i ∈ CFilter.f F.F s → (G i).σ)
x✝ : β
⊢ ∀ (x : α) (x_1 : x ∈ CFilter.f F.F (CFilter.inf F.F x✝².fst x✝¹.fst)),
    x✝ ∈
        CFilter.f (G x).F
          (CFilter.inf (G x).F (Sigma.snd x✝² x (_ : x ∈ CFilter.f F.F x✝².fst))
            (Sigma.snd x✝¹ x (_ : x ∈ CFilter.f F.F x✝¹.fst))) →
      ∃ i i_1, x✝ ∈ CFilter.f (G i).F (Sigma.snd x✝² i i_1)
[PROOFSTEP]
exact fun i h₁ h₂ ↦ ⟨i, F.F.inf_le_left _ _ h₁, (G i).F.inf_le_left _ _ h₂⟩
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
F : Realizer f
G : (i : α) → Realizer (m i)
x✝² x✝¹ : (s : F.σ) × ((i : α) → i ∈ CFilter.f F.F s → (G i).σ)
x✝ : β
⊢ x✝ ∈
      (fun x =>
          match x with
          | { fst := s, snd := f_1 } => ⋃ (i : α) (h : i ∈ CFilter.f F.F s), CFilter.f (G i).F (f_1 i h))
        ((fun x x_1 =>
            match x with
            | { fst := a, snd := f_1 } =>
              match x_1 with
              | { fst := b, snd := f' } =>
                { fst := CFilter.inf F.F a b,
                  snd := fun i h =>
                    CFilter.inf (G i).F (f_1 i (_ : i ∈ CFilter.f F.F a)) (f' i (_ : i ∈ CFilter.f F.F b)) })
          x✝² x✝¹) →
    x✝ ∈
      (fun x =>
          match x with
          | { fst := s, snd := f_1 } => ⋃ (i : α) (h : i ∈ CFilter.f F.F s), CFilter.f (G i).F (f_1 i h))
        x✝¹
[PROOFSTEP]
simp only [mem_iUnion, forall_exists_index]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
F : Realizer f
G : (i : α) → Realizer (m i)
x✝² x✝¹ : (s : F.σ) × ((i : α) → i ∈ CFilter.f F.F s → (G i).σ)
x✝ : β
⊢ ∀ (x : α) (x_1 : x ∈ CFilter.f F.F (CFilter.inf F.F x✝².fst x✝¹.fst)),
    x✝ ∈
        CFilter.f (G x).F
          (CFilter.inf (G x).F (Sigma.snd x✝² x (_ : x ∈ CFilter.f F.F x✝².fst))
            (Sigma.snd x✝¹ x (_ : x ∈ CFilter.f F.F x✝¹.fst))) →
      ∃ i i_1, x✝ ∈ CFilter.f (G i).F (Sigma.snd x✝¹ i i_1)
[PROOFSTEP]
exact fun i h₁ h₂ ↦ ⟨i, F.F.inf_le_right _ _ h₁, (G i).F.inf_le_right _ _ h₂⟩
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
F : Realizer f
G : (i : α) → Realizer (m i)
x✝ : Set β
⊢ x✝ ∈
      (CFilter.toFilter
          {
            f := fun x =>
              match x with
              | { fst := s, snd := f_1 } => ⋃ (i : α) (h : i ∈ CFilter.f F.F s), CFilter.f (G i).F (f_1 i h),
            pt := { fst := F.F.pt, snd := fun i x => (G i).F.pt },
            inf := fun x x_1 =>
              match x with
              | { fst := a, snd := f_1 } =>
                match x_1 with
                | { fst := b, snd := f' } =>
                  { fst := CFilter.inf F.F a b,
                    snd := fun i h =>
                      CFilter.inf (G i).F (f_1 i (_ : i ∈ CFilter.f F.F a)) (f' i (_ : i ∈ CFilter.f F.F b)) },
            inf_le_left :=
              (_ :
                ∀ (x x_1 : (s : F.σ) × ((i : α) → i ∈ CFilter.f F.F s → (G i).σ)) (x_2 : β),
                  x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f_1 } =>
                            ⋃ (i : α) (h : i ∈ CFilter.f F.F s), CFilter.f (G i).F (f_1 i h))
                        ((fun x x_3 =>
                            match x with
                            | { fst := a, snd := f_1 } =>
                              match x_3 with
                              | { fst := b, snd := f' } =>
                                { fst := CFilter.inf F.F a b,
                                  snd := fun i h =>
                                    CFilter.inf (G i).F (f_1 i (_ : i ∈ CFilter.f F.F a))
                                      (f' i (_ : i ∈ CFilter.f F.F b)) })
                          x x_1) →
                    x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f_1 } =>
                            ⋃ (i : α) (h : i ∈ CFilter.f F.F s), CFilter.f (G i).F (f_1 i h))
                        x),
            inf_le_right :=
              (_ :
                ∀ (x x_1 : (s : F.σ) × ((i : α) → i ∈ CFilter.f F.F s → (G i).σ)) (x_2 : β),
                  x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f_1 } =>
                            ⋃ (i : α) (h : i ∈ CFilter.f F.F s), CFilter.f (G i).F (f_1 i h))
                        ((fun x x_3 =>
                            match x with
                            | { fst := a, snd := f_1 } =>
                              match x_3 with
                              | { fst := b, snd := f' } =>
                                { fst := CFilter.inf F.F a b,
                                  snd := fun i h =>
                                    CFilter.inf (G i).F (f_1 i (_ : i ∈ CFilter.f F.F a))
                                      (f' i (_ : i ∈ CFilter.f F.F b)) })
                          x x_1) →
                    x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f_1 } =>
                            ⋃ (i : α) (h : i ∈ CFilter.f F.F s), CFilter.f (G i).F (f_1 i h))
                        x_1) }).sets ↔
    x✝ ∈ (bind f m).sets
[PROOFSTEP]
cases' F with _ F _
[GOAL]
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
G : (i : α) → Realizer (m i)
x✝ : Set β
σ✝ : Type ?u.44096
F : CFilter (Set α) σ✝
eq✝ : CFilter.toFilter F = f
⊢ x✝ ∈
      (CFilter.toFilter
          {
            f := fun x =>
              match x with
              | { fst := s, snd := f_1 } =>
                ⋃ (i : α) (h : i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F s), CFilter.f (G i).F (f_1 i h),
            pt := { fst := { σ := σ✝, F := F, eq := eq✝ }.F.pt, snd := fun i x => (G i).F.pt },
            inf := fun x x_1 =>
              match x with
              | { fst := a, snd := f_1 } =>
                match x_1 with
                | { fst := b, snd := f' } =>
                  { fst := CFilter.inf { σ := σ✝, F := F, eq := eq✝ }.F a b,
                    snd := fun i h =>
                      CFilter.inf (G i).F (f_1 i (_ : i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F a))
                        (f' i (_ : i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F b)) },
            inf_le_left :=
              (_ :
                ∀
                  (x x_1 :
                    (s : { σ := σ✝, F := F, eq := eq✝ }.σ) ×
                      ((i : α) → i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F s → (G i).σ))
                  (x_2 : β),
                  x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f_1 } =>
                            ⋃ (i : α) (h : i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F s),
                              CFilter.f (G i).F (f_1 i h))
                        ((fun x x_3 =>
                            match x with
                            | { fst := a, snd := f_1 } =>
                              match x_3 with
                              | { fst := b, snd := f' } =>
                                { fst := CFilter.inf { σ := σ✝, F := F, eq := eq✝ }.F a b,
                                  snd := fun i h =>
                                    CFilter.inf (G i).F (f_1 i (_ : i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F a))
                                      (f' i (_ : i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F b)) })
                          x x_1) →
                    x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f_1 } =>
                            ⋃ (i : α) (h : i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F s),
                              CFilter.f (G i).F (f_1 i h))
                        x),
            inf_le_right :=
              (_ :
                ∀
                  (x x_1 :
                    (s : { σ := σ✝, F := F, eq := eq✝ }.σ) ×
                      ((i : α) → i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F s → (G i).σ))
                  (x_2 : β),
                  x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f_1 } =>
                            ⋃ (i : α) (h : i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F s),
                              CFilter.f (G i).F (f_1 i h))
                        ((fun x x_3 =>
                            match x with
                            | { fst := a, snd := f_1 } =>
                              match x_3 with
                              | { fst := b, snd := f' } =>
                                { fst := CFilter.inf { σ := σ✝, F := F, eq := eq✝ }.F a b,
                                  snd := fun i h =>
                                    CFilter.inf (G i).F (f_1 i (_ : i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F a))
                                      (f' i (_ : i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F b)) })
                          x x_1) →
                    x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f_1 } =>
                            ⋃ (i : α) (h : i ∈ CFilter.f { σ := σ✝, F := F, eq := eq✝ }.F s),
                              CFilter.f (G i).F (f_1 i h))
                        x_1) }).sets ↔
    x✝ ∈ (bind f m).sets
[PROOFSTEP]
subst f
[GOAL]
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → Filter β
G : (i : α) → Realizer (m i)
x✝ : Set β
σ✝ : Type ?u.44096
F : CFilter (Set α) σ✝
⊢ x✝ ∈
      (CFilter.toFilter
          {
            f := fun x =>
              match x with
              | { fst := s, snd := f } =>
                ⋃ (i : α) (h :
                  i ∈ CFilter.f { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F s),
                  CFilter.f (G i).F (f i h),
            pt :=
              { fst := { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F.pt,
                snd := fun i x => (G i).F.pt },
            inf := fun x x_1 =>
              match x with
              | { fst := a, snd := f } =>
                match x_1 with
                | { fst := b, snd := f' } =>
                  { fst := CFilter.inf { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F a b,
                    snd := fun i h =>
                      CFilter.inf (G i).F
                        (f i
                          (_ :
                            i ∈ CFilter.f { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F a))
                        (f' i
                          (_ :
                            i ∈
                              CFilter.f { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F
                                b)) },
            inf_le_left :=
              (_ :
                ∀
                  (x x_1 :
                    (s : { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.σ) ×
                      ((i : α) →
                        i ∈ CFilter.f { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F s →
                          (G i).σ))
                  (x_2 : β),
                  x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f } =>
                            ⋃ (i : α) (h :
                              i ∈
                                CFilter.f { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F s),
                              CFilter.f (G i).F (f i h))
                        ((fun x x_3 =>
                            match x with
                            | { fst := a, snd := f } =>
                              match x_3 with
                              | { fst := b, snd := f' } =>
                                {
                                  fst :=
                                    CFilter.inf
                                      { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F a b,
                                  snd := fun i h =>
                                    CFilter.inf (G i).F
                                      (f i
                                        (_ :
                                          i ∈
                                            CFilter.f
                                              { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F
                                              a))
                                      (f' i
                                        (_ :
                                          i ∈
                                            CFilter.f
                                              { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F
                                              b)) })
                          x x_1) →
                    x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f } =>
                            ⋃ (i : α) (h :
                              i ∈
                                CFilter.f { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F s),
                              CFilter.f (G i).F (f i h))
                        x),
            inf_le_right :=
              (_ :
                ∀
                  (x x_1 :
                    (s : { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.σ) ×
                      ((i : α) →
                        i ∈ CFilter.f { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F s →
                          (G i).σ))
                  (x_2 : β),
                  x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f } =>
                            ⋃ (i : α) (h :
                              i ∈
                                CFilter.f { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F s),
                              CFilter.f (G i).F (f i h))
                        ((fun x x_3 =>
                            match x with
                            | { fst := a, snd := f } =>
                              match x_3 with
                              | { fst := b, snd := f' } =>
                                {
                                  fst :=
                                    CFilter.inf
                                      { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F a b,
                                  snd := fun i h =>
                                    CFilter.inf (G i).F
                                      (f i
                                        (_ :
                                          i ∈
                                            CFilter.f
                                              { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F
                                              a))
                                      (f' i
                                        (_ :
                                          i ∈
                                            CFilter.f
                                              { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F
                                              b)) })
                          x x_1) →
                    x_2 ∈
                      (fun x =>
                          match x with
                          | { fst := s, snd := f } =>
                            ⋃ (i : α) (h :
                              i ∈
                                CFilter.f { σ := σ✝, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }.F s),
                              CFilter.f (G i).F (f i h))
                        x_1) }).sets ↔
    x✝ ∈ (bind (CFilter.toFilter F) m).sets
[PROOFSTEP]
simp only [CFilter.toFilter, iUnion_subset_iff, Sigma.exists, Filter.mem_sets, mem_bind]
[GOAL]
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → Filter β
G : (i : α) → Realizer (m i)
x✝ : Set β
σ✝ : Type ?u.44096
F : CFilter (Set α) σ✝
⊢ x✝ ∈ {a | ∃ a_1 b, ∀ (i : α) (i_1 : i ∈ CFilter.f F { fst := a_1, snd := b }.fst), CFilter.f (G i).F (b i i_1) ⊆ a} ↔
    ∃ t,
      t ∈
          { sets := {a | ∃ b, CFilter.f F b ⊆ a}, univ_sets := (_ : ∃ b, CFilter.f F b ⊆ univ),
            sets_of_superset :=
              (_ : ∀ {x y : Set α}, x ∈ {a | ∃ b, CFilter.f F b ⊆ a} → x ⊆ y → y ∈ {a | ∃ b, CFilter.f F b ⊆ a}),
            inter_sets :=
              (_ :
                ∀ {x y : Set α},
                  x ∈ {a | ∃ b, CFilter.f F b ⊆ a} →
                    y ∈ {a | ∃ b, CFilter.f F b ⊆ a} → x ∩ y ∈ {a | ∃ b, CFilter.f F b ⊆ a}) } ∧
        ∀ (x : α), x ∈ t → x✝ ∈ m x
[PROOFSTEP]
exact
  ⟨fun ⟨s, f, h⟩ ↦ ⟨F s, ⟨s, Subset.refl _⟩, fun i H ↦ (G i).mem_sets.2 ⟨f i H, fun _ h' ↦ h i H h'⟩⟩,
    fun ⟨_, ⟨s, h⟩, f⟩ ↦
    let ⟨f', h'⟩ := Classical.axiom_of_choice fun i : F s ↦ (G i).mem_sets.1 (f i (h i.2))
    ⟨s, fun i h ↦ f' ⟨i, h⟩, fun _ H _ m ↦ h' ⟨_, H⟩ m⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : α → Filter β
F : (i : α) → Realizer (f i)
⊢ ∀ (x : Set β), x ∈ (bind ⊤ fun i => f i).sets ↔ x ∈ (⨆ (i : α), f i).sets
[PROOFSTEP]
simp [Filter.bind, eq_univ_iff_forall, iSup_sets_eq]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : Realizer f
⊢ f ≠ ⊥ ↔ ∀ (a : F.σ), Set.Nonempty (CFilter.f F.F a)
[PROOFSTEP]
rw [not_iff_comm, ← le_bot_iff, F.le_iff Realizer.bot, not_forall]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : Realizer f
⊢ (∃ x, ¬Set.Nonempty (CFilter.f F.F x)) ↔ ∀ (b : Realizer.bot.σ), ∃ a, CFilter.f F.F a ≤ CFilter.f Realizer.bot.F b
[PROOFSTEP]
simp only [Set.not_nonempty_iff_eq_empty]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : Realizer f
⊢ (∃ x, CFilter.f F.F x = ∅) ↔ ∀ (b : Realizer.bot.σ), ∃ a, CFilter.f F.F a ≤ CFilter.f Realizer.bot.F b
[PROOFSTEP]
exact
  ⟨fun ⟨x, e⟩ _ ↦ ⟨x, le_of_eq e⟩, fun h ↦
    let ⟨x, h⟩ := h ()
    ⟨x, le_bot_iff.1 h⟩⟩
