-- Mathlib/CategoryTheory/ComposableArrows.lean
lemma map_comp {i j k : Fin (n + 1 + 1)} (hij : i ≤ j) (hjk : j ≤ k) :
    map F f i k (hij.trans hjk) = map F f i j hij ≫ map F f j k hjk

Proof state:
case mk.mk.mk.zero.succ.zero.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
hj : 0 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨0 + 1, hj⟩
hk : 0 < n + 1 + 1
hjk : ⟨0 + 1, hj⟩ ≤ ⟨0, hk⟩
⊢ map F f ⟨0, hi⟩ ⟨0, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨0 + 1, hj⟩ hij ≫ map F f ⟨0 + 1, hj⟩ ⟨0, hk⟩ hjk

Tactic:
simp [Nat.succ.injEq] at hjk

Result:
no goals

Proof state:
case mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows 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⟩ ≤ j
⊢ map F f ⟨i, hi⟩ k ⋯ = map F f ⟨i, hi⟩ j hij ≫ map F f j k hjk

Tactic:
obtain ⟨j, hj⟩ := j

Result:
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows 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⟩ ≤ k
hij : ⟨i, hi⟩ ≤ ⟨j, hj⟩
⊢ map F f ⟨i, hi⟩ k ⋯ = map F f ⟨i, hi⟩ ⟨j, hj⟩ hij ≫ map F f ⟨j, hj⟩ k hjk

Proof state:
case mk.mk.mk.succ.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
k : ℕ
hk : k < n + 1 + 1
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
hj : 0 < n + 1 + 1
hjk : ⟨0, hj⟩ ≤ ⟨k, hk⟩
hij : ⟨n✝ + 1, hi⟩ ≤ ⟨0, hj⟩
⊢ map F f ⟨n✝ + 1, hi⟩ ⟨k, hk⟩ ⋯ = map F f ⟨n✝ + 1, hi⟩ ⟨0, hj⟩ hij ≫ map F f ⟨0, hj⟩ ⟨k, hk⟩ hjk

Tactic:
simp [Fin.ext_iff] at hij

Result:
no goals

Proof state:
case mk.mk.mk.zero.succ.succ.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
hk : 0 < n + 1 + 1
hjk : ⟨j + 1 + 1, hj⟩ ≤ ⟨0, hk⟩
⊢ map F f ⟨0, hi⟩ ⟨0, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨j + 1 + 1, hj⟩ hij ≫ map F f ⟨j + 1 + 1, hj⟩ ⟨0, hk⟩ hjk

Tactic:
simp [Fin.ext_iff] at hjk

Result:
no goals

Proof state:
case mk.mk.mk.zero.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
k : ℕ
hk : k < n + 1 + 1
hi hj : 0 < n + 1 + 1
hjk : ⟨0, hj⟩ ≤ ⟨k, hk⟩
hij : ⟨0, hi⟩ ≤ ⟨0, hj⟩
⊢ map F f ⟨0, hi⟩ ⟨k, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨0, hj⟩ hij ≫ map F f ⟨0, hj⟩ ⟨k, hk⟩ hjk

Tactic:
dsimp

Result:
case mk.mk.mk.zero.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
k : ℕ
hk : k < n + 1 + 1
hi hj : 0 < n + 1 + 1
hjk : ⟨0, hj⟩ ≤ ⟨k, hk⟩
hij : ⟨0, hi⟩ ≤ ⟨0, hj⟩
⊢ map F f 0 ⟨k, hk⟩ ⋯ = 𝟙 X ≫ map F f 0 ⟨k, hk⟩ hjk

Proof state:
case mk.mk.mk.zero.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
k : ℕ
hk : k < n + 1 + 1
hi hj : 0 < n + 1 + 1
hjk : ⟨0, hj⟩ ≤ ⟨k, hk⟩
hij : ⟨0, hi⟩ ≤ ⟨0, hj⟩
⊢ map F f 0 ⟨k, hk⟩ ⋯ = 𝟙 X ≫ map F f 0 ⟨k, hk⟩ hjk

Tactic:
rw [id_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
i j k : Fin (n + 1 + 1)
hij : i ≤ j
hjk : j ≤ k
⊢ map F f i k ⋯ = map F f i j hij ≫ map F f j k hjk

Tactic:
obtain ⟨i, hi⟩ := i

Result:
case mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows 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⟩ ≤ j
⊢ map F f ⟨i, hi⟩ k ⋯ = map F f ⟨i, hi⟩ j hij ≫ map F f j k hjk

Proof state:
case mk.mk.mk.succ.succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
k : ℕ
hk : k < n + 1 + 1
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
j : ℕ
hj : j + 1 < n + 1 + 1
hjk : ⟨j + 1, hj⟩ ≤ ⟨k, hk⟩
hij : ⟨n✝ + 1, hi⟩ ≤ ⟨j + 1, hj⟩
⊢ map F f ⟨n✝ + 1, hi⟩ ⟨k, hk⟩ ⋯ = map F f ⟨n✝ + 1, hi⟩ ⟨j + 1, hj⟩ hij ≫ map F f ⟨j + 1, hj⟩ ⟨k, hk⟩ hjk

Tactic:
obtain _ | k := k

Result:
case mk.mk.mk.succ.succ.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
j : ℕ
hj : j + 1 < n + 1 + 1
hij : ⟨n✝ + 1, hi⟩ ≤ ⟨j + 1, hj⟩
hk : 0 < n + 1 + 1
hjk : ⟨j + 1, hj⟩ ≤ ⟨0, hk⟩
⊢ map F f ⟨n✝ + 1, hi⟩ ⟨0, hk⟩ ⋯ = map F f ⟨n✝ + 1, hi⟩ ⟨j + 1, hj⟩ hij ≫ map F f ⟨j + 1, hj⟩ ⟨0, hk⟩ hjk

case mk.mk.mk.succ.succ.succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
j : ℕ
hj : j + 1 < n + 1 + 1
hij : ⟨n✝ + 1, hi⟩ ≤ ⟨j + 1, hj⟩
k : ℕ
hk : k + 1 < n + 1 + 1
hjk : ⟨j + 1, hj⟩ ≤ ⟨k + 1, hk⟩
⊢ map F f ⟨n✝ + 1, hi⟩ ⟨k + 1, hk⟩ ⋯ = map F f ⟨n✝ + 1, hi⟩ ⟨j + 1, hj⟩ hij ≫ map F f ⟨j + 1, hj⟩ ⟨k + 1, hk⟩ hjk

Proof state:
case mk.mk.mk.zero.succ.succ.succ.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
hk : 0 + 1 < n + 1 + 1
hjk✝ : ⟨j + 1 + 1, hj⟩ ≤ ⟨0 + 1, hk⟩
hjk : j + 1 + 1 ≤ 1
⊢ map F f ⟨0, hi⟩ ⟨0 + 1, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨j + 1 + 1, hj⟩ hij ≫ map F f ⟨j + 1 + 1, hj⟩ ⟨0 + 1, hk⟩ hjk✝

Tactic:
omega

Result:
no goals

Proof state:
case mk.mk.mk.zero.succ.zero.succ.succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
hj : 0 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨0 + 1, hj⟩
k : ℕ
hk : k + 1 + 1 < n + 1 + 1
hjk : ⟨0 + 1, hj⟩ ≤ ⟨k + 1 + 1, hk⟩
⊢ map F f ⟨0, hi⟩ ⟨k + 1 + 1, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨0 + 1, hj⟩ hij ≫ map F f ⟨0 + 1, hj⟩ ⟨k + 1 + 1, hk⟩ hjk

Tactic:
rfl

Result:
no goals

Proof state:
case mk.mk.mk.zero.succ.succ.succ.succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
k : ℕ
hk : k + 1 + 1 < n + 1 + 1
hjk : ⟨j + 1 + 1, hj⟩ ≤ ⟨k + 1 + 1, hk⟩
⊢ map F f ⟨0, hi⟩ ⟨k + 1 + 1, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨j + 1 + 1, hj⟩ hij ≫ map F f ⟨j + 1 + 1, hj⟩ ⟨k + 1 + 1, hk⟩ hjk

Tactic:
dsimp

Result:
case mk.mk.mk.zero.succ.succ.succ.succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
k : ℕ
hk : k + 1 + 1 < n + 1 + 1
hjk : ⟨j + 1 + 1, hj⟩ ≤ ⟨k + 1 + 1, hk⟩
⊢ f ≫ F.map (homOfLE ⋯) = (f ≫ F.map (homOfLE ⋯)) ≫ F.map (homOfLE ⋯)

Proof state:
case mk.mk.mk.succ.succ.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
j : ℕ
hj : j + 1 < n + 1 + 1
hij : ⟨n✝ + 1, hi⟩ ≤ ⟨j + 1, hj⟩
hk : 0 < n + 1 + 1
hjk : ⟨j + 1, hj⟩ ≤ ⟨0, hk⟩
⊢ map F f ⟨n✝ + 1, hi⟩ ⟨0, hk⟩ ⋯ = map F f ⟨n✝ + 1, hi⟩ ⟨j + 1, hj⟩ hij ≫ map F f ⟨j + 1, hj⟩ ⟨0, hk⟩ hjk

Tactic:
simp [Fin.ext_iff] at hjk

Result:
no goals