From 03a6a6015c0b12dce7b36b4a1f7205a92dfaa592 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Wed, 18 Aug 2021 21:26:33 +0000
Subject: [PATCH] fix(library/init/function): make injective semireducible
 (#604)

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/bad.20simp.20lemmas/near/249899277
---
 library/init/function.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/init/function.lean b/library/init/function.lean
index a3a2f98e00..397319bb9b 100644
--- a/library/init/function.lean
+++ b/library/init/function.lean
@@ -70,7 +70,7 @@ lemma comp.assoc (f : φ → δ) (g : β → φ) (h : α → β) : (f ∘ g) ∘
 lemma comp_const_right (f : β → φ) (b : β) : f ∘ (const α b) = const α (f b) := rfl
 
 /-- A function `f : α → β` is called injective if `f x = f y` implies `x = y`. -/
-@[reducible] def injective (f : α → β) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂
+def injective (f : α → β) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂
 
 lemma injective.comp {g : β → φ} {f : α → β} (hg : injective g) (hf : injective f) :
   injective (g ∘ f) :=