fix(data/set/function): do not use reducible (#12377)

Reducible should only be used if the definition if it occurs as an explicit argument in a type class and must reduce during type class search, or if it is a type that should inherit instances.  Propositions should only be reducible if they are trivial variants (`<` and `>` for example).

These reducible attributes here will cause issues in Lean 4.  In Lean 4, the simplifier unfold reducible definitions in simp lemmas.  This means that tagging an `inj_on`-theorem with `@[simp]` creates the simp lemma `?a = ?b` (i.e. match anything).

Author: gebner

src/data/set/function.lean

@@ -205,7 +205,7 @@ end order
 /-! ### maps to -/
 
 /-- `maps_to f a b` means that the image of `a` is contained in `b`. -/
-@[reducible] def maps_to (f : α → β) (s : set α) (t : set β) : Prop := ∀ ⦃x⦄, x ∈ s → f x ∈ t
+def maps_to (f : α → β) (s : set α) (t : set β) : Prop := ∀ ⦃x⦄, x ∈ s → f x ∈ t
 
 /-- Given a map `f` sending `s : set α` into `t : set β`, restrict domain of `f` to `s`
 and the codomain to `t`. Same as `subtype.map`. -/
@@ -325,7 +325,7 @@ theorem maps_to.mem_iff (h : maps_to f s t) (hc : maps_to f sᶜ tᶜ) {x} : f x
 /-! ### Injectivity on a set -/
 
 /-- `f` is injective on `a` if the restriction of `f` to `a` is injective. -/
-@[reducible] def inj_on (f : α → β) (s : set α) : Prop :=
+def inj_on (f : α → β) (s : set α) : Prop :=
 ∀ ⦃x₁ : α⦄, x₁ ∈ s → ∀ ⦃x₂ : α⦄, x₂ ∈ s → f x₁ = f x₂ → x₁ = x₂
 
 theorem subsingleton.inj_on (hs : s.subsingleton) (f : α → β) : inj_on f s :=
@@ -414,7 +414,7 @@ lemma inj_on.cancel_left (hg : t.inj_on g) (hf₁ : s.maps_to f₁ t) (hf₂ : s
 /-! ### Surjectivity on a set -/
 
 /-- `f` is surjective from `a` to `b` if `b` is contained in the image of `a`. -/
-@[reducible] def surj_on (f : α → β) (s : set α) (t : set β) : Prop := t ⊆ f '' s
+def surj_on (f : α → β) (s : set α) (t : set β) : Prop := t ⊆ f '' s
 
 theorem surj_on.subset_range (h : surj_on f s t) : t ⊆ range f :=
 subset.trans h $ image_subset_range f s
@@ -508,7 +508,7 @@ lemma eq_on_comp_right_iff : s.eq_on (g₁ ∘ f) (g₂ ∘ f) ↔ (f '' s).eq_o
 /-! ### Bijectivity -/
 
 /-- `f` is bijective from `s` to `t` if `f` is injective on `s` and `f '' s = t`. -/
-@[reducible] def bij_on (f : α → β) (s : set α) (t : set β) : Prop :=
+def bij_on (f : α → β) (s : set α) (t : set β) : Prop :=
 maps_to f s t ∧ inj_on f s ∧ surj_on f s t
 
 lemma bij_on.maps_to (h : bij_on f s t) : maps_to f s t := h.left
@@ -572,7 +572,7 @@ lemma bij_on.compl (hst : bij_on f s t) (hf : bijective f) : bij_on f sᶜ tᶜ
 /-! ### left inverse -/
 
 /-- `g` is a left inverse to `f` on `a` means that `g (f x) = x` for all `x ∈ a`. -/
-@[reducible] def left_inv_on (f' : β → α) (f : α → β) (s : set α) : Prop :=
+def left_inv_on (f' : β → α) (f : α → β) (s : set α) : Prop :=
 ∀ ⦃x⦄, x ∈ s → f' (f x) = x
 
 lemma left_inv_on.eq_on (h : left_inv_on f' f s) : eq_on (f' ∘ f) id s := h
@@ -688,7 +688,7 @@ theorem surj_on.left_inv_on_of_right_inv_on (hf : surj_on f s t) (hf' : right_in
 /-! ### Two-side inverses -/
 
 /-- `g` is an inverse to `f` viewed as a map from `a` to `b` -/
-@[reducible] def inv_on (g : β → α) (f : α → β) (s : set α) (t : set β) : Prop :=
+def inv_on (g : β → α) (f : α → β) (s : set α) (t : set β) : Prop :=
 left_inv_on g f s ∧ right_inv_on g f t
 
 lemma inv_on.symm (h : inv_on f' f s t) : inv_on f f' t s := ⟨h.right, h.left⟩

src/logic/function/basic.lean

@@ -677,7 +677,7 @@ end involutive
 /-- The property of a binary function `f : α → β → γ` being injective.
 Mathematically this should be thought of as the corresponding function `α × β → γ` being injective.
 -/
-@[reducible] def injective2 {α β γ} (f : α → β → γ) : Prop :=
+def injective2 {α β γ} (f : α → β → γ) : Prop :=
 ∀ ⦃a₁ a₂ b₁ b₂⦄, f a₁ b₁ = f a₂ b₂ → a₁ = a₂ ∧ b₁ = b₂
 
 namespace injective2