Undo rename in test/elementwise.lean

leanprover-community · Nov 11, 2021 · 4c51e75 · 4c51e75
1 parent 5b154e4
commit 4c51e75
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/test/elementwise.lean b/test/elementwise.lean
@@ -15,7 +15,7 @@ lemma foo' {C : Type*} [category C]
   {M N K : C} {f : M ⟶ N} {g : N ⟶ K} {h : M ⟶ K} (w : f ≫ g = h) : f ≫ 𝟙 N ≫ g = h :=
 by simp [w]
 
-local attribute [instance] concrete_category.has_coe_to_sort concrete_category.to_fun
+local attribute [instance] concrete_category.has_coe_to_sort concrete_category.has_coe_to_fun
 
 lemma bar {C : Type u} [category.{v} C] [concrete_category.{w} C]
   {M N K : C} {f : M ⟶ N} {g : N ⟶ K} {h : M ⟶ K} (w : f ≫ g = h) (x : M) : g (f x) = h x :=