-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 : ComposableArrows.{v_1, u_1} C n
F G : ComposableArrows.{v_1, u_1} C (n + 1)
α : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯
β : F.δ₀ ⟶ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
i : ℕ
hi : i < n + 1
zero :
  ∀ (hi : 0 < n + 1),
    Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩)
      (F.map' 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ hi ≫
          (fun (i : Fin (n + 1 + 1)) ↦
              (match (motive := (i : Fin (n + 1 + 1)) → F.obj i ⟶ G.obj i) i with
                | ⟨0, isLt⟩ => α
                | ⟨i.succ, hi⟩ => app' β i ⋯ :
                F.obj i ⟶ G.obj i))
            ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ :
        F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩)
      (CategoryStruct.comp (Y := G.obj ⟨0, ⋯⟩)
          ((fun (i : Fin (n + 1 + 1)) ↦
                (match (motive := (i : Fin (n + 1 + 1)) → F.obj i ⟶ G.obj i) i with
                  | ⟨0, isLt⟩ => α
                  | ⟨i.succ, hi⟩ => app' β i ⋯ :
                  F.obj i ⟶ G.obj i))
              ⟨0, ⋯⟩ :
            F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨0, ⋯⟩)
          (G.map' 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ hi :
            G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩) :
        F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩)
⊢ F.map' i (i + 1) ⋯ hi ≫
      (fun (i : Fin (n + 1 + 1)) ↦
          (match (motive := (i : Fin (n + 1 + 1)) → F.obj i ⟶ G.obj i) i with
            | ⟨0, isLt⟩ => α
            | ⟨i.succ, hi⟩ => app' β i ⋯ :
            F.obj i ⟶ G.obj i))
        ⟨i + 1, ⋯⟩ =
    (fun (i : Fin (n + 1 + 1)) ↦
          (match (motive := (i : Fin (n + 1 + 1)) → F.obj i ⟶ G.obj i) i with
            | ⟨0, isLt⟩ => α
            | ⟨i.succ, hi⟩ => app' β i ⋯ :
            F.obj i ⟶ G.obj i))
        (⟨i, ⋯⟩ : Fin (n + 1 + 1)) ≫
      G.map' i (i + 1) ⋯ hi
have succ : ∀ (i : ℕ) (hi : i + 1 < n + 1),
  Eq (α := F.obj (⟨i + 1, sorry⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i + 1 + 1, sorry⟩)
    (F.map' (i + 1) (i + 1 + 1) sorry hi ≫
        (fun (i : Fin (n + 1 + 1)) ↦
            (match (motive := (i : Fin (n + 1 + 1)) → F.obj i ⟶ G.obj i) i with
              | ⟨0, isLt⟩ => α
              | ⟨i.succ, hi⟩ => app' β i sorry :
              F.obj i ⟶ G.obj i))
          ⟨i + 1 + 1, sorry⟩ :
      F.obj (⟨i + 1, sorry⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i + 1 + 1, sorry⟩)
    (CategoryStruct.comp (Y := G.obj ⟨i + 1, sorry⟩)
        ((fun (i : Fin (n + 1 + 1)) ↦
              (match (motive := (i : Fin (n + 1 + 1)) → F.obj i ⟶ G.obj i) i with
                | ⟨0, isLt⟩ => α
                | ⟨i.succ, hi⟩ => app' β i sorry :
                F.obj i ⟶ G.obj i))
            ⟨i + 1, sorry⟩ :
          F.obj (⟨i + 1, sorry⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i + 1, sorry⟩)
        (G.map' (i + 1) (i + 1 + 1) sorry hi : G.obj (⟨i + 1, sorry⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i + 1 + 1, sorry⟩) :
      F.obj (⟨i + 1, sorry⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i + 1 + 1, sorry⟩)
Tactic: obtain _ | i := i
Cleared hypotheses: i, hi