-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
hn :
  ∀ (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ),
    ∃ (F : ComposableArrows.{v_1, u_1} C n) (e : (i : Fin (n + 1)) → F.obj i ≅ obj i),
      ∀ (i : ℕ) (hi : i < n),
        mapSucc ⟨i, hi⟩ =
          Iso.inv (e (⟨i, ⋯⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) ⋯ hi ≫ Iso.hom (e (⟨i + 1, ⋯⟩ : Fin (n + 1)))
obj : Fin (n + 1 + 1) → C
mapSucc : (i : Fin (n + 1)) → obj i.castSucc ⟶ obj i.succ
F : ComposableArrows.{v_1, u_1} C n
e : (i : Fin (n + 1)) → F.obj i ≅ obj i.succ
h :
  ∀ (i : ℕ) (hi : i < n),
    mapSucc ⟨i, hi⟩.succ =
      Iso.inv (e (⟨i, ⋯⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) ⋯ hi ≫ Iso.hom (e (⟨i + 1, ⋯⟩ : Fin (n + 1)))
i : ℕ
hi : i < n + 1
succ :
  ∀ (hi : 0 < n + 1),
    Eq (α := obj (⟨0, hi⟩ : Fin (n + 1)).castSucc ⟶ obj ⟨0, hi⟩.succ) (mapSucc ⟨0, hi⟩)
      (CategoryStruct.comp (Y := (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj ⟨0, ⋯⟩)
        (Iso.inv
            ((fun (i : Fin (n + 1 + 1)) ↦
                (match (motive := (i : Fin (n + 1 + 1)) → (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj i ≅ obj i) i with
                  | ⟨0, ⋯⟩ => Iso.refl ((F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj 0)
                  | ⟨i.succ, hi⟩ => e ⟨i, ⋯⟩ :
                  (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj i ≅ obj i))
              ⟨0, ⋯⟩) :
          obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj ⟨0, ⋯⟩)
        ((F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).map' 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ hi ≫
            Iso.hom
              ((fun (i : Fin (n + 1 + 1)) ↦
                  (match (motive := (i : Fin (n + 1 + 1)) → (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj i ≅ obj i)
                      i with
                    | ⟨0, ⋯⟩ => Iso.refl ((F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj 0)
                    | ⟨i.succ, hi⟩ => e ⟨i, ⋯⟩ :
                    (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj i ≅ obj i))
                ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩) :
          (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩))
succ₁ :
  ∀ (i : ℕ) (hi : i + 1 < n + 1),
    Eq (α := obj (⟨i + 1, hi⟩ : Fin (n + 1)).castSucc ⟶ obj ⟨i + 1, hi⟩.succ) (mapSucc ⟨i + 1, hi⟩)
      (CategoryStruct.comp (Y := (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj ⟨i + 1, ⋯⟩)
        (Iso.inv
            ((fun (i : Fin (n + 1 + 1)) ↦
                (match (motive := (i : Fin (n + 1 + 1)) → (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj i ≅ obj i) i with
                  | ⟨0, ⋯⟩ => Iso.refl ((F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj 0)
                  | ⟨i.succ, hi⟩ => e ⟨i, ⋯⟩ :
                  (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj i ≅ obj i))
              ⟨i + 1, ⋯⟩) :
          obj (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj ⟨i + 1, ⋯⟩)
        ((F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).map' (i + 1) (i + 1 + 1) ⋯ hi ≫
            Iso.hom
              ((fun (i : Fin (n + 1 + 1)) ↦
                  (match (motive := (i : Fin (n + 1 + 1)) → (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj i ≅ obj i)
                      i with
                    | ⟨0, ⋯⟩ => Iso.refl ((F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj 0)
                    | ⟨i.succ, hi⟩ => e ⟨i, ⋯⟩ :
                    (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj i ≅ obj i))
                ⟨i + 1 + 1, ⋯⟩) :
          (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ obj ⟨i + 1 + 1, ⋯⟩))
⊢ Eq (α := obj (⟨i, hi⟩ : Fin (n + 1)).castSucc ⟶ obj ⟨i, hi⟩.succ) (mapSucc ⟨i, hi⟩)
    (Iso.inv
        ((fun (i : Fin (n + 1 + 1)) ↦
            (match (motive := (i : Fin (n + 1 + 1)) → (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj i ≅ obj i) i with
              | ⟨0, ⋯⟩ => Iso.refl ((F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj 0)
              | ⟨i.succ, hi⟩ => e ⟨i, ⋯⟩ :
              (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj i ≅ obj i))
          ⟨i, ⋯⟩) ≫
      (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).map' i (i + 1) ⋯ hi ≫
        Iso.hom
          ((fun (i : Fin (n + 1 + 1)) ↦
              (match (motive := (i : Fin (n + 1 + 1)) → (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj i ≅ obj i) i with
                | ⟨0, ⋯⟩ => Iso.refl ((F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj 0)
                | ⟨i.succ, hi⟩ => e (⟨i, ⋯⟩ : Fin (n + 1)) :
                (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj i ≅ obj i))
            (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1))))

Tactic:
obtain _ | i := i