feat(Algebra/Module/Submodule): Add pointwise negation lemma (#36634)

- Add `Submodule.neg_eq_iff_neg_le` proving `-S = S ↔ -S ≤ S`
- Make arguments of `Submodule.neg_le_neg` and `Submodule.neg_le` implicit

For completeness I added the set version:

- Add `Set.inv_eq_iff_inv_subset` proving `s⁻¹ = s ↔ s⁻¹ ⊆ s` and its additive version

I did not manage to give a short proof of the submodule version from the set version like it is the case for `neg_le` and `neg_le_neg`.

Co-authored-by: Martin Winter <martin.winter.math@gmail.com>

Author: martinwintermath

Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

@@ -229,6 +229,10 @@ theorem inv_subset_inv : s⁻¹ ⊆ t⁻¹ ↔ s ⊆ t :=
 @[to_additive]
 theorem inv_subset : s⁻¹ ⊆ t ↔ s ⊆ t⁻¹ := by rw [← inv_subset_inv, inv_inv]
 
+@[to_additive]
+theorem inv_eq_self_iff_inv_subset : s⁻¹ = s ↔ s⁻¹ ⊆ s :=
+  ⟨le_of_eq, fun h => antisymm h <| inv_subset.mp h⟩
+
 @[to_additive (attr := simp)]
 theorem inv_singleton (a : α) : ({a} : Set α)⁻¹ = {a⁻¹} := by
   rw [← image_inv_eq_inv, image_singleton]

Mathlib/Algebra/Module/Submodule/Pointwise.lean

@@ -96,12 +96,15 @@ protected def involutivePointwiseNeg : InvolutiveNeg (Submodule R M) where
 scoped[Pointwise] attribute [instance] Submodule.involutivePointwiseNeg
 
 @[simp]
-theorem neg_le_neg (S T : Submodule R M) : -S ≤ -T ↔ S ≤ T :=
+theorem neg_le_neg {S T : Submodule R M} : -S ≤ -T ↔ S ≤ T :=
   SetLike.coe_subset_coe.symm.trans Set.neg_subset_neg
 
-theorem neg_le (S T : Submodule R M) : -S ≤ T ↔ S ≤ -T :=
+theorem neg_le {S T : Submodule R M} : -S ≤ T ↔ S ≤ -T :=
   SetLike.coe_subset_coe.symm.trans Set.neg_subset
 
+theorem neg_eq_self_iff_neg_le {S : Submodule R M} : -S = S ↔ -S ≤ S :=
+  ⟨le_of_eq, fun h => antisymm h <| neg_le.mp h⟩
+
 /-- `Submodule.pointwiseNeg` as an order isomorphism. -/
 def negOrderIso : Submodule R M ≃o Submodule R M where
   toEquiv := Equiv.neg _