diff --git a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
index 38882d4e9f448..ebeea719fe2dc 100644
--- a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
+++ b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
@@ -55,7 +55,7 @@ class ConcreteCategory (C : Type u) [Category.{v} C] where
   /-- That functor is faithful -/
   [forget_faithful : forget.Faithful]
 
-attribute [reducible] ConcreteCategory.forget
+attribute [inline, reducible] ConcreteCategory.forget
 attribute [instance] ConcreteCategory.forget_faithful
 
 /-- The forgetful functor from a concrete category to `Type u`. -/