inter_eq_of_self_of_subset

Stream: general

[Reid Barton]

Should these lemmas from data.set.basic be simp lemmas? I was surprised when simp didn't solve these statements automatically.

theorem inter_eq_self_of_subset_left {s t : set α} (h : s ⊆ t) : s ∩ t = s :=
by finish [subset_def, ext_iff, iff_def]

theorem inter_eq_self_of_subset_right {s t : set α} (h : t ⊆ s) : s ∩ t = t :=
by finish [subset_def, ext_iff, iff_def]