fix

leanprover-community · Jan 5, 2025 · a340252 · a340252
1 parent 18fe524
commit a340252
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
@@ -625,7 +625,7 @@ instance biproduct.map_epi {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p
       ι_colimMap_assoc, Discrete.functor_obj_eq_as, Discrete.natTrans_app, colimit.ι_desc_assoc,
       Cofan.mk_pt, Cofan.mk_ι_app, ι_π, ι_π_assoc]
     split
-    simp
+    all_goals simp_all
   rw [this]
   infer_instance