chore(*): change notation for set.compl (leanprover-community#3212)

* introduce typeclass `has_compl` and notation `∁` for `has_compl.compl`
* use it instead of `has_neg` for `set` and `boolean_algebra`

src/algebra/punit_instances.lean

@@ -40,8 +40,9 @@ by refine
   inf := λ _ _, star,
   Sup := λ _, star,
   Inf := λ _, star,
-  sub := λ _ _, star,
-  .. punit.comm_ring, .. };
+  compl := λ _, star,
+  sdiff := λ _ _, star,
+  .. };
 intros; trivial
 
 instance : canonically_ordered_add_monoid punit :=

src/algebraic_geometry/prime_spectrum.lean

@@ -294,8 +294,8 @@ topological_space.of_closed (set.range prime_spectrum.zero_locus)
   (by { rintro _ _ ⟨s, rfl⟩ ⟨t, rfl⟩, exact ⟨_, (union_zero_locus s t).symm⟩ })
 
 lemma is_open_iff (U : set (prime_spectrum R)) :
-  is_open U ↔ ∃ s, -U = zero_locus s :=
-by simp only [@eq_comm _ (-U)]; refl
+  is_open U ↔ ∃ s, Uᶜ = zero_locus s :=
+by simp only [@eq_comm _ Uᶜ]; refl
 
 lemma is_closed_iff_zero_locus (Z : set (prime_spectrum R)) :
   is_closed Z ↔ ∃ s, Z = zero_locus s :=

src/analysis/calculus/deriv.lean

@@ -231,7 +231,7 @@ definition with a limit. In this version we have to take the limit along the sub
 because for `y=x` the slope equals zero due to the convention `0⁻¹=0`. -/
 lemma has_deriv_at_filter_iff_tendsto_slope {x : 𝕜} {L : filter 𝕜} :
   has_deriv_at_filter f f' x L ↔
-    tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (L ⊓ 𝓟 (-{x})) (𝓝 f') :=
+    tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (L ⊓ 𝓟 {x}ᶜ) (𝓝 f') :=
 begin
   conv_lhs { simp only [has_deriv_at_filter_iff_tendsto, (normed_field.norm_inv _).symm,
     (norm_smul _ _).symm, tendsto_zero_iff_norm_tendsto_zero.symm] },
@@ -260,7 +260,7 @@ end
 
 lemma has_deriv_at_iff_tendsto_slope {x : 𝕜} :
   has_deriv_at f f' x ↔
-    tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (nhds_within x (-{x})) (𝓝 f') :=
+    tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (nhds_within x {x}ᶜ) (𝓝 f') :=
 has_deriv_at_filter_iff_tendsto_slope
 
 theorem has_deriv_at_iff_is_o_nhds_zero : has_deriv_at f f' x ↔

src/analysis/normed_space/basic.lean

@@ -556,7 +556,7 @@ let ⟨n, hle, hlt⟩ := exists_int_pow_near' hr hw in
 by rwa norm_fpow⟩
 
 lemma punctured_nhds_ne_bot {α : Type*} [nondiscrete_normed_field α] (x : α) :
-  nhds_within x (-{x}) ≠ ⊥ :=
+  nhds_within x {x}ᶜ ≠ ⊥ :=
 begin
   rw [← mem_closure_iff_nhds_within_ne_bot, metric.mem_closure_iff],
   rintros ε ε0,
@@ -813,7 +813,7 @@ begin
       exact this hy },
     rw [← set.mem_compl_iff, ← closure_compl],
     rcases hE with ⟨z, hz⟩,
-    suffices : (λ c : ℝ, x + c • z) 0 ∈ closure (-{x} : set E),
+    suffices : (λ c : ℝ, x + c • z) 0 ∈ closure ({x}ᶜ : set E),
       by simpa only [zero_smul, add_zero] using this,
     have : (0:ℝ) ∈ closure (set.Ioi (0:ℝ)), by simp [closure_Ioi],
     refine (continuous_const.add (continuous_id.smul

src/data/analysis/filter.lean

@@ -175,7 +175,7 @@ protected def cofinite [decidable_eq α] : (@cofinite α).realizer := ⟨finset
   inf_le_right := λ s t a, mt (finset.mem_union_right _) },
 filter_eq $ set.ext $ λ x,
 ⟨λ ⟨s, h⟩, s.finite_to_set.subset (compl_subset_comm.1 h),
- λ ⟨fs⟩, by exactI ⟨(-x).to_finset, λ a (h : a ∉ (-x).to_finset),
+ λ ⟨fs⟩, by exactI ⟨xᶜ.to_finset, λ a (h : a ∉ xᶜ.to_finset),
   classical.by_contradiction $ λ h', h (mem_to_finset.2 h')⟩⟩⟩
 
 /-- Construct a realizer for filter bind -/

src/data/equiv/basic.lean

@@ -189,7 +189,7 @@ lemma symm_image_image {α β} (f : equiv α β) (s : set α) : f.symm '' (f ''
 by { rw [← set.image_comp], simp }
 
 protected lemma image_compl {α β} (f : equiv α β) (s : set α) :
-  f '' -s = -(f '' s) :=
+  f '' sᶜ = (f '' s)ᶜ :=
 set.image_compl_eq f.bijective
 
 /- The group of permutations (self-equivalences) of a type `α` -/
@@ -1075,26 +1075,26 @@ calc (insert a s : set α) ≃ ↥(s ∪ {a}) : equiv.set.of_eq (by simp)
 ... ≃ s ⊕ ({a} : set α) : equiv.set.union (by finish [set.subset_def])
 ... ≃ s ⊕ punit.{u+1} : sum_congr (equiv.refl _) (equiv.set.singleton _)
 
-/-- If `s : set α` is a set with decidable membership, then `s ⊕ (-s)` is equivalent to `α`. -/
-protected def sum_compl {α} (s : set α) [decidable_pred s] : s ⊕ (-s : set α) ≃ α :=
-calc s ⊕ (-s : set α) ≃ ↥(s ∪ -s) : (equiv.set.union (by simp [set.ext_iff])).symm
+/-- If `s : set α` is a set with decidable membership, then `s ⊕ sᶜ` is equivalent to `α`. -/
+protected def sum_compl {α} (s : set α) [decidable_pred s] : s ⊕ (sᶜ : set α) ≃ α :=
+calc s ⊕ (sᶜ : set α) ≃ ↥(s ∪ sᶜ) : (equiv.set.union (by simp [set.ext_iff])).symm
 ... ≃ @univ α : equiv.set.of_eq (by simp)
 ... ≃ α : equiv.set.univ _
 
 @[simp] lemma sum_compl_apply_inl {α : Type u} (s : set α) [decidable_pred s] (x : s) :
   equiv.set.sum_compl s (sum.inl x) = x := rfl
 
-@[simp] lemma sum_compl_apply_inr {α : Type u} (s : set α) [decidable_pred s] (x : -s) :
+@[simp] lemma sum_compl_apply_inr {α : Type u} (s : set α) [decidable_pred s] (x : sᶜ) :
   equiv.set.sum_compl s (sum.inr x) = x := rfl
 
 lemma sum_compl_symm_apply_of_mem {α : Type u} {s : set α} [decidable_pred s] {x : α}
   (hx : x ∈ s) : (equiv.set.sum_compl s).symm x = sum.inl ⟨x, hx⟩ :=
-have ↑(⟨x, or.inl hx⟩ : (s ∪ -s : set α)) ∈ s, from hx,
+have ↑(⟨x, or.inl hx⟩ : (s ∪ sᶜ : set α)) ∈ s, from hx,
 by { rw [equiv.set.sum_compl], simpa using set.union_apply_left _ this }
 
 lemma sum_compl_symm_apply_of_not_mem {α : Type u} {s : set α} [decidable_pred s] {x : α}
   (hx : x ∉ s) : (equiv.set.sum_compl s).symm x = sum.inr ⟨x, hx⟩ :=
-have ↑(⟨x, or.inr hx⟩ : (s ∪ -s : set α)) ∈ -s, from hx,
+have ↑(⟨x, or.inr hx⟩ : (s ∪ sᶜ : set α)) ∈ sᶜ, from hx,
 by { rw [equiv.set.sum_compl], simpa using set.union_apply_right _ this }
 
 /-- `sum_diff_subset s t` is the natural equivalence between

src/data/indicator_function.lean

@@ -80,7 +80,7 @@ begin
 end
 
 lemma indicator_preimage (s : set α) (f : α → β) (B : set β) :
-  (indicator s f)⁻¹' B = s ∩ f ⁻¹' B ∪ (-s) ∩ (λa:α, (0:β)) ⁻¹' B :=
+  (indicator s f)⁻¹' B = s ∩ f ⁻¹' B ∪ sᶜ ∩ (λa:α, (0:β)) ⁻¹' B :=
 by { rw [indicator, if_preimage] }
 
 lemma indicator_preimage_of_not_mem (s : set α) (f : α → β) {t : set β} (ht : (0:β) ∉ t) :
@@ -139,7 +139,7 @@ lemma indicator_sub (s : set α) (f g : α → β) :
   indicator s (λa, f a - g a) = λa, indicator s f a - indicator s g a :=
 show indicator s (f - g) = indicator s f - indicator s g, from is_add_group_hom.map_sub _ _ _
 
-lemma indicator_compl (s : set α) (f : α → β) : indicator (-s) f = λ a, f a - indicator s f a :=
+lemma indicator_compl (s : set α) (f : α → β) : indicator sᶜ f = λ a, f a - indicator s f a :=
 begin
   funext,
   simp only [indicator],

src/data/pfun.lean

@@ -531,7 +531,7 @@ lemma core_def (s : set β) : core f s = {x | ∀ y, y ∈ f x → y ∈ s} := r
 lemma mem_core (x : α) (s : set β) : x ∈ core f s ↔ (∀ y, y ∈ f x → y ∈ s) :=
 iff.rfl
 
-lemma compl_dom_subset_core (s : set β) : -f.dom ⊆ f.core s :=
+lemma compl_dom_subset_core (s : set β) : f.domᶜ ⊆ f.core s :=
 assume x hx y fxy,
 absurd ((mem_dom f x).mpr ⟨y, fxy⟩) hx
 
@@ -552,7 +552,7 @@ end
 section
 open_locale classical
 
-lemma core_res (f : α → β) (s : set α) (t : set β) : core (res f s) t = -s ∪ f ⁻¹' t :=
+lemma core_res (f : α → β) (s : set α) (t : set β) : core (res f s) t = sᶜ ∪ f ⁻¹' t :=
 by { ext, rw mem_core_res, by_cases h : x ∈ s; simp [h] }
 
 end
@@ -573,7 +573,7 @@ set.eq_of_subset_of_subset
     have ys : y ∈ s, from xcore _ (roption.get_mem _),
     show x ∈ preimage f s, from  ⟨(f x).get xdom, ys, roption.get_mem _⟩)
 
-lemma core_eq (f : α →. β) (s : set β) : f.core s = f.preimage s ∪ -f.dom :=
+lemma core_eq (f : α →. β) (s : set β) : f.core s = f.preimage s ∪ f.domᶜ :=
 by rw [preimage_eq, set.union_distrib_right, set.union_comm (dom f), set.compl_union_self,
         set.inter_univ, set.union_eq_self_of_subset_right (compl_dom_subset_core f s)]
 

src/data/real/hyperreal.lean

@@ -93,7 +93,7 @@ lemma lt_of_tendsto_zero_of_pos {f : ℕ → ℝ} (hf : tendsto f at_top (𝓝 0
 begin
   simp only [metric.tendsto_at_top, dist_zero_right, norm, lt_def U] at hf ⊢,
   intros r hr, cases hf r hr with N hf',
-  have hs : -{i : ℕ | f i < r} ⊆ {i : ℕ | i ≤ N} :=
+  have hs : {i : ℕ | f i < r}ᶜ ⊆ {i : ℕ | i ≤ N} :=
     λ i hi1, le_of_lt (by simp only [lt_iff_not_ge];
     exact λ hi2, hi1 (lt_of_le_of_lt (le_abs_self _) (hf' i hi2)) : i < N),
   exact mem_hyperfilter_of_finite_compl
@@ -440,7 +440,7 @@ theorem infinite_pos_of_tendsto_top {f : ℕ → ℝ} (hf : tendsto f at_top at_
 Exists.cases_on (hf' (r + 1)) $ λ i hi,
   have hi' : ∀ (a : ℕ), f a < (r + 1) → a < i :=
     λ a, by rw [←not_le, ←not_le]; exact not_imp_not.mpr (hi a),
-  have hS : - {a : ℕ | r < f a} ⊆ {a : ℕ | a ≤ i} :=
+  have hS : {a : ℕ | r < f a}ᶜ ⊆ {a : ℕ | a ≤ i} :=
     by simp only [set.compl_set_of, not_lt];
     exact λ a har, le_of_lt (hi' a (lt_of_le_of_lt har (lt_add_one _))),
   (germ.coe_lt U).2 $ mem_hyperfilter_of_finite_compl $
@@ -452,7 +452,7 @@ theorem infinite_neg_of_tendsto_bot {f : ℕ → ℝ} (hf : tendsto f at_top at_
 Exists.cases_on (hf' (r - 1)) $ λ i hi,
   have hi' : ∀ (a : ℕ), r - 1 < f a → a < i :=
     λ a, by rw [←not_le, ←not_le]; exact not_imp_not.mpr (hi a),
-  have hS : - {a : ℕ | f a < r} ⊆ {a : ℕ | a ≤ i} :=
+  have hS : {a : ℕ | f a < r}ᶜ ⊆ {a : ℕ | a ≤ i} :=
     by simp only [set.compl_set_of, not_lt];
     exact λ a har, le_of_lt (hi' a (lt_of_lt_of_le (sub_one_lt _) har)),
   (germ.coe_lt U).2 $ mem_hyperfilter_of_finite_compl $