try

Author: sgouezel

Mathlib/CategoryTheory/Localization/LocallySmall.lean

@@ -41,13 +41,12 @@ noncomputable def hasLocalizationOfLocallySmall
   D := ShrinkHoms D
   L := L ⋙ (ShrinkHoms.equivalence D).functor
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- If `L : C ⥤ D` is a localization functor for a class of morphisms
 `W : MorphismProperty C`, and `D` is locally `w`-small, we may obtain
 a `HasLocalization.{w} W` instance. This should be used only in the
 unlikely situation where the types of objects of `C` and `D` are in
 different universes. Otherwise, use `hasLocalizationOfLocallySmall`. -/
+@[implicit_reducible]
 noncomputable irreducible_def hasLocalizationOfLocallySmall'
     {D : Type u₂} [Category.{v₂} D] [LocallySmall.{w} D]
     (L : C ⥤ D) [L.IsLocalization W] :

Mathlib/Data/Fintype/Defs.lean

@@ -260,18 +260,16 @@ instance subsingleton (α : Type*) : Subsingleton (Fintype α) :=
 
 instance (α : Type*) : Lean.Meta.FastSubsingleton (Fintype α) := {}
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- Given a predicate that can be represented by a finset, the subtype
 associated to the predicate is a fintype. -/
+@[implicit_reducible]
 protected def subtype {p : α → Prop} (s : Finset α) (H : ∀ x : α, x ∈ s ↔ p x) :
     Fintype { x // p x } :=
   ⟨⟨s.1.pmap Subtype.mk fun x => (H x).1, s.nodup.pmap fun _ _ _ _ => congr_arg Subtype.val⟩,
     fun ⟨x, px⟩ => Multiset.mem_pmap.2 ⟨x, (H x).2 px, rfl⟩⟩
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- Construct a fintype from a finset with the same elements. -/
+@[implicit_reducible]
 def ofFinset {p : Set α} (s : Finset α) (H : ∀ x, x ∈ s ↔ x ∈ p) : Fintype p :=
   Fintype.subtype s H
 

Mathlib/Data/Fintype/Sets.lean

@@ -264,9 +264,8 @@ theorem Fintype.univ_Prop : (Finset.univ : Finset Prop) = {True, False} :=
 instance Subtype.fintype (p : α → Prop) [DecidablePred p] [Fintype α] : Fintype { x // p x } :=
   Fintype.subtype (univ.filter p) (by simp)
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- A set on a fintype, when coerced to a type, is a fintype. -/
+@[implicit_reducible]
 def setFintype [Fintype α] (s : Set α) [DecidablePred (· ∈ s)] : Fintype s :=
   Subtype.fintype fun x => x ∈ s