fix

joelriou · joelriou · commit 4e50e585aeba · 2026-02-04T21:03:20.000+01:00
diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/KInjective.lean b/Mathlib/Algebra/Homology/HomotopyCategory/KInjective.lean
@@ -170,7 +170,7 @@ instance (K L : CochainComplex C ℤ) [hK : K.IsKInjective] [hL : L.IsKInjective
     preservesBinaryBiproducts_of_preservesBiproducts _
   refine ObjectProperty.prop_of_iso _
     ((HomotopyCategory.quotient C (.up ℤ)).mapBiprod K L).symm ?_
-  apply ObjectProperty.prop_biprod
+  apply ObjectProperty.prop_biprod_of_isClosedUnderBinaryProducts
   all_goals assumption
 
 lemma IsKInjective.eq_δ_of_cocycle {K L : CochainComplex C ℤ} {n : ℤ}
diff --git a/Mathlib/CategoryTheory/ObjectProperty/FiniteProducts.lean b/Mathlib/CategoryTheory/ObjectProperty/FiniteProducts.lean
@@ -40,7 +40,8 @@ lemma prop_prod [P.IsClosedUnderBinaryProducts] (X Y : C) [HasBinaryProduct X Y]
     P (X ⨯ Y) :=
   P.prop_limit _ (by rintro ⟨_ | _⟩ <;> assumption)
 
-lemma prop_biprod [HasZeroMorphisms C] [P.IsClosedUnderBinaryProducts] (X Y : C)
+lemma prop_biprod_of_isClosedUnderBinaryProducts
+    [HasZeroMorphisms C] [P.IsClosedUnderBinaryProducts] (X Y : C)
     [HasBinaryBiproduct X Y]
     (hX : P X) (hY : P Y) :
     P (X ⊞ Y) :=
