Insert lemmas

Stream: Is there code for X?

[Jason KY.]

Do we have these two insert lemmas?

lemma set.insert_inter_of_mem {s₁ s₂ : set α} {a : α} (h : a ∈ s₂) :
  insert a s₁ ∩ s₂ = insert a (s₁ ∩ s₂) :=
by { ext, split; finish }

lemma set.insert_inter_of_not_mem {s₁ s₂ : set α} {a : α} (h : a ∉ s₂) :
  insert a s₁ ∩ s₂ = s₁ ∩ s₂ :=
by { ext, split; finish }

I think they are pretty useful but I can't seem to find them anywhere (I was able to find a finset version but not for set).

[Eric Wieser]

docs#set.insert_inter followed by docs#set.insert_eq_of_mem?

[Jason KY.]

That works great! Thanks