no goals
F : Type ?u.30467
α : Type u_1
β : Type ?u.30473
γ : Type ?u.30476
δ : Type ?u.30479
ε : Type ?u.30482
inst✝ : InvolutiveInv α
f g : Filter α
s : Set α
hs : s ∈ f
⊢ s⁻¹ ∈ f⁻¹
rwa [mem_inv, inv_preimage, inv_inv]