diff --git a/Mathlib/CategoryTheory/Preadditive/Mat.lean b/Mathlib/CategoryTheory/Preadditive/Mat.lean
index 66427c64c35345..e4c1a473beddfa 100644
--- a/Mathlib/CategoryTheory/Preadditive/Mat.lean
+++ b/Mathlib/CategoryTheory/Preadditive/Mat.lean
@@ -195,7 +195,7 @@ instance hasFiniteBiproducts : HasFiniteBiproducts (Mat_ C) where
               simp_rw [dite_comp, comp_dite]
               simp only [ite_self, dite_eq_ite, Limits.comp_zero, Limits.zero_comp,
                 eqToHom_trans]
-              erw [Finset.sum_sigma]
+              rw [← Finset.univ_sigma_univ, Finset.sum_sigma]
               dsimp +instances
               simp only [if_true, Finset.sum_dite_irrel, Finset.mem_univ,
                 Finset.sum_const_zero, Finset.sum_dite_eq']