equalities with set differences

Stream: Is there code for X?

[Kalle Kytölä]

I did not find the following two, although I suspect they must exist. If they do, where? If not, should they, and how to golf their proofs to an acceptable shape?

lemma union_diff_of_subset {α' : Type*} {s t : set α'}
  (hst : s ⊆ t) : t = s ∪ (t.diff s) :=
begin
  apply le_antisymm,
  { intros x hx,
    by_cases hxs : x ∈ s,
    { left, exact hxs, },
    { right, exact ⟨hx, hxs⟩, }, },
  { simp only [le_eq_subset, union_subset_iff],
    exact ⟨hst, sep_subset t (λ (x : α'), x ∉ s)⟩, },
end

lemma diff_diff_of_subset {α' : Type*} {s t : set α'}
  (hst : s ⊆ t) : s = t.diff (t.diff s) :=
begin
  apply le_antisymm,
  { intros x hx,
    fsplit,
    { exact hst hx, },
    { intros h, exact h.2 hx, }, },
  { intros x hx,
    by_contradiction contra,
    exact hx.2 ⟨hx.1, contra⟩, },
end

[Heather Macbeth]

I just used this the other day! Let me find it :)

[Heather Macbeth]

docs#set.diff_union_of_subset

[Heather Macbeth]

and docs#set.diff_diff_cancel_left

[Kalle Kytölä]

Ah, with the first I knew I should try the equality both ways to help library_search, but didn't think of writing the union in that order...

And I almost guessed the name of the second, but autocomplete did not suggest this...

Thank you very much, Heather!