chore(CategoryTheory.ConcreteCategory): inline `ConcreteCategory.forg…

…et` (#19217) We already make `forget` `reducible` and further declarations downstream of it `abbrev`'s. It makes sense to `inline` it also to avoid Lean noticing it.
leanprover-community · Nov 23, 2024 · ba61bf3 · ba61bf3
1 parent 8eedc61
commit ba61bf3
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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`. -/