feat(algebra/module): sub_mem_sup for modules over rings (#15733)

src/algebra/module/submodule/lattice.lean

@@ -213,6 +213,14 @@ show T ≤ S ⊔ T, from le_sup_right
 lemma add_mem_sup {S T : submodule R M} {s t : M} (hs : s ∈ S) (ht : t ∈ T) : s + t ∈ S ⊔ T :=
 add_mem (mem_sup_left hs) (mem_sup_right ht)
 
+lemma sub_mem_sup {R' M' : Type*} [ring R'] [add_comm_group M'] [module R' M']
+  {S T : submodule R' M'} {s t : M'} (hs : s ∈ S) (ht : t ∈ T) :
+  s - t ∈ S ⊔ T :=
+begin
+  rw sub_eq_add_neg,
+  exact add_mem_sup hs (neg_mem ht),
+end
+
 lemma mem_supr_of_mem {ι : Sort*} {b : M} {p : ι → submodule R M} (i : ι) (h : b ∈ p i) :
   b ∈ (⨆i, p i) :=
 have p i ≤ (⨆i, p i) := le_supr p i,