awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 5
app₀ : f.obj' 0 _proof_83 ≅ g.obj' 0 _proof_83
app₁ : f.obj' 1 _proof_84 ≅ g.obj' 1 _proof_84
app₂ : f.obj' 2 _proof_85 ≅ g.obj' 2 _proof_85
app₃ : f.obj' 3 _proof_86 ≅ g.obj' 3 _proof_86
app₄ : f.obj' 4 _proof_87 ≅ g.obj' 4 _proof_87
app₅ : f.obj' 5 _proof_88 ≅ g.obj' 5 _proof_88
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_84 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_84
w₁ : f.map' 1 2 _proof_8 _proof_85 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_85
w₂ : f.map' 2 3 _proof_25 _proof_86 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_86
w₃ : f.map' 3 4 _proof_50 _proof_87 ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_50 _proof_87
w₄ : f.map' 4 5 _proof_87 _proof_88 ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_87 _proof_88
⊢ HAdd.hAdd (α := ℕ) 4 1 ≤ 5

Tactic:
valid
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 5
app₀ : f.obj' 0 _proof_83 ≅ g.obj' 0 _proof_83
app₁ : f.obj' 1 _proof_84 ≅ g.obj' 1 _proof_84
app₂ : f.obj' 2 _proof_85 ≅ g.obj' 2 _proof_85
app₃ : f.obj' 3 _proof_86 ≅ g.obj' 3 _proof_86
app₄ : f.obj' 4 _proof_87 ≅ g.obj' 4 _proof_87
app₅ : f.obj' 5 _proof_88 ≅ g.obj' 5 _proof_88
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_84 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_84
w₁ : f.map' 1 2 _proof_8 _proof_85 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_85
w₂ : f.map' 2 3 _proof_25 _proof_86 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_86
w₃ : f.map' 3 4 _proof_50 _proof_87 ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_50 _proof_87
w₄ : f.map' 4 5 _proof_87 _proof_88 ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_87 _proof_88
rw rw₁ : app₄.inv ≫ f.map' 4 (HAdd.hAdd (α := ℕ) 4 1) ⋯ ⋯ = app₄.inv ≫ f.map' 4 5 _proof_87 _proof_88
⊢ g.map' 4 5 _proof_87 _proof_88 ≫ app₅.inv = app₄.inv ≫ f.map' 4 5 _proof_87 _proof_88

Tactic:
rw [map'_inv_eq_inv_map' (by valid) app₄ app₅ w₄]

Premises used: CategoryTheory.ComposableArrows.map'_inv_eq_inv_map'
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
f g : ComposableArrows.{v_1, u_1} C 5
h₀ : f.obj' 0 _proof_83 = g.obj' 0 _proof_83
h₁ : f.obj' 1 _proof_84 = g.obj' 1 _proof_84
h₂ : f.obj' 2 _proof_85 = g.obj' 2 _proof_85
h₃ : f.obj' 3 _proof_86 = g.obj' 3 _proof_86
h₄ : f.obj' 4 _proof_87 = g.obj' 4 _proof_87
h₅ : f.obj' 5 _proof_88 = g.obj' 5 _proof_88
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_84 = eqToHom h₀ ≫ g.map' 0 1 homMk₁._proof_2 _proof_84 ≫ eqToHom ⋯
w₁ : f.map' 1 2 _proof_8 _proof_85 = eqToHom h₁ ≫ g.map' 1 2 _proof_8 _proof_85 ≫ eqToHom ⋯
w₂ : f.map' 2 3 _proof_25 _proof_86 = eqToHom h₂ ≫ g.map' 2 3 _proof_25 _proof_86 ≫ eqToHom ⋯
w₃ : f.map' 3 4 _proof_50 _proof_87 = eqToHom h₃ ≫ g.map' 3 4 _proof_50 _proof_87 ≫ eqToHom ⋯
w₄ : f.map' 4 5 _proof_87 _proof_88 = eqToHom h₄ ≫ g.map' 4 5 _proof_87 _proof_88 ≫ eqToHom ⋯
⊢ f = g

Tactic:
ext_succ h₀ (ext₄ h₁ h₂ h₃ h₄ h₅ w₁ w₂ w₃ w₄) w₀

Premises used: CategoryTheory.ComposableArrows.ext₄, CategoryTheory.ComposableArrows.ext_succ
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ComposableArrows.{v_1, u_1} C 5
⊢ X.map' 0 1 homMk₁._proof_2 _proof_84 =
    eqToHom ⋯ ≫
      (mk₅ (X₀ := X.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1))) (X₁ := X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X₂ := X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1))) (X₃ :=
              X.obj (⟨3, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1))) (X₄ := X.obj (⟨4, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 0 1 ⋯ ⋯ :
                X.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 1 2 ⋯ ⋯ :
                X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 2 3 ⋯ ⋯ :
                X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨3, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 3 4 ⋯ ⋯ :
                X.obj (⟨3, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨4, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 4 5 ⋯ ⋯ :
                X.obj (⟨4, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨5, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))).map'
          0 1 homMk₁._proof_2 _proof_84 ≫
        eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ComposableArrows.{v_1, u_1} C 5
⊢ X.map' 1 2 _proof_8 _proof_85 =
    eqToHom ⋯ ≫
      (mk₅ (X₀ := X.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1))) (X₁ := X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X₂ := X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1))) (X₃ :=
              X.obj (⟨3, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1))) (X₄ := X.obj (⟨4, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 0 1 ⋯ ⋯ :
                X.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 1 2 ⋯ ⋯ :
                X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 2 3 ⋯ ⋯ :
                X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨3, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 3 4 ⋯ ⋯ :
                X.obj (⟨3, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨4, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 4 5 ⋯ ⋯ :
                X.obj (⟨4, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨5, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))).map'
          1 2 _proof_8 _proof_85 ≫
        eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ComposableArrows.{v_1, u_1} C 5
⊢ X.map' 2 3 _proof_25 _proof_86 =
    eqToHom ⋯ ≫
      (mk₅ (X₀ := X.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1))) (X₁ := X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X₂ := X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1))) (X₃ :=
              X.obj (⟨3, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1))) (X₄ := X.obj (⟨4, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 0 1 ⋯ ⋯ :
                X.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 1 2 ⋯ ⋯ :
                X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 2 3 ⋯ ⋯ :
                X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨3, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 3 4 ⋯ ⋯ :
                X.obj (⟨3, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨4, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 4 5 ⋯ ⋯ :
                X.obj (⟨4, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨5, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))).map'
          2 3 _proof_25 _proof_86 ≫
        eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ComposableArrows.{v_1, u_1} C 5
⊢ X.map' 3 4 _proof_50 _proof_87 =
    eqToHom ⋯ ≫
      (mk₅ (X₀ := X.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1))) (X₁ := X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X₂ := X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1))) (X₃ :=
              X.obj (⟨3, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1))) (X₄ := X.obj (⟨4, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 0 1 ⋯ ⋯ :
                X.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 1 2 ⋯ ⋯ :
                X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 2 3 ⋯ ⋯ :
                X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨3, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 3 4 ⋯ ⋯ :
                X.obj (⟨3, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨4, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 4 5 ⋯ ⋯ :
                X.obj (⟨4, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨5, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))).map'
          3 4 _proof_50 _proof_87 ≫
        eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ComposableArrows.{v_1, u_1} C 5
⊢ X.map' 4 5 _proof_87 _proof_88 =
    eqToHom ⋯ ≫
      (mk₅ (X₀ := X.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1))) (X₁ := X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X₂ := X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1))) (X₃ :=
              X.obj (⟨3, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1))) (X₄ := X.obj (⟨4, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 0 1 ⋯ ⋯ :
                X.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 1 2 ⋯ ⋯ :
                X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 2 3 ⋯ ⋯ :
                X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨3, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 3 4 ⋯ ⋯ :
                X.obj (⟨3, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨4, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))
              (X.map' 4 5 ⋯ ⋯ :
                X.obj (⟨4, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)) ⟶ X.obj (⟨5, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 5 1)))).map'
          4 5 _proof_87 _proof_88 ≫
        eqToHom ⋯

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

Tactic:
simp at hi
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
obj : Fin (HAdd.hAdd (α := ℕ) 0 1) → C
mapSucc : (i : Fin 0) → obj i.castSucc ⟶ obj i.succ
⊢ ∃ (F : ComposableArrows.{v_1, u_1} C 0) (e : (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) → F.obj i ≅ obj i),
    ∀ (i : ℕ) (hi : i < 0),
      mapSucc ⟨i, hi⟩ =
        Iso.inv (e (⟨i, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1))) ≫
          F.map' i (i + 1) ⋯ hi ≫ Iso.hom (e (⟨i + 1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)))

Tactic:
exact ⟨mk₀ (obj 0), fun 0 => Iso.refl _, fun i hi => by simp at hi⟩
-- 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
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)))),
    ∃ (F : ComposableArrows.{v_1, u_1} C (n + 1)) (e : (i : Fin (n + 1 + 1)) → F.obj i ≅ obj i),
      ∀ (i : ℕ) (hi : i < n + 1),
        mapSucc ⟨i, hi⟩ =
          Iso.inv (e (⟨i, ⋯⟩ : Fin (n + 1 + 1))) ≫ F.map' i (i + 1) ⋯ hi ≫ Iso.hom (e (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)))
⊢ ∃ (F : ComposableArrows.{v_1, u_1} C (n + 1)) (e : (i : Fin (n + 1 + 1)) → F.obj i ≅ obj i),
    ∀ (i : ℕ) (hi : i < n + 1),
      mapSucc ⟨i, hi⟩ =
        Iso.inv (e (⟨i, ⋯⟩ : Fin (n + 1 + 1))) ≫ F.map' i (i + 1) ⋯ hi ≫ Iso.hom (e (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)))

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

Premises used: Fin.succ
-- 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)))
⊢ ∃ (F : ComposableArrows.{v_1, u_1} C (n + 1)) (e : (i : Fin (n + 1 + 1)) → F.obj i ≅ obj i),
    ∀ (i : ℕ) (hi : i < n + 1),
      mapSucc ⟨i, hi⟩ =
        Iso.inv (e (⟨i, ⋯⟩ : Fin (n + 1 + 1))) ≫ F.map' i (i + 1) ⋯ hi ≫ Iso.hom (e (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)))

Tactic:
⟨F.precomp (mapSucc 0 ≫ (e 0).inv), fun i => match i with
      | 0 => Iso.refl _
      | ⟨i + 1, hi⟩ => e _, fun i hi => ?_⟩

Premises used: CategoryTheory.ComposableArrows.Precomp.obj._proof_2, Fin.mk, CategoryTheory.Iso.refl, CategoryTheory.Iso, CategoryTheory.ComposableArrows.obj'._proof_2, CategoryTheory.ComposableArrows.precomp, _private.0.CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_exists.match_2, Exists.intro, CategoryTheory.CategoryStruct.comp, OfNat.ofNat, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj
-- 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)))
succ :
  ∀ (i : ℕ) (hi : i < n + 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))))
⊢ ∃ (F : ComposableArrows.{v_1, u_1} C (n + 1)) (e : (i : Fin (n + 1 + 1)) → F.obj i ≅ obj i),
    ∀ (i : ℕ) (hi : i < n + 1),
      mapSucc ⟨i, hi⟩ =
        Iso.inv (e (⟨i, ⋯⟩ : Fin (n + 1 + 1))) ≫ F.map' i (i + 1) ⋯ hi ≫ Iso.hom (e (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)))

Tactic:
refine ⟨F.precomp (mapSucc 0 ≫ (e 0).inv), fun i => match i with
      | 0 => Iso.refl _
      | ⟨i + 1, hi⟩ => e _, fun i hi => ?_⟩
-- 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)))
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, ⋯⟩))

Tactic:
simp
-- 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 + 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, ⋯⟩))

Tactic:
exact h i (by valid)
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
obj : Fin (n + 1) → C
mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ
zero :
  ∀ (obj : Fin (HAdd.hAdd (α := ℕ) 0 1) → C) (mapSucc : (i : Fin 0) → obj i.castSucc ⟶ obj i.succ),
    ∃ (F : ComposableArrows.{v_1, u_1} C 0) (e : (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) → F.obj i ≅ obj i),
      ∀ (i : ℕ) (hi : i < 0),
        mapSucc ⟨i, hi⟩ =
          Iso.inv (e (⟨i, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1))) ≫
            F.map' i (i + 1) ⋯ hi ≫ Iso.hom (e (⟨i + 1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)))
succ :
  ∀ (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 + 1)) (e : (i : Fin (n + 1 + 1)) → F.obj i ≅ obj i),
      ∀ (i : ℕ) (hi : i < n + 1),
        mapSucc ⟨i, hi⟩ =
          Iso.inv (e (⟨i, ⋯⟩ : Fin (n + 1 + 1))) ≫ F.map' i (i + 1) ⋯ hi ≫ Iso.hom (e (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)))
⊢ ∃ (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)))

Tactic:
induction n with
  | zero => exact ⟨mk₀ (obj 0), fun 0 => Iso.refl _, fun i hi => by simp at hi⟩
  | succ n hn =>
    obtain ⟨F, e, h⟩ := hn (fun i => obj i.succ) (fun i => mapSucc i.succ)
    refine ⟨F.precomp (mapSucc 0 ≫ (e 0).inv), fun i => match i with
      | 0 => Iso.refl _
      | ⟨i + 1, hi⟩ => e _, fun i hi => ?_⟩
    obtain _ | i := i
    · simp
    · exact h i (by valid)
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
obj : Fin (n + 1) → C
mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ
i : Fin (n + 1)
⊢ (mkOfObjOfMapSucc obj mapSucc).obj i = obj i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
obj : Fin (n + 1) → C
mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ
i : ℕ
hi : i < n
⊢ (mkOfObjOfMapSucc obj mapSucc).map' i (i + 1) ⋯ hi = mapSucc ⟨i, hi⟩

Tactic:
((mkOfObjOfMapSucc_exists obj mapSucc).choose_spec.choose_spec i hi).symm

Premises used: Exists.choose_spec, Fin.succ, CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_exists, Eq.symm
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
obj : Fin (n + 1) → C
mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ
i : ℕ
hi : i < n
⊢ ((mkOfObjOfMapSucc obj mapSucc).arrow i hi).hom =
    eqToHom ⋯ ≫ (mk₁ (X₀ := obj (⟨i, hi⟩ : Fin n).castSucc) (mapSucc (⟨i, hi⟩ : Fin n))).hom ≫ eqToHom ⋯

Tactic:
simpa using mkOfObjOfMapSucc_map_succ obj mapSucc i hi

Premises used: CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_map_succ