. intro h; rw [h]
case mp
α : Type u_1
f g : Filter α
⊢ f = g → f.sets = g.sets

case mpr
α : Type u_1
f g : Filter α
⊢ f.sets = g.sets → f = g
case mpr
α : Type u_1
f g : Filter α
⊢ f.sets = g.sets → f = g