case mk
α : Type u_1
β : Type ?u.7565
σ : Type ?u.7568
τ : Type ?u.7571
f : Filter α
a : Set α
σ✝ : Type u_2
F✝ : CFilter (Set α) σ✝
eq✝ : CFilter.toFilter F✝ = f
⊢ a ∈ f ↔ ∃ b, CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F b ⊆ a
α : Type u_1
β : Type ?u.7565
σ : Type ?u.7568
τ : Type ?u.7571
f : Filter α
F : Realizer f
a : Set α
⊢ a ∈ f ↔ ∃ b, CFilter.f F.F b ⊆ a
cases F
case mk
α : Type u_1
β : Type ?u.7565
σ : Type ?u.7568
τ : Type ?u.7571
a : Set α
σ✝ : Type u_2
F✝ : CFilter (Set α) σ✝
⊢ a ∈ CFilter.toFilter F✝ ↔
    ∃ b, CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F b ⊆ a
case mk
α : Type u_1
β : Type ?u.7565
σ : Type ?u.7568
τ : Type ?u.7571
f : Filter α
a : Set α
σ✝ : Type u_2
F✝ : CFilter (Set α) σ✝
eq✝ : CFilter.toFilter F✝ = f
⊢ a ∈ f ↔ ∃ b, CFilter.f { σ := σ✝, F := F✝, eq := eq✝ }.F b ⊆ a
subst f
no goals
case mk
α : Type u_1
β : Type ?u.7565
σ : Type ?u.7568
τ : Type ?u.7571
a : Set α
σ✝ : Type u_2
F✝ : CFilter (Set α) σ✝
⊢ a ∈ CFilter.toFilter F✝ ↔
    ∃ b, CFilter.f { σ := σ✝, F := F✝, eq := (_ : CFilter.toFilter F✝ = CFilter.toFilter F✝) }.F b ⊆ a
rfl