no goals
F : Type ?u.32470
α : Type u_1
β : Type ?u.32476
γ : Type ?u.32479
δ : Type ?u.32482
ε : Type ?u.32485
inst✝ : InvolutiveInv α
f g : Filter α
s : Set α
⊢ f⁻¹ ≤ g ↔ f ≤ g⁻¹
rw [← Filter.inv_le_inv_iff, inv_inv]