Can remove these local instances, they're mentioned explicitly below …

…anyway
leanprover-community · Jan 17, 2025 · 5f65e81 · 5f65e81
1 parent 540b773
commit 5f65e81
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
@@ -371,7 +371,6 @@ abbrev HasForget.toFunLike [HasForget C] (X Y : C) :
   coe := (forget C).map
   coe_injective' _ _ h := Functor.Faithful.map_injective h
 
-attribute [local instance] HasForget.toFunLike
 /-- Build a concrete category out of `HasForget`.
 
 The intended usecase is to prove theorems referencing only `(forget C)`
@@ -387,8 +386,6 @@ abbrev HasForget.toConcreteCategory [HasForget C] :
   id_apply := congr_fun ((forget C).map_id _)
   comp_apply _ _ := congr_fun ((forget C).map_comp _ _)
 
-attribute [local instance] HasForget.toConcreteCategory
-
 /-- Check that the new `ConcreteCategory` has the same forgetful functor as we started with. -/
 example [inst : HasForget C] :
     @forget C _ ((HasForget.toConcreteCategory _).toHasForget) = @forget C _ inst := by