Revert "workaround"

This reverts commit 4e69a93.

Mathlib/AlgebraicTopology/DoldKan/HomotopyEquivalence.lean

@@ -73,17 +73,13 @@ def homotopyPInftyToId : Homotopy (PInfty : K[X] ⟶ _) (𝟙 _) where
     rcases n with _|n
     . simpa only [Homotopy.dNext_zero_chainComplex, Homotopy.prevD_chainComplex,
         PInfty_f, Nat.zero_eq, P_f_0_eq, zero_add] using (homotopyPToId X 2).comm 0
-    · have := (homotopyPToId X (n + 2)).comm (n + 1)
-      rw [Homotopy.dNext_succ_chainComplex, Homotopy.prevD_chainComplex] at this
-      rw [Homotopy.dNext_succ_chainComplex, Homotopy.prevD_chainComplex, PInfty_f,
-        ← P_is_eventually_constant (rfl.le : n + 1 ≤ n + 1),
-        homotopyPToId_eventually_constant X (lt_add_one (n + 1))]
-      exact this
+    · simpa only [Homotopy.dNext_succ_chainComplex, Homotopy.prevD_chainComplex,
+        HomologicalComplex.id_f, PInfty_f, ← P_is_eventually_constant (rfl.le : n + 1 ≤ n + 1),
+        homotopyPToId_eventually_constant X (lt_add_one (n + 1))] using
+        (homotopyPToId X (n + 2)).comm (n + 1)
 set_option linter.uppercaseLean3 false in
 #align algebraic_topology.dold_kan.homotopy_P_infty_to_id AlgebraicTopology.DoldKan.homotopyPInftyToId
 
--- #exit
-
 /-- The inclusion of the Moore complex in the alternating face map complex
 is an homotopy equivalence -/
 @[simps]