Set.diff_subset_diff_inj?

Stream: Is there code for X?

[Monica Omar]

do we have something like this:

theorem Set.diff_subset_diff_inj {α : Type*} (s : Set α) {t u : Set α} (h : u ⊆ t) :
    s \ u ⊆ t \ u ↔ s ⊆ t := by

[Aaron Liu]

import Mathlib

theorem Set.diff_subset_diff_right_iff {α : Type*} (s : Set α) {t u : Set α} (h : u ⊆ t) :
    s \ u ⊆ t \ u ↔ s ⊆ t := by
  rw [Set.diff_subset_iff, Set.union_diff_cancel h]

[Aaron Liu]

This holds more generally in a docs#GeneralizedCoheytingAlgebra