From 92c78c9302e1c0ed59ca7eb46376a1867921d59b Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Sat, 25 Apr 2026 19:55:04 +0800 Subject: [PATCH] chore(CategoryTheory/Preadditive/Mat): remove an erw --- Mathlib/CategoryTheory/Preadditive/Mat.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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']