-- 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.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

Tactic:
exact h i (by valid)

Result:
no goals

Proof state:
case zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
obj : Fin (0 + 1) → C
mapSucc✝ : (i : Fin 0) → obj i.castSucc ⟶ obj i.succ
⊢ ∃ F e, ∀ (i : ℕ) (hi : i < 0), mapSucc✝ ⟨i, hi⟩ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom

Tactic:
exact ⟨mk₀ (obj 0), fun 0 => Iso.refl _, fun i hi => by simp at hi⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
⊢ ∀ (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

Tactic:
induction' n with n hn

Result:
case zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
⊢ ∀ (obj : Fin (0 + 1) → C) (mapSucc : (i : Fin 0) → obj i.castSucc ⟶ obj i.succ),
    ∃ F e, ∀ (i : ℕ) (hi : i < 0), mapSucc ⟨i, hi⟩ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom

case 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 e, ∀ (i : ℕ) (hi : i < n + 1), mapSucc ⟨i, hi⟩ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
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

Tactic:
revert obj mapSucc

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
⊢ ∀ (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

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
obj : Fin (0 + 1) → C
mapSucc✝ : (i : Fin 0) → obj i.castSucc ⟶ obj i.succ
i : ℕ
hi : i < 0
⊢ mapSucc✝ ⟨i, hi⟩ =
    ((fun x =>
            match x with
            | 0 => Iso.refl ((mk₀ (obj 0)).obj 0))
          ⟨i, ⋯⟩).inv ≫
      (mk₀ (obj 0)).map' i (i + 1) ⋯ hi ≫
        ((fun x =>
              match x with
              | 0 => Iso.refl ((mk₀ (obj 0)).obj 0))
            ⟨i + 1, ⋯⟩).hom

Tactic:
simp at hi

Result:
no goals

Proof state:
case 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 e, ∀ (i : ℕ) (hi : i < n + 1), mapSucc ⟨i, hi⟩ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom

Tactic:
obtain ⟨F, e, h⟩ := hn (fun i => obj i.succ) (fun i => mapSucc i.succ)

Result:
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
⊢ ∃ F e, ∀ (i : ℕ) (hi : i < n + 1), mapSucc ⟨i, hi⟩ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom

Proof state:
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 =
    (match 0 with
        | ⟨0, ⋯⟩ => Iso.refl (obj 0)
        | ⟨i.succ, hi⟩ => e ⟨i, ⋯⟩).inv ≫
      mapSucc 0

Tactic:
erw [id_comp]

Result:
no goals