fixes for leanprover/lean4#6123

leanprover-community · Dec 3, 2024 · e46b013 · e46b013
1 parent 559f03b
commit e46b013
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 3 deletions.
diff --git 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
@@ -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