feat(order/filter/pointwise): add lemmas (#18098)

src/order/filter/pointwise.lean

@@ -84,6 +84,9 @@ localized "attribute [instance] filter.has_one filter.has_zero" in pointwise
    tendsto f a 1 ↔ ∀ᶠ x in a, f x = 1 :=
 tendsto_pure
 
+@[simp, to_additive] lemma one_prod_one [has_one β] : (1 : filter α) ×ᶠ (1 : filter β) = 1 :=
+prod_pure_pure
+
 /-- `pure` as a `one_hom`. -/
 @[to_additive "`pure` as a `zero_hom`."]
 def pure_one_hom : one_hom α (filter α) := ⟨pure, pure_one⟩
@@ -119,7 +122,7 @@ instance : has_inv (filter α) := ⟨map has_inv.inv⟩
 end has_inv
 
 section has_involutive_inv
-variables [has_involutive_inv α] {f : filter α} {s : set α}
+variables [has_involutive_inv α] {f g : filter α} {s : set α}
 
 @[to_additive] lemma inv_mem_inv (hs : s ∈ f) : s⁻¹ ∈ f⁻¹ := by rwa [mem_inv, inv_preimage, inv_inv]
 
@@ -129,6 +132,17 @@ protected def has_involutive_inv : has_involutive_inv (filter α) :=
 { inv_inv := λ f, map_map.trans $ by rw [inv_involutive.comp_self, map_id],
   ..filter.has_inv }
 
+localized "attribute [instance] filter.has_involutive_inv filter.has_involutive_neg" in pointwise
+
+@[simp, to_additive] protected lemma inv_le_inv_iff : f⁻¹ ≤ g⁻¹ ↔ f ≤ g :=
+⟨λ h, inv_inv f ▸ inv_inv g ▸ filter.inv_le_inv h, filter.inv_le_inv⟩
+
+@[to_additive] lemma inv_le_iff_le_inv : f⁻¹ ≤ g ↔ f ≤ g⁻¹ :=
+by rw [← filter.inv_le_inv_iff, inv_inv]
+
+@[simp, to_additive] lemma inv_le_self : f⁻¹ ≤ f ↔ f⁻¹ = f :=
+⟨λ h, h.antisymm $ inv_le_iff_le_inv.1 h, eq.le⟩
+
 end has_involutive_inv
 
 /-! ### Filter addition/multiplication -/