Theorem: FilterGame.Filter.as_basis_as_filter_eq_self (FilterGame/Basis.lean)

State before:
α : Type u_1
f : Filter α
⊢ Basis.as_filter (as_basis f) = f
Tactic:
sorry
State after:
no goals