Fixes in ComposableArrows

Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean

@@ -167,7 +167,8 @@ theorem mono_of_epi_of_epi_mono' (hR₁ : R₁.map' 0 2 = 0) (hR₁' : Epi (R₁
     mk₃ (R₂.map' 0 1) (R₂.map' 1 2) (0 : _ ⟶ R₁.obj' 0) := homMk₃ (app' φ 0) (app' φ 1)
       (app' φ 2) (𝟙 _) (naturality' φ 0 1) (naturality' φ 1 2) (by simp)
   refine mono_of_epi_of_mono_of_mono' ψ ?_ (exact₂_mk _ (by simp) ?_)
-    (hR₂.exact 0).exact_toComposableArrows h₀ h₁ (by dsimp [ψ]; infer_instance)
+    (hR₂.exact 0).exact_toComposableArrows h₀ h₁
+    (by dsimp only [ψ, homMk₃_app_three]; infer_instance)
   · dsimp
     rw [← Functor.map_comp]
     exact hR₁
@@ -222,7 +223,7 @@ theorem epi_of_epi_of_epi_of_epi (hR₂ : R₂.Exact) (hR₁' : Epi (R₁.map' 1
       (app' φ 2) (𝟙 _) (naturality' φ 0 1) (naturality' φ 1 2) (by simp)
   refine epi_of_epi_of_epi_of_mono' ψ (exact₂_mk _ (by simp) ?_)
     (hR₂.exact 0).exact_toComposableArrows (by simp)
-    h₀ h₁ (by dsimp [ψ]; infer_instance)
+    h₀ h₁ (by dsimp only [ψ, homMk₃_app_three]; infer_instance)
   rw [ShortComplex.exact_iff_epi _ (by simp)]
   exact hR₁'
 

Mathlib/CategoryTheory/ComposableArrows.lean

@@ -76,7 +76,7 @@ abbrev obj' (i : ℕ) (hi : i ≤ n := by valid) : C := F.obj ⟨i, by omega⟩
 
 /-- The map `F.obj' i ⟶ F.obj' j` when `F : ComposableArrows C n`, and `i` and `j`
 are natural numbers such that `i ≤ j ≤ n`. -/
-@[simp]
+-- @[simp]: Simp and reducible don't go together nicely with `#4154`
 abbrev map' (i j : ℕ) (hij : i ≤ j := by valid) (hjn : j ≤ n := by valid) :
   F.obj ⟨i, by omega⟩ ⟶ F.obj ⟨j, by omega⟩ := F.map (homOfLE (by
     simp only [Fin.mk_le_mk]
@@ -359,7 +359,7 @@ lemma map_comp {i j k : Fin (n + 1 + 1)} (hij : i ≤ j) (hjk : j ≤ k) :
       rw [id_comp]
     · obtain _ | _ | k := k
       · simp [Nat.succ.injEq] at hjk
-      · simp
+      · simp [map'.eq_1]
       · rfl
     · obtain _ | _ | k := k
       · simp [Fin.ext_iff] at hjk