-- Mathlib/CategoryTheory/ComposableArrows.lean
lemma mkOfObjOfMapSucc_exists : ∃ (F : ComposableArrows C n) (e : ∀ i, F.obj i ≅ obj i),
    ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩ =
      (e ⟨i, _⟩).inv ≫ F.map' i (i + 1) ≫ (e ⟨i + 1, _⟩).hom

Proof state:
case succ.intro.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
hn :
  ∀ (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ),
    ∃ F e, ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom
obj : Fin (n + 1 + 1) → C
mapSucc : (i : Fin (n + 1)) → obj i.castSucc ⟶ obj i.succ
F : ComposableArrows C n
e : (i : Fin (n + 1)) → F.obj i ≅ obj i.succ
h : ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩.succ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom
i : ℕ
hi : i < n + 1
⊢ mapSucc ⟨i, hi⟩ =
    ((fun i =>
            match i with
            | ⟨0, ⋯⟩ => Iso.refl ((F.precomp (mapSucc 0 ≫ (e 0).inv)).obj 0)
            | ⟨i.succ, hi⟩ => e ⟨i, ⋯⟩)
          ⟨i, ⋯⟩).inv ≫
      (F.precomp (mapSucc 0 ≫ (e 0).inv)).map' i (i + 1) ⋯ hi ≫
        ((fun i =>
              match i with
              | ⟨0, ⋯⟩ => Iso.refl ((F.precomp (mapSucc 0 ≫ (e 0).inv)).obj 0)
              | ⟨i.succ, hi⟩ => e ⟨i, ⋯⟩)
            ⟨i + 1, ⋯⟩).hom

Tactic:
obtain _ | i := i

Result:
case succ.intro.intro.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
hn :
  ∀ (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ),
    ∃ F e, ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom
obj : Fin (n + 1 + 1) → C
mapSucc : (i : Fin (n + 1)) → obj i.castSucc ⟶ obj i.succ
F : ComposableArrows C n
e : (i : Fin (n + 1)) → F.obj i ≅ obj i.succ
h : ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩.succ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom
hi : 0 < n + 1
⊢ mapSucc ⟨0, hi⟩ =
    ((fun i =>
            match i with
            | ⟨0, ⋯⟩ => Iso.refl ((F.precomp (mapSucc 0 ≫ (e 0).inv)).obj 0)
            | ⟨i.succ, hi⟩ => e ⟨i, ⋯⟩)
          ⟨0, ⋯⟩).inv ≫
      (F.precomp (mapSucc 0 ≫ (e 0).inv)).map' 0 (0 + 1) ⋯ hi ≫
        ((fun i =>
              match i with
              | ⟨0, ⋯⟩ => Iso.refl ((F.precomp (mapSucc 0 ≫ (e 0).inv)).obj 0)
              | ⟨i.succ, hi⟩ => e ⟨i, ⋯⟩)
            ⟨0 + 1, ⋯⟩).hom

case succ.intro.intro.succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
hn :
  ∀ (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ),
    ∃ F e, ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom
obj : Fin (n + 1 + 1) → C
mapSucc : (i : Fin (n + 1)) → obj i.castSucc ⟶ obj i.succ
F : ComposableArrows C n
e : (i : Fin (n + 1)) → F.obj i ≅ obj i.succ
h : ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩.succ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom
i : ℕ
hi : i + 1 < n + 1
⊢ mapSucc ⟨i + 1, hi⟩ =
    ((fun i =>
            match i with
            | ⟨0, ⋯⟩ => Iso.refl ((F.precomp (mapSucc 0 ≫ (e 0).inv)).obj 0)
            | ⟨i.succ, hi⟩ => e ⟨i, ⋯⟩)
          ⟨i + 1, ⋯⟩).inv ≫
      (F.precomp (mapSucc 0 ≫ (e 0).inv)).map' (i + 1) (i + 1 + 1) ⋯ hi ≫
        ((fun i =>
              match i with
              | ⟨0, ⋯⟩ => Iso.refl ((F.precomp (mapSucc 0 ≫ (e 0).inv)).obj 0)
              | ⟨i.succ, hi⟩ => e ⟨i, ⋯⟩)
            ⟨i + 1 + 1, ⋯⟩).hom