diff --git a/Mathlib/AlgebraicTopology/DoldKan/Faces.lean b/Mathlib/AlgebraicTopology/DoldKan/Faces.lean
index 845dd32f779d1..9d627dc6e3b6a 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/Faces.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/Faces.lean
@@ -150,8 +150,7 @@ theorem comp_Hσ_eq_zero {Y : C} {n q : ℕ} {φ : Y ⟶ X _[n + 1]} (v : Higher
     · intro j
       dsimp [Fin.cast, Fin.castLE, Fin.castLT]
       rw [comp_zsmul, comp_zsmul, δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]
-      · simp only [Fin.lt_iff_val_lt_val]
-        dsimp [Fin.succ]
+      · simp [Fin.lt_iff_val_lt_val]
         omega
       · intro h
         simp only [Fin.pred, Fin.subNat, Fin.ext_iff, Nat.succ_add_sub_one,
diff --git a/Mathlib/CategoryTheory/ComposableArrows.lean b/Mathlib/CategoryTheory/ComposableArrows.lean
index 0fcf2d10bbac5..0e94df5b10c76 100644
--- a/Mathlib/CategoryTheory/ComposableArrows.lean
+++ b/Mathlib/CategoryTheory/ComposableArrows.lean
@@ -526,7 +526,7 @@ def isoMkSucc {F G : ComposableArrows C (n + 1)} (α : F.obj' 0 ≅ G.obj' 0)
   hom := homMkSucc α.hom β.hom w
   inv := homMkSucc α.inv β.inv (by
     rw [← cancel_epi α.hom, ← reassoc_of% w, α.hom_inv_id_assoc, β.hom_inv_id_app]
-    dsimp
+    dsimp [Fin.succ_zero_eq_one]
     rw [comp_id])
   hom_inv_id := by
     apply hom_ext_succ