feat(data/basic/lean): add lemmas finset.subset_iff_inter_eq_{left, r…

…ight} (#7053)

These lemmas are the analogues of `set.subset_iff_inter_eq_{left, right}`, except stated for `finset`s.

Zulip:
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/finset.2Esubset_iff_inter_eq_left.20.2F.20right





Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/data/finset/basic.lean

@@ -701,6 +701,9 @@ end
 /-- `s ∩ t` is the set such that `a ∈ s ∩ t` iff `a ∈ s` and `a ∈ t`. -/
 instance : has_inter (finset α) := ⟨λ s₁ s₂, ⟨_, nodup_ndinter s₂.1 s₁.2⟩⟩
 
+-- TODO: some of these results may have simpler proofs, once there are enough results
+-- to obtain the `lattice` instance.
+
 theorem inter_val_nd (s₁ s₂ : finset α) : (s₁ ∩ s₂).1 = ndinter s₁.1 s₂.1 := rfl
 
 @[simp] theorem inter_val (s₁ s₂ : finset α) : (s₁ ∩ s₂).1 = s₁.1 ∩ s₂.1 :=
@@ -841,6 +844,14 @@ theorem union_distrib_right (s t u : finset α) : (s ∩ t) ∪ u = (s ∪ u) 
 
 lemma union_eq_empty_iff (A B : finset α) : A ∪ B = ∅ ↔ A = ∅ ∧ B = ∅ := sup_eq_bot_iff
 
+theorem inter_eq_left_iff_subset (s t : finset α) :
+  s ∩ t = s ↔ s ⊆ t :=
+(inf_eq_left : s ⊓ t = s ↔ s ≤ t)
+
+theorem inter_eq_right_iff_subset (s t : finset α) :
+  t ∩ s = s ↔ s ⊆ t :=
+(inf_eq_right : t ⊓ s = s ↔ s ≤ t)
+
 /-! ### erase -/
 
 /-- `erase s a` is the set `s - {a}`, that is, the elements of `s` which are

src/data/set/basic.lean

@@ -536,17 +536,17 @@ theorem subset_inter {s t r : set α} (rs : r ⊆ s) (rt : r ⊆ t) : r ⊆ s 
 @[simp] theorem subset_inter_iff {s t r : set α} : r ⊆ s ∩ t ↔ r ⊆ s ∧ r ⊆ t :=
 (forall_congr (by exact λ x, imp_and_distrib)).trans forall_and_distrib
 
-theorem subset_iff_inter_eq_left {s t : set α} : s ⊆ t ↔ s ∩ t = s :=
-(ext_iff.trans $ forall_congr $ λ x, and_iff_left_iff_imp).symm
+theorem inter_eq_left_iff_subset {s t : set α} : s ∩ t = s ↔ s ⊆ t :=
+ext_iff.trans $ forall_congr $ λ x, and_iff_left_iff_imp
 
-theorem subset_iff_inter_eq_right {s t : set α} : t ⊆ s ↔ s ∩ t = t :=
-(ext_iff.trans $ forall_congr $ λ x, and_iff_right_iff_imp).symm
+theorem inter_eq_right_iff_subset {s t : set α} : s ∩ t = t ↔ t ⊆ s :=
+ext_iff.trans $ forall_congr $ λ x, and_iff_right_iff_imp
 
 theorem inter_eq_self_of_subset_left {s t : set α} : s ⊆ t → s ∩ t = s :=
-subset_iff_inter_eq_left.1
+inter_eq_left_iff_subset.mpr
 
 theorem inter_eq_self_of_subset_right {s t : set α} : t ⊆ s → s ∩ t = t :=
-subset_iff_inter_eq_right.1
+inter_eq_right_iff_subset.mpr
 
 @[simp] theorem inter_univ (a : set α) : a ∩ univ = a :=
 inter_eq_self_of_subset_left $ subset_univ _
@@ -564,10 +564,10 @@ theorem inter_subset_inter_right {s t : set α} (u : set α) (H : s ⊆ t) : u 
 inter_subset_inter subset.rfl H
 
 theorem union_inter_cancel_left {s t : set α} : (s ∪ t) ∩ s = s :=
-subset_iff_inter_eq_right.1 $ subset_union_left _ _
+inter_eq_self_of_subset_right $ subset_union_left _ _
 
 theorem union_inter_cancel_right {s t : set α} : (s ∪ t) ∩ t = t :=
-subset_iff_inter_eq_right.1 $ subset_union_right _ _
+inter_eq_self_of_subset_right $ subset_union_right _ _
 
 /-! ### Distributivity laws -/
 
@@ -742,7 +742,7 @@ theorem mem_sep_iff {s : set α} {p : α → Prop} {x : α} : x ∈ {x ∈ s | p
 iff.rfl
 
 theorem eq_sep_of_subset {s t : set α} (h : s ⊆ t) : s = {x ∈ t | x ∈ s} :=
-(subset_iff_inter_eq_right.1 h).symm
+(inter_eq_self_of_subset_right h).symm
 
 theorem sep_subset (s : set α) (p : α → Prop) : {x ∈ s | p x} ⊆ s := λ x, and.left
 

src/measure_theory/measure_space.lean

@@ -943,7 +943,7 @@ rfl
 by simp [← restrictₗ_apply, restrictₗ, ht]
 
 lemma restrict_eq_self (h_meas_t : measurable_set t) (h : t ⊆ s) : μ.restrict s t = μ t :=
-by rw [restrict_apply h_meas_t, subset_iff_inter_eq_left.1 h]
+by rw [restrict_apply h_meas_t, inter_eq_left_iff_subset.mpr h]
 
 lemma restrict_apply_self (μ:measure α) (h_meas_s : measurable_set s) :
   (μ.restrict s) s = μ s := (restrict_eq_self h_meas_s (set.subset.refl _))