cases f
case mpr
α : Type u_1
f g : Filter α
h : f.sets = g.sets
⊢ f = g
case mpr.mk
α : Type u_1
g : Filter α
sets✝ : Set (Set α)
univ_mem_sets✝ : Set.univ ∈ sets✝
superset_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → s ⊆ t → t ∈ sets✝
inter_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → s ∩ t ∈ sets✝
h :
  { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
        inter_mem_sets := inter_mem_sets✝ }.sets =
    g.sets
⊢ { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
      inter_mem_sets := inter_mem_sets✝ } =
    g