chore(data/finset/basic): remove inter_eq_sdiff_sdiff (#4953)

This is a duplicate of sdiff_sdiff_self_left
leanprover-community · Nov 9, 2020 · e1c333d · e1c333d
1 parent 40f673e
commit e1c333d
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 8 deletions.
diff --git a/archive/imo/imo1998_q2.lean b/archive/imo/imo1998_q2.lean
@@ -173,7 +173,7 @@ begin
     { finish, },
     { suffices : p.judge₁ = p.judge₂, { simp [this], }, finish, }, },
   have hst' : (s \ t).card = 2*z + 1, { rw [hst, finset.diag_card, ← hJ], refl, },
-  rw [finset.filter_and, finset.inter_eq_sdiff_sdiff s t, finset.card_sdiff],
+  rw [finset.filter_and, ← finset.sdiff_sdiff_self_left s t, finset.card_sdiff],
   { rw hst', rw add_assoc at hs, apply nat.le_sub_right_of_add_le hs, },
   { apply finset.sdiff_subset_self, },
 end

diff --git a/src/data/finset/basic.lean b/src/data/finset/basic.lean
@@ -761,13 +761,6 @@ by simp only [sdiff_inter_distrib_right, sdiff_self, empty_union]
 @[simp] theorem sdiff_inter_self_right (s₁ s₂ : finset α) : s₁ \ (s₂ ∩ s₁) = s₁ \ s₂ :=
 by simp only [sdiff_inter_distrib_right, sdiff_self, union_empty]
 
-lemma inter_eq_sdiff_sdiff (s₁ s₂ : finset α) : s₁ ∩ s₂ = s₁ \ (s₁ \ s₂) :=
-begin
-  ext a, split; intros h;
-  simp only [not_and, not_not, finset.mem_sdiff, finset.mem_inter] at h;
-  simp [h],
-end
-
 @[simp] theorem sdiff_empty {s₁ : finset α} : s₁ \ ∅ = s₁ :=
 ext (by simp)