refactor(data/set/basic): Remove _eq lemmas (#16572)

This PR removes `_eq` lemmas from `data.set.basic` which asset a `rfl` propositional equality, in favour of the `iff` versions, and makes the latter `simp` lemmas if they weren't already.



Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>

Author: linesthatinterlace

archive/100-theorems-list/30_ballot_problem.lean

@@ -320,7 +320,7 @@ lemma first_vote_pos :
         (nonempty_image_iff.2 (counted_sequence_nonempty _ _))],
     { have : list.cons (-1) '' counted_sequence (p + 1) q ∩ {l : list ℤ | l.head = 1} = ∅,
       { ext,
-        simp only [mem_inter_eq, mem_image, mem_set_of_eq, mem_empty_eq, iff_false, not_and,
+        simp only [mem_inter_iff, mem_image, mem_set_of_eq, mem_empty_iff_false, iff_false, not_and,
           forall_exists_index, and_imp],
         rintro l _ rfl,
         norm_num },
@@ -392,7 +392,7 @@ begin
   rw [counted_succ_succ, union_inter_distrib_right,
     (_ : list.cons (-1) '' counted_sequence (p + 1) q ∩ {l | l.head = 1} = ∅), union_empty];
   { ext,
-    simp only [mem_inter_eq, mem_image, mem_set_of_eq, and_iff_left_iff_imp, mem_empty_eq,
+    simp only [mem_inter_iff, mem_image, mem_set_of_eq, and_iff_left_iff_imp, mem_empty_iff_false,
       iff_false, not_and, forall_exists_index, and_imp],
     rintro y hy rfl,
     norm_num }
@@ -410,7 +410,7 @@ begin
   have : (counted_sequence p (q + 1)).image (list.cons 1) ∩ stays_positive =
          (counted_sequence p (q + 1) ∩ stays_positive).image (list.cons 1),
   { ext t,
-    simp only [mem_inter_eq, mem_image],
+    simp only [mem_inter_iff, mem_image],
     split,
     { simp only [and_imp, exists_imp_distrib],
       rintro l hl rfl t,
@@ -433,7 +433,7 @@ begin
   rw [counted_succ_succ, union_inter_distrib_right,
     (_ : list.cons 1 '' counted_sequence p (q + 1) ∩ {l : list ℤ | l.head = 1}ᶜ = ∅), empty_union];
   { ext,
-    simp only [mem_inter_eq, mem_image, mem_set_of_eq, and_iff_left_iff_imp, mem_empty_eq,
+    simp only [mem_inter_iff, mem_image, mem_set_of_eq, and_iff_left_iff_imp, mem_empty_iff_false,
       iff_false, not_and, forall_exists_index, and_imp],
     rintro y hy rfl,
     norm_num }
@@ -451,7 +451,7 @@ begin
   have : (counted_sequence (p + 1) q).image (list.cons (-1)) ∩ stays_positive =
          ((counted_sequence (p + 1) q) ∩ stays_positive).image (list.cons (-1)),
   { ext t,
-    simp only [mem_inter_eq, mem_image],
+    simp only [mem_inter_iff, mem_image],
     split,
     { simp only [and_imp, exists_imp_distrib],
       rintro l hl rfl t,

counterexamples/phillips.lean

@@ -546,7 +546,7 @@ begin
   apply ae_restrict_of_ae,
   refine measure_mono_null _ ((countable_ne Hcont φ).measure_zero _),
   assume x,
-  simp only [imp_self, mem_set_of_eq, mem_compl_eq],
+  simp only [imp_self, mem_set_of_eq, mem_compl_iff],
 end
 
 lemma integrable_comp (Hcont : #ℝ = aleph 1) (φ : (discrete_copy ℝ →ᵇ ℝ) →L[ℝ] ℝ) :

src/algebra/indicator_function.lean

@@ -96,7 +96,7 @@ mul_indicator_eq_one
 
 @[to_additive] lemma mul_indicator_apply_ne_one {a : α} :
   s.mul_indicator f a ≠ 1 ↔ a ∈ s ∩ mul_support f :=
-by simp only [ne.def, mul_indicator_apply_eq_one, not_imp, mem_inter_eq, mem_mul_support]
+by simp only [ne.def, mul_indicator_apply_eq_one, not_imp, mem_inter_iff, mem_mul_support]
 
 @[simp, to_additive] lemma mul_support_mul_indicator :
   function.mul_support (s.mul_indicator f) = s ∩ function.mul_support f :=
@@ -413,7 +413,7 @@ begin
   rw [finset.prod_insert haI, finset.set_bUnion_insert, mul_indicator_union_of_not_mem_inter, ih _],
   { assume i hi j hj hij,
     exact hI i (finset.mem_insert_of_mem hi) j (finset.mem_insert_of_mem hj) hij },
-  simp only [not_exists, exists_prop, mem_Union, mem_inter_eq, not_and],
+  simp only [not_exists, exists_prop, mem_Union, mem_inter_iff, not_and],
   assume hx a' ha',
   refine disjoint_left.1 (hI a (finset.mem_insert_self _ _) a' (finset.mem_insert_of_mem ha') _) hx,
   exact (ne_of_mem_of_not_mem ha' haI).symm

src/algebra/order/floor.lean

@@ -596,7 +596,7 @@ end
 lemma preimage_fract (s : set α) : fract ⁻¹' s = ⋃ m : ℤ, (λ x, x - m) ⁻¹' (s ∩ Ico (0 : α) 1) :=
 begin
   ext x,
-  simp only [mem_preimage, mem_Union, mem_inter_eq],
+  simp only [mem_preimage, mem_Union, mem_inter_iff],
   refine ⟨λ h, ⟨⌊x⌋, h, fract_nonneg x, fract_lt_one x⟩, _⟩,
   rintro ⟨m, hms, hm0, hm1⟩,
   obtain rfl : ⌊x⌋ = m, from floor_eq_iff.2 ⟨sub_nonneg.1 hm0, sub_lt_iff_lt_add'.1 hm1⟩,
@@ -606,7 +606,7 @@ end
 lemma image_fract (s : set α) : fract '' s = ⋃ m : ℤ, (λ x, x - m) '' s ∩ Ico 0 1 :=
 begin
   ext x,
-  simp only [mem_image, mem_inter_eq, mem_Union], split,
+  simp only [mem_image, mem_inter_iff, mem_Union], split,
   { rintro ⟨y, hy, rfl⟩,
     exact ⟨⌊y⌋, ⟨y, hy, rfl⟩, fract_nonneg y, fract_lt_one y⟩ },
   { rintro ⟨m, ⟨y, hys, rfl⟩, h0, h1⟩,

src/algebra/support.lean

@@ -149,7 +149,7 @@ rfl
 
 @[to_additive support_prod_mk] lemma mul_support_prod_mk (f : α → M) (g : α → N) :
   mul_support (λ x, (f x, g x)) = mul_support f ∪ mul_support g :=
-set.ext $ λ x, by simp only [mul_support, not_and_distrib, mem_union_eq, mem_set_of_eq,
+set.ext $ λ x, by simp only [mul_support, not_and_distrib, mem_union, mem_set_of_eq,
   prod.mk_eq_one, ne.def]
 
 @[to_additive support_prod_mk'] lemma mul_support_prod_mk' (f : α → M × N) :
@@ -200,7 +200,7 @@ end division_monoid
 
 @[simp] lemma support_mul [mul_zero_class R] [no_zero_divisors R] (f g : α → R) :
   support (λ x, f x * g x) = support f ∩ support g :=
-set.ext $ λ x, by simp only [mem_support, mul_ne_zero_iff, mem_inter_eq, not_or_distrib]
+set.ext $ λ x, by simp only [mem_support, mul_ne_zero_iff, mem_inter_iff, not_or_distrib]
 
 @[simp] lemma support_mul_subset_left [mul_zero_class R] (f g : α → R) :
   support (λ x, f x * g x) ⊆ support f :=

src/algebraic_geometry/locally_ringed_space.lean

@@ -250,9 +250,9 @@ end
   X.to_RingedSpace.basic_open (0 : X.presheaf.obj $ op U) = ∅ :=
 begin
   ext,
-  simp only [set.mem_empty_eq, topological_space.opens.empty_eq, topological_space.opens.mem_coe,
-    opens.coe_bot, iff_false, RingedSpace.basic_open, is_unit_zero_iff, set.mem_set_of_eq,
-    map_zero],
+  simp only [set.mem_empty_iff_false, topological_space.opens.empty_eq,
+    topological_space.opens.mem_coe, opens.coe_bot, iff_false, RingedSpace.basic_open,
+    is_unit_zero_iff, set.mem_set_of_eq, map_zero],
   rintro ⟨⟨y, _⟩, h, e⟩,
   exact @zero_ne_one (X.presheaf.stalk y) _ _ h,
 end

src/algebraic_geometry/prime_spectrum/basic.lean

@@ -332,7 +332,7 @@ end
 
 lemma mem_compl_zero_locus_iff_not_mem {f : R} {I : prime_spectrum R} :
   I ∈ (zero_locus {f} : set (prime_spectrum R))ᶜ ↔ f ∉ I.as_ideal :=
-by rw [set.mem_compl_eq, mem_zero_locus, set.singleton_subset_iff]; refl
+by rw [set.mem_compl_iff, mem_zero_locus, set.singleton_subset_iff]; refl
 
 /-- The Zariski topology on the prime spectrum of a commutative ring
 is defined via the closed sets of the topology:
@@ -659,7 +659,7 @@ lemma is_open_basic_open {a : R} : is_open ((basic_open a) : set (prime_spectrum
 
 @[simp] lemma basic_open_eq_zero_locus_compl (r : R) :
   (basic_open r : set (prime_spectrum R)) = (zero_locus {r})ᶜ :=
-set.ext $ λ x, by simpa only [set.mem_compl_eq, mem_zero_locus, set.singleton_subset_iff]
+set.ext $ λ x, by simpa only [set.mem_compl_iff, mem_zero_locus, set.singleton_subset_iff]
 
 @[simp] lemma basic_open_one : basic_open (1 : R) = ⊤ :=
 topological_space.opens.ext $ by simp
@@ -692,7 +692,7 @@ begin
   { rintros _ ⟨r, rfl⟩,
     exact is_open_basic_open },
   { rintros p U hp ⟨s, hs⟩,
-    rw [← compl_compl U, set.mem_compl_eq, ← hs, mem_zero_locus, set.not_subset] at hp,
+    rw [← compl_compl U, set.mem_compl_iff, ← hs, mem_zero_locus, set.not_subset] at hp,
     obtain ⟨f, hfs, hfp⟩ := hp,
     refine ⟨basic_open f, ⟨f, rfl⟩, hfp, _⟩,
     rw [← set.compl_subset_compl, ← hs, basic_open_eq_zero_locus_compl, compl_compl],
@@ -747,7 +747,7 @@ begin
   rw localization_comap_range S (submonoid.powers r),
   ext,
   simp only [mem_zero_locus, basic_open_eq_zero_locus_compl, set_like.mem_coe, set.mem_set_of_eq,
-    set.singleton_subset_iff, set.mem_compl_eq],
+    set.singleton_subset_iff, set.mem_compl_iff],
   split,
   { intros h₁ h₂,
     exact h₁ ⟨submonoid.mem_powers r, h₂⟩ },

src/algebraic_geometry/prime_spectrum/is_open_comap_C.lean

@@ -49,7 +49,7 @@ lemma image_of_Df_eq_comap_C_compl_zero_locus :
   image_of_Df f = prime_spectrum.comap (C : R →+* R[X]) '' (zero_locus {f})ᶜ :=
 begin
   refine ext (λ x, ⟨λ hx, ⟨⟨map C x.val, (is_prime_map_C_of_is_prime x.property)⟩, ⟨_, _⟩⟩, _⟩),
-  { rw [mem_compl_eq, mem_zero_locus, singleton_subset_iff],
+  { rw [mem_compl_iff, mem_zero_locus, singleton_subset_iff],
     cases hx with i hi,
     exact λ a, hi (mem_map_C_iff.mp a i) },
   { refine subtype.ext (ext (λ x, ⟨λ h, _, λ h, subset_span (mem_image_of_mem C.1 h)⟩)),

src/algebraic_geometry/projective_spectrum/topology.lean

@@ -287,7 +287,7 @@ end
 
 lemma mem_compl_zero_locus_iff_not_mem {f : A} {I : projective_spectrum 𝒜} :
   I ∈ (zero_locus 𝒜 {f} : set (projective_spectrum 𝒜))ᶜ ↔ f ∉ I.as_homogeneous_ideal :=
-by rw [set.mem_compl_eq, mem_zero_locus, set.singleton_subset_iff]; refl
+by rw [set.mem_compl_iff, mem_zero_locus, set.singleton_subset_iff]; refl
 
 /-- The Zariski topology on the prime spectrum of a commutative ring
 is defined via the closed sets of the topology:
@@ -364,7 +364,7 @@ lemma is_open_basic_open {a : A} : is_open ((basic_open 𝒜 a) :
 
 @[simp] lemma basic_open_eq_zero_locus_compl (r : A) :
   (basic_open 𝒜 r : set (projective_spectrum 𝒜)) = (zero_locus 𝒜 {r})ᶜ :=
-set.ext $ λ x, by simpa only [set.mem_compl_eq, mem_zero_locus, set.singleton_subset_iff]
+set.ext $ λ x, by simpa only [set.mem_compl_iff, mem_zero_locus, set.singleton_subset_iff]
 
 @[simp] lemma basic_open_one : basic_open 𝒜 (1 : A) = ⊤ :=
 topological_space.opens.ext $ by simp
@@ -408,7 +408,7 @@ begin
   { rintros _ ⟨r, rfl⟩,
     exact is_open_basic_open 𝒜 },
   { rintros p U hp ⟨s, hs⟩,
-    rw [← compl_compl U, set.mem_compl_eq, ← hs, mem_zero_locus, set.not_subset] at hp,
+    rw [← compl_compl U, set.mem_compl_iff, ← hs, mem_zero_locus, set.not_subset] at hp,
     obtain ⟨f, hfs, hfp⟩ := hp,
     refine ⟨basic_open 𝒜 f, ⟨f, rfl⟩, hfp, _⟩,
     rw [← set.compl_subset_compl, ← hs, basic_open_eq_zero_locus_compl, compl_compl],

src/analysis/box_integral/basic.lean

@@ -207,7 +207,7 @@ begin
     (l.has_basis_to_filter_Union_top _).prod_self.tendsto_iff uniformity_basis_dist_le],
   refine forall₂_congr (λ ε ε0, exists_congr $ λ r, _),
   simp only [exists_prop, prod.forall, set.mem_Union, exists_imp_distrib,
-    prod_mk_mem_set_prod_eq, and_imp, mem_inter_eq, mem_set_of_eq],
+    prod_mk_mem_set_prod_eq, and_imp, mem_inter_iff, mem_set_of_eq],
   exact and_congr iff.rfl ⟨λ H c₁ c₂ π₁ π₂ h₁ hU₁ h₂ hU₂, H π₁ π₂ c₁ h₁ hU₁ c₂ h₂ hU₂,
     λ H π₁ π₂ c₁ h₁ hU₁ c₂ h₂ hU₂, H c₁ c₂ π₁ π₂ h₁ hU₁ h₂ hU₂⟩
 end
@@ -593,7 +593,7 @@ lemma tendsto_integral_sum_sum_integral (h : integrable I l f vol) (π₀ : prep
 begin
   refine ((l.has_basis_to_filter_Union I π₀).tendsto_iff nhds_basis_closed_ball).2 (λ ε ε0, _),
   refine ⟨h.convergence_r ε, h.convergence_r_cond ε, _⟩,
-  simp only [mem_inter_eq, set.mem_Union, mem_set_of_eq],
+  simp only [mem_inter_iff, set.mem_Union, mem_set_of_eq],
   rintro π ⟨c, hc, hU⟩,
   exact h.dist_integral_sum_sum_integral_le_of_mem_base_set_of_Union_eq ε0 hc hU
 end
@@ -707,7 +707,7 @@ begin
   rcases exists_pos_mul_lt ε0' (B I) with ⟨ε', ε'0, hεI⟩,
   set δ : ℝ≥0 → ℝⁿ → Ioi (0 : ℝ) := λ c x, if x ∈ s then δ₁ c x (εs x) else (δ₂ c) x ε',
   refine ⟨δ, λ c, l.r_cond_of_bRiemann_eq_ff hl, _⟩,
-  simp only [set.mem_Union, mem_inter_eq, mem_set_of_eq],
+  simp only [set.mem_Union, mem_inter_iff, mem_set_of_eq],
   rintro π ⟨c, hπδ, hπp⟩,
   /- Now we split the sum into two parts based on whether `π.tag J` belongs to `s` or not. -/
   rw [← g.sum_partition_boxes le_rfl hπp, mem_closed_ball, integral_sum,