Update Mathlib/Algebra/Homology/SpectralObject/Page.lean

joelriou · robin-carlier · web-flow · commit f740c72d57a2 · 2026-03-05T13:01:52.000Z
Co-authored-by: Robin Carlier &lt;57142648+robin-carlier@users.noreply.github.com&gt;
diff --git a/Mathlib/Algebra/Homology/SpectralObject/Page.lean b/Mathlib/Algebra/Homology/SpectralObject/Page.lean
@@ -613,8 +613,7 @@ lemma cokernelSequenceOpcyclesE_exact
     ⟨y₁ ≫ biprod.fst, y₁ ≫ biprod.snd, by ext <;> simp⟩
   simp only [Preadditive.add_comp, Category.assoc, biprod.inl_desc, biprod.inr_desc] at hy₁
   refine ⟨A₂, π₂ ≫ π₁, inferInstance, a, ?_⟩
-  dsimp
-  simp only [Category.assoc, hy₂, reassoc_of% hy₁, Preadditive.add_comp, δ_pOpcycles,
+  simp [Category.assoc, hy₂, reassoc_of% hy₁, Preadditive.add_comp, δ_pOpcycles,
     comp_zero, add_zero]
 
 -- TODO: add dual statement to `cokernelSequenceOpcyclesE_exact`?
