diff --git a/Mathlib/Algebra/Homology/Opposite.lean b/Mathlib/Algebra/Homology/Opposite.lean
index c4532f7c469d0f..10e5d2d49f745b 100644
--- a/Mathlib/Algebra/Homology/Opposite.lean
+++ b/Mathlib/Algebra/Homology/Opposite.lean
@@ -426,10 +426,10 @@ section
 
 variable [Preadditive V]
 
-set_option backward.isDefEq.respectTransparency false in
+example : Preadditive (HomologicalComplex Vᵒᵖ c) := inferInstance
+
 instance opFunctor_additive : (@opFunctor ι V _ c _).Additive where
 
-set_option backward.isDefEq.respectTransparency false in
 instance unopFunctor_additive : (@unopFunctor ι V _ c _).Additive where
 
 end
diff --git a/Mathlib/CategoryTheory/Preadditive/Opposite.lean b/Mathlib/CategoryTheory/Preadditive/Opposite.lean
index b231ff0ce9705a..eea96f56183214 100644
--- a/Mathlib/CategoryTheory/Preadditive/Opposite.lean
+++ b/Mathlib/CategoryTheory/Preadditive/Opposite.lean
@@ -25,10 +25,16 @@ namespace CategoryTheory
 variable (C : Type*) [Category* C] [Preadditive C]
 
 instance : Preadditive Cᵒᵖ where
-  homGroup X Y := Equiv.addCommGroup (opEquiv X Y)
+  homGroup X Y := fast_instance% Equiv.addCommGroup (opEquiv X Y)
   add_comp _ _ _ f f' g := Quiver.Hom.unop_inj (Preadditive.comp_add _ _ _ g.unop f.unop f'.unop)
   comp_add _ _ _ f g g' := Quiver.Hom.unop_inj (Preadditive.add_comp _ _ _ g.unop g'.unop f.unop)
 
+/-- Test that the two ways to obtain the `HasZeroMorphisms Cᵒᵖ` instance
+from `Preadditive C` are the same. -/
+example : (instPreadditiveOpposite C).preadditiveHasZeroMorphisms =
+    @Limits.hasZeroMorphismsOpposite  C _ Preadditive.preadditiveHasZeroMorphisms := by
+  with_reducible_and_instances rfl
+
 instance moduleEndLeft {X Y : C} : Module (End X)ᵐᵒᵖ (X ⟶ Y) where
   smul_add _ _ _ := Preadditive.comp_add _ _ _ _ _ _
   smul_zero _ := Limits.comp_zero