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 : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
i j : ℕ
hi : i + 1 < n + 1 + 1
hj : j + 1 < n + 1 + 1
hij : i + 1 ≤ j + 1
⊢ Eq (α := obj F X (⟨i + 1, hi⟩ : Fin (n + 1 + 1)) ⟶ obj F X ⟨j + 1, hj⟩) (map F f ⟨i + 1, hi⟩ ⟨j + 1, hj⟩ hij)
    (F.map' i j ⋯ ⋯)

Tactic:
rfl

Premises used: CategoryTheory.ComposableArrows.Precomp.map, rfl
-- 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
X : C
f : X ⟶ F.left
j : ℕ
hj : j + 1 < n + 1 + 1
⊢ 1 ≤ (⟨j + 1, hj⟩ : Fin (n + 1 + 1))

Tactic:
simp [Fin.le_def]

Premises used: Fin.le_def
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
j : ℕ
hj : j + 1 < n + 1 + 1
⊢ map F f 1 (⟨j + 1, hj⟩ : Fin (n + 1 + 1)) ⋯ = F.map' 0 j ⋯ ⋯

Tactic:
rfl

Premises used: CategoryTheory.ComposableArrows.Precomp.map, rfl
-- 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
X : C
f : X ⟶ F.left
i : Fin (n + 1 + 1)
⊢ i ≤ i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
i : Fin (n + 1 + 1)
zero : ∀ (hi : 0 < n + 1 + 1), map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨0, hi⟩ : Fin (n + 1 + 1)) ⋯ = 𝟙 (obj F X ⟨0, hi⟩)
succ :
  ∀ (n_1 : ℕ) (hi : n_1 + 1 < n + 1 + 1),
    map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) ⋯ = 𝟙 (obj F X ⟨n_1 + 1, hi⟩)
⊢ map F f i i ⋯ = 𝟙 (obj F X i)

Tactic:
obtain ⟨_ | _, hi⟩ := i
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
⊢ map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨0, hi⟩ : Fin (n + 1 + 1)) ⋯ = 𝟙 (obj F X ⟨0, hi⟩)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
n_1 : ℕ
hi : n_1 + 1 < n + 1 + 1
⊢ map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) ⋯ = 𝟙 (obj F X ⟨n_1 + 1, hi⟩)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
i j k : Fin (n + 1 + 1)
hij : i ≤ j
hjk : j ≤ k
obtain :
  ∀ (i : ℕ) (hi : i < n + 1 + 1) (hij : (⟨i, hi⟩ : Fin (n + 1 + 1)) ≤ j),
    map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) k ⋯ = map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) j hij ≫ map F f j k hjk
⊢ map F f i k ⋯ = map F f i j hij ≫ map F f j k hjk

Tactic:
obtain ⟨i, hi⟩ := i
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
j k : Fin (n + 1 + 1)
hjk : j ≤ k
i : ℕ
hi : i < n + 1 + 1
hij : (⟨i, hi⟩ : Fin (n + 1 + 1)) ≤ j
obtain :
  ∀ (j : ℕ) (hj : j < n + 1 + 1) (hjk : (⟨j, hj⟩ : Fin (n + 1 + 1)) ≤ k) (hij : (⟨i, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j, hj⟩),
    map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) k ⋯ =
      map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) (⟨j, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j, hj⟩ k hjk
⊢ map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) k ⋯ = map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) j hij ≫ map F f j k hjk

Tactic:
obtain ⟨j, hj⟩ := j
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
k : Fin (n + 1 + 1)
i : ℕ
hi : i < n + 1 + 1
j : ℕ
hj : j < n + 1 + 1
hjk : (⟨j, hj⟩ : Fin (n + 1 + 1)) ≤ k
hij : (⟨i, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j, hj⟩
obtain :
  ∀ (k : ℕ) (hk : k < n + 1 + 1) (hjk : (⟨j, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩),
    map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) (⟨k, hk⟩ : Fin (n + 1 + 1)) ⋯ =
      map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) (⟨j, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j, hj⟩ ⟨k, hk⟩ hjk
⊢ map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) k ⋯ =
    map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) (⟨j, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j, hj⟩ k hjk

Tactic:
obtain ⟨k, hk⟩ := k
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
i : ℕ
hi : i < n + 1 + 1
j : ℕ
hj : j < n + 1 + 1
hij : (⟨i, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j, hj⟩
k : ℕ
hk : k < n + 1 + 1
hjk : (⟨j, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩
zero :
  ∀ (hi : 0 < n + 1 + 1) (hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j, hj⟩),
    map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨k, hk⟩ : Fin (n + 1 + 1)) ⋯ =
      map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨j, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j, hj⟩ ⟨k, hk⟩ hjk
succ :
  ∀ (n_1 : ℕ) (hi : n_1 + 1 < n + 1 + 1) (hij : (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j, hj⟩),
    map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨k, hk⟩ : Fin (n + 1 + 1)) ⋯ =
      map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨j, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j, hj⟩ ⟨k, hk⟩ hjk
⊢ map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) (⟨k, hk⟩ : Fin (n + 1 + 1)) ⋯ =
    map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) (⟨j, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j, hj⟩ ⟨k, hk⟩ hjk

Tactic:
cases i
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
j : ℕ
hj : j < n + 1 + 1
k : ℕ
hk : k < n + 1 + 1
hjk : (⟨j, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩
hi : 0 < n + 1 + 1
hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j, hj⟩
zero :
  ∀ (hj : 0 < n + 1 + 1) (hjk : (⟨0, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩) (hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨0, hj⟩),
    map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨k, hk⟩ : Fin (n + 1 + 1)) ⋯ =
      map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨0, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨0, hj⟩ ⟨k, hk⟩ hjk
zero₁ :
  ∀ (hj : HAdd.hAdd (α := ℕ) 0 1 < n + 1 + 1) (hjk : (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩)
    (hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩),
    map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨k, hk⟩ : Fin (n + 1 + 1)) ⋯ =
      map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
        map F f ⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ ⟨k, hk⟩ hjk
zero₂ :
  ∀ (j : ℕ) (hj : j + 1 + 1 < n + 1 + 1) (hjk : (⟨j + 1 + 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩)
    (hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j + 1 + 1, hj⟩),
    map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨k, hk⟩ : Fin (n + 1 + 1)) ⋯ =
      map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨j + 1 + 1, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j + 1 + 1, hj⟩ ⟨k, hk⟩ hjk
⊢ map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨k, hk⟩ : Fin (n + 1 + 1)) ⋯ =
    map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨j, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j, hj⟩ ⟨k, hk⟩ hjk

Tactic:
obtain _ | _ | j := j
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
k : ℕ
hk : k < n + 1 + 1
hi hj : 0 < n + 1 + 1
hjk : (⟨0, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩
hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨0, hj⟩
zero : map F f 0 (⟨k, hk⟩ : Fin (n + 1 + 1)) ⋯ = 𝟙 X ≫ map F f 0 (⟨k, hk⟩ : Fin (n + 1 + 1)) hjk
⊢ map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨k, hk⟩ : Fin (n + 1 + 1)) ⋯ =
    map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨0, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨0, hj⟩ ⟨k, hk⟩ hjk

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
k : ℕ
hk : k < n + 1 + 1
hi hj : 0 < n + 1 + 1
hjk : (⟨0, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩
hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨0, hj⟩
zero zero₁ : map F f 0 (⟨k, hk⟩ : Fin (n + 1 + 1)) ⋯ = map F f 0 ⟨k, hk⟩ hjk
⊢ map F f 0 (⟨k, hk⟩ : Fin (n + 1 + 1)) ⋯ = 𝟙 X ≫ map F f 0 (⟨k, hk⟩ : Fin (n + 1 + 1)) hjk

Tactic:
rw [id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
k : ℕ
hk : k < n + 1 + 1
hi : 0 < n + 1 + 1
hj : HAdd.hAdd (α := ℕ) 0 1 < n + 1 + 1
hjk : (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩
hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩
zero :
  ∀ (hk : 0 < n + 1 + 1) (hjk : (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨0, hk⟩),
    map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨0, hk⟩ : Fin (n + 1 + 1)) ⋯ =
      map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
        map F f ⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ ⟨0, hk⟩ hjk
zero₁ :
  ∀ (hk : HAdd.hAdd (α := ℕ) 0 1 < n + 1 + 1)
    (hjk : (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨HAdd.hAdd (α := ℕ) 0 1, hk⟩),
    map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨HAdd.hAdd (α := ℕ) 0 1, hk⟩ : Fin (n + 1 + 1)) ⋯ =
      map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
        map F f ⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ ⟨HAdd.hAdd (α := ℕ) 0 1, hk⟩ hjk
zero₂ :
  ∀ (k : ℕ) (hk : k + 1 + 1 < n + 1 + 1) (hjk : (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k + 1 + 1, hk⟩),
    map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨k + 1 + 1, hk⟩ : Fin (n + 1 + 1)) ⋯ =
      map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
        map F f ⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ ⟨k + 1 + 1, hk⟩ hjk
⊢ map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨k, hk⟩ : Fin (n + 1 + 1)) ⋯ =
    map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
      map F f ⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ ⟨k, hk⟩ hjk

Tactic:
obtain _ | _ | k := k
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
hj : HAdd.hAdd (α := ℕ) 0 1 < n + 1 + 1
hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩
hk : 0 < n + 1 + 1
hjk : (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨0, hk⟩
⊢ map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨0, hk⟩ : Fin (n + 1 + 1)) ⋯ =
    map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
      map F f ⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ ⟨0, hk⟩ hjk

Tactic:
simp at hjk
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
hj : HAdd.hAdd (α := ℕ) 0 1 < n + 1 + 1
hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩
hk : HAdd.hAdd (α := ℕ) 0 1 < n + 1 + 1
hjk : (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨HAdd.hAdd (α := ℕ) 0 1, hk⟩
⊢ map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨HAdd.hAdd (α := ℕ) 0 1, hk⟩ : Fin (n + 1 + 1)) ⋯ =
    map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
      map F f ⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ ⟨HAdd.hAdd (α := ℕ) 0 1, hk⟩ hjk

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
hj : HAdd.hAdd (α := ℕ) 0 1 < n + 1 + 1
hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩
k : ℕ
hk : k + 1 + 1 < n + 1 + 1
hjk : (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k + 1 + 1, hk⟩
⊢ map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨k + 1 + 1, hk⟩ : Fin (n + 1 + 1)) ⋯ =
    map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
      map F f ⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ ⟨k + 1 + 1, hk⟩ hjk

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
k : ℕ
hk : k < n + 1 + 1
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hjk : (⟨j + 1 + 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩
hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j + 1 + 1, hj⟩
zero :
  ∀ (hk : 0 < n + 1 + 1) (hjk : (⟨j + 1 + 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨0, hk⟩),
    map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨0, hk⟩ : Fin (n + 1 + 1)) ⋯ =
      map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨j + 1 + 1, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j + 1 + 1, hj⟩ ⟨0, hk⟩ hjk
zero₁ :
  ∀ (hk : HAdd.hAdd (α := ℕ) 0 1 < n + 1 + 1)
    (hjk : (⟨j + 1 + 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨HAdd.hAdd (α := ℕ) 0 1, hk⟩),
    map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨HAdd.hAdd (α := ℕ) 0 1, hk⟩ : Fin (n + 1 + 1)) ⋯ =
      map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨j + 1 + 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
        map F f ⟨j + 1 + 1, hj⟩ ⟨HAdd.hAdd (α := ℕ) 0 1, hk⟩ hjk
zero₂ :
  ∀ (k : ℕ) (hk : k + 1 + 1 < n + 1 + 1) (hjk : (⟨j + 1 + 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k + 1 + 1, hk⟩),
    map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨k + 1 + 1, hk⟩ : Fin (n + 1 + 1)) ⋯ =
      map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨j + 1 + 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
        map F f ⟨j + 1 + 1, hj⟩ ⟨k + 1 + 1, hk⟩ hjk
⊢ map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨k, hk⟩ : Fin (n + 1 + 1)) ⋯ =
    map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨j + 1 + 1, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j + 1 + 1, hj⟩ ⟨k, hk⟩ hjk

Tactic:
obtain _ | _ | k := k
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j + 1 + 1, hj⟩
hk : 0 < n + 1 + 1
hjk : (⟨j + 1 + 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨0, hk⟩
⊢ map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨0, hk⟩ : Fin (n + 1 + 1)) ⋯ =
    map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨j + 1 + 1, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j + 1 + 1, hj⟩ ⟨0, hk⟩ hjk

Tactic:
simp [Fin.ext_iff] at hjk

Premises used: Fin.ext_iff
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j + 1 + 1, hj⟩
hk : HAdd.hAdd (α := ℕ) 0 1 < n + 1 + 1
hjk : (⟨j + 1 + 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨HAdd.hAdd (α := ℕ) 0 1, hk⟩
⊢ map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨HAdd.hAdd (α := ℕ) 0 1, hk⟩ : Fin (n + 1 + 1)) ⋯ =
    map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨j + 1 + 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
      map F f ⟨j + 1 + 1, hj⟩ ⟨HAdd.hAdd (α := ℕ) 0 1, hk⟩ hjk

Tactic:
simp [Fin.le_def] at hjk

Premises used: Fin.le_def
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j + 1 + 1, hj⟩
k : ℕ
hk : k + 1 + 1 < n + 1 + 1
hjk : (⟨j + 1 + 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k + 1 + 1, hk⟩
zero : f ≫ F.map (homOfLE ⋯) = (f ≫ F.map (homOfLE ⋯)) ≫ F.map (homOfLE ⋯)
⊢ map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨k + 1 + 1, hk⟩ : Fin (n + 1 + 1)) ⋯ =
    map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨j + 1 + 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
      map F f ⟨j + 1 + 1, hj⟩ ⟨k + 1 + 1, hk⟩ hjk

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j + 1 + 1, hj⟩
k : ℕ
hk : k + 1 + 1 < n + 1 + 1
hjk : (⟨j + 1 + 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k + 1 + 1, hk⟩
zero : f ≫ F.map (homOfLE ⋯) = f ≫ F.map (homOfLE ⋯) ≫ F.map (homOfLE ⋯)
zero₁ : f ≫ F.map (homOfLE ⋯) = f ≫ F.map (homOfLE ⋯ ≫ homOfLE ⋯)
zero₂ zero₃ : f ≫ F.map (homOfLE ⋯) = f ≫ F.map (homOfLE ⋯)
⊢ f ≫ F.map (homOfLE ⋯) = (f ≫ F.map (homOfLE ⋯)) ≫ F.map (homOfLE ⋯)

Tactic:
rw [assoc, ← F.map_comp, homOfLE_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.homOfLE_comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
j : ℕ
hj : j < n + 1 + 1
k : ℕ
hk : k < n + 1 + 1
hjk : (⟨j, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩
n_1 : ℕ
hi : n_1 + 1 < n + 1 + 1
hij : (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j, hj⟩
succ :
  ∀ (hj : 0 < n + 1 + 1) (hjk : (⟨0, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩)
    (hij : (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨0, hj⟩),
    map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨k, hk⟩ : Fin (n + 1 + 1)) ⋯ =
      map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨0, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨0, hj⟩ ⟨k, hk⟩ hjk
succ₁ :
  ∀ (j : ℕ) (hj : j + 1 < n + 1 + 1) (hjk : (⟨j + 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩)
    (hij : (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j + 1, hj⟩),
    map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨k, hk⟩ : Fin (n + 1 + 1)) ⋯ =
      map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨j + 1, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j + 1, hj⟩ ⟨k, hk⟩ hjk
⊢ map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨k, hk⟩ : Fin (n + 1 + 1)) ⋯ =
    map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨j, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j, hj⟩ ⟨k, hk⟩ hjk

Tactic:
obtain _ | j := j
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
k : ℕ
hk : k < n + 1 + 1
n_1 : ℕ
hi : n_1 + 1 < n + 1 + 1
hj : 0 < n + 1 + 1
hjk : (⟨0, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩
hij : (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨0, hj⟩
⊢ map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨k, hk⟩ : Fin (n + 1 + 1)) ⋯ =
    map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨0, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨0, hj⟩ ⟨k, hk⟩ hjk

Tactic:
simp [Fin.ext_iff] at hij

Premises used: Fin.ext_iff
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
k : ℕ
hk : k < n + 1 + 1
n_1 : ℕ
hi : n_1 + 1 < n + 1 + 1
j : ℕ
hj : j + 1 < n + 1 + 1
hjk : (⟨j + 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩
hij : (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j + 1, hj⟩
succ :
  ∀ (hk : 0 < n + 1 + 1) (hjk : (⟨j + 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨0, hk⟩),
    map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨0, hk⟩ : Fin (n + 1 + 1)) ⋯ =
      map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨j + 1, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j + 1, hj⟩ ⟨0, hk⟩ hjk
succ₁ :
  ∀ (k : ℕ) (hk : k + 1 < n + 1 + 1) (hjk : (⟨j + 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k + 1, hk⟩),
    map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨k + 1, hk⟩ : Fin (n + 1 + 1)) ⋯ =
      map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨j + 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
        map F f ⟨j + 1, hj⟩ ⟨k + 1, hk⟩ hjk
⊢ map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨k, hk⟩ : Fin (n + 1 + 1)) ⋯ =
    map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨j + 1, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j + 1, hj⟩ ⟨k, hk⟩ hjk

Tactic:
obtain _ | k := k
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
n_1 : ℕ
hi : n_1 + 1 < n + 1 + 1
j : ℕ
hj : j + 1 < n + 1 + 1
hij : (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j + 1, hj⟩
hk : 0 < n + 1 + 1
hjk : (⟨j + 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨0, hk⟩
⊢ map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨0, hk⟩ : Fin (n + 1 + 1)) ⋯ =
    map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨j + 1, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j + 1, hj⟩ ⟨0, hk⟩ hjk

Tactic:
simp [Fin.ext_iff] at hjk

Premises used: Fin.ext_iff
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
n_1 : ℕ
hi : n_1 + 1 < n + 1 + 1
j : ℕ
hj : j + 1 < n + 1 + 1
hij : (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j + 1, hj⟩
k : ℕ
hk : k + 1 < n + 1 + 1
hjk : (⟨j + 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k + 1, hk⟩
succ :
  Eq (α := F.obj (⟨n_1, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, ⋯⟩)
    (F.map (homOfLE ⋯) : F.obj (⟨n_1, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, ⋯⟩)
    (F.map (homOfLE ⋯) ≫ F.map (homOfLE ⋯) : F.obj (⟨n_1, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, ⋯⟩)
⊢ map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨k + 1, hk⟩ : Fin (n + 1 + 1)) ⋯ =
    map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨j + 1, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j + 1, hj⟩ ⟨k + 1, hk⟩ hjk

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
n_1 : ℕ
hi : n_1 + 1 < n + 1 + 1
j : ℕ
hj : j + 1 < n + 1 + 1
hij : (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j + 1, hj⟩
k : ℕ
hk : k + 1 < n + 1 + 1
hjk : (⟨j + 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k + 1, hk⟩
succ :
  Eq (α := F.obj (⟨n_1, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, ⋯⟩)
    (F.map (homOfLE ⋯) : F.obj (⟨n_1, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, ⋯⟩)
    (F.map (homOfLE ⋯ ≫ homOfLE ⋯) : F.obj (⟨n_1, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, ⋯⟩)
succ₁ succ₂ :
  Eq (α := F.obj (⟨n_1, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, ⋯⟩)
    (F.map (homOfLE ⋯) : F.obj (⟨n_1, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, ⋯⟩)
    (F.map (homOfLE ⋯) : F.obj (⟨n_1, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, ⋯⟩)
⊢ Eq (α := F.obj (⟨n_1, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, ⋯⟩)
    (F.map (homOfLE ⋯) : F.obj (⟨n_1, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, ⋯⟩)
    (F.map (homOfLE ⋯) ≫ F.map (homOfLE ⋯) : F.obj (⟨n_1, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, ⋯⟩)

Tactic:
rw [← F.map_comp, homOfLE_comp]

Premises used: CategoryTheory.homOfLE_comp, CategoryTheory.Functor.map_comp
-- 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
X₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₂ f g).map' 0 1 ⋯ ⋯ = f

Tactic:
dsimp
-- 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
X₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₂ f g).map' 1 2 ⋯ ⋯ = g

Tactic:
dsimp
-- 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
X₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₂ f g).map' 0 2 ⋯ ⋯ = f ≫ g

Tactic:
dsimp
-- 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
X₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₂ f g).hom = f ≫ g

Tactic:
dsimp
-- 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
X₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ Eq (α := (mk₂ f g).obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ (mk₂ f g).obj ⟨0, ⋯⟩)
    ((mk₂ f g).map' 0 0 ⋯ ⋯ : (mk₂ f g).obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ (mk₂ f g).obj ⟨0, ⋯⟩)
    (𝟙 ((mk₂ f g).obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) :
      (mk₂ f g).obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ (mk₂ f g).obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))

Tactic:
dsimp
-- 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
X₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ Eq (α := (mk₂ f g).obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ (mk₂ f g).obj ⟨1, ⋯⟩)
    ((mk₂ f g).map' 1 1 ⋯ ⋯ : (mk₂ f g).obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ (mk₂ f g).obj ⟨1, ⋯⟩)
    (𝟙 ((mk₂ f g).obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) :
      (mk₂ f g).obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ (mk₂ f g).obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))

Tactic:
dsimp