-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
hk :
  ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
i : ℕ
hj : i + (k + 1) = i + k + 1
hj' : i + k + 1 ≤ n
succ :
  Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (CategoryStruct.comp (Y := F.obj ⟨i + k, ⋯⟩)
          (F.map' i (i + k) ⋯ ⋯ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨i + k, ⋯⟩)
          (F.map' (i + k) (i + k + 1) ⋯ hj' : F.obj (⟨i + k, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨i + k + 1, ⋯⟩) ≫
        app ⟨i + k + 1, ⋯⟩ :
      F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i (i + k + 1) ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
succ₁ :
  Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (CategoryStruct.comp (Y := F.obj ⟨i + k, ⋯⟩)
          (F.map' i (i + k) ⋯ ⋯ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨i + k, ⋯⟩)
          (F.map' (i + k) (i + k + 1) ⋯ hj' : F.obj (⟨i + k, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨i + k + 1, ⋯⟩) ≫
        app ⟨i + k + 1, ⋯⟩ :
      F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫
        CategoryStruct.comp (Y := G.obj ⟨i + k, ⋯⟩)
          (G.map' i (i + k) ⋯ ⋯ : G.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k, ⋯⟩)
          (G.map' (i + k) (i + k + 1) ⋯ hj' : G.obj (⟨i + k, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩) :
      F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
succ₂ :
  Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (CategoryStruct.comp (Y := F.obj ⟨i + k, ⋯⟩)
        (F.map' i (i + k) ⋯ ⋯ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨i + k, ⋯⟩)
        (F.map' (i + k) (i + k + 1) ⋯ hj' ≫ app ⟨i + k + 1, ⋯⟩ :
          F.obj (⟨i + k, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩) :
      F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫
        CategoryStruct.comp (Y := G.obj ⟨i + k, ⋯⟩)
          (G.map' i (i + k) ⋯ ⋯ : G.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k, ⋯⟩)
          (G.map' (i + k) (i + k + 1) ⋯ hj' : G.obj (⟨i + k, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩) :
      F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
succ₃ :
  Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (CategoryStruct.comp (Y := F.obj ⟨i + k, ⋯⟩)
        (F.map' i (i + k) ⋯ ⋯ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨i + k, ⋯⟩)
        (app (⟨i + k, ⋯⟩ : Fin (n + 1)) ≫ G.map' (i + k) (i + k + 1) ⋯ hj' :
          F.obj (⟨i + k, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩) :
      F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫
        CategoryStruct.comp (Y := G.obj ⟨i + k, ⋯⟩)
          (G.map' i (i + k) ⋯ ⋯ : G.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k, ⋯⟩)
          (G.map' (i + k) (i + k + 1) ⋯ hj' : G.obj (⟨i + k, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩) :
      F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
succ₄ succ₅ :
  Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫
        CategoryStruct.comp (Y := G.obj ⟨i + k, ⋯⟩)
          (G.map' i (i + k) ⋯ ⋯ : G.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k, ⋯⟩)
          (G.map' (i + k) (i + k + 1) ⋯ hj' : G.obj (⟨i + k, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩) :
      F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫
        CategoryStruct.comp (Y := G.obj ⟨i + k, ⋯⟩)
          (G.map' i (i + k) ⋯ ⋯ : G.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k, ⋯⟩)
          (G.map' (i + k) (i + k + 1) ⋯ hj' : G.obj (⟨i + k, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩) :
      F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
⊢ Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (F.map' i (i + k + 1) ⋯ hj' ≫ app ⟨i + k + 1, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i (i + k + 1) ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)

Tactic:
rw [F.map'_comp i (i + k) (i + k + 1), G.map'_comp i (i + k) (i + k + 1), assoc,
        w (i + k) (by valid), reassoc_of% (hk i (i + k) rfl (by valid))]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ComposableArrows.map'_comp, HAdd.hAdd, OfNat.ofNat, rfl