-- 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.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⟩
⊢ F.map (homOfLE ⋯) = F.map (homOfLE ⋯) ≫ F.map (homOfLE ⋯)

Tactic:
rw [← F.map_comp, homOfLE_comp]

Result:
no goals

Proof state:
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

Tactic:
dsimp

Result:
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⟩
⊢ F.map (homOfLE ⋯) = F.map (homOfLE ⋯) ≫ F.map (homOfLE ⋯)

Proof state:
case mk.mk.mk.zero.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
hi : 0 < n + 1 + 1
hj : 0 + 1 < n + 1 + 1
hjk : ⟨0 + 1, hj⟩ ≤ ⟨k, hk⟩
hij : ⟨0, hi⟩ ≤ ⟨0 + 1, hj⟩
⊢ map F f ⟨0, hi⟩ ⟨k, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨0 + 1, hj⟩ hij ≫ map F f ⟨0 + 1, hj⟩ ⟨k, hk⟩ hjk

Tactic:
obtain _ | _ | k := k

Result:
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

case mk.mk.mk.zero.succ.zero.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
hj : 0 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨0 + 1, hj⟩
hk : 0 + 1 < n + 1 + 1
hjk : ⟨0 + 1, hj⟩ ≤ ⟨0 + 1, hk⟩
⊢ map F f ⟨0, hi⟩ ⟨0 + 1, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨0 + 1, hj⟩ hij ≫ map F f ⟨0 + 1, hj⟩ ⟨0 + 1, hk⟩ hjk

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

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⟩
⊢ f ≫ F.map (homOfLE ⋯) = (f ≫ F.map (homOfLE ⋯)) ≫ F.map (homOfLE ⋯)

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

Result:
no goals

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

Tactic:
obtain _ | j := j

Result:
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

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

Proof state:
case mk.mk.mk.zero.succ.zero.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
hj : 0 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨0 + 1, hj⟩
hk : 0 + 1 < n + 1 + 1
hjk : ⟨0 + 1, hj⟩ ≤ ⟨0 + 1, hk⟩
⊢ map F f ⟨0, hi⟩ ⟨0 + 1, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨0 + 1, hj⟩ hij ≫ map F f ⟨0 + 1, hj⟩ ⟨0 + 1, hk⟩ hjk

Tactic:
simp

Result:
no goals

Proof state:
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

Tactic:
obtain ⟨k, hk⟩ := k

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

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

Tactic:
obtain _ | _ | j := j

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, hi⟩ ⟨k, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨0, hj⟩ hij ≫ map F f ⟨0, hj⟩ ⟨k, hk⟩ hjk

case mk.mk.mk.zero.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
hi : 0 < n + 1 + 1
hj : 0 + 1 < n + 1 + 1
hjk : ⟨0 + 1, hj⟩ ≤ ⟨k, hk⟩
hij : ⟨0, hi⟩ ≤ ⟨0 + 1, hj⟩
⊢ map F f ⟨0, hi⟩ ⟨k, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨0 + 1, hj⟩ hij ≫ map F f ⟨0 + 1, hj⟩ ⟨k, hk⟩ hjk

case mk.mk.mk.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
k : ℕ
hk : k < n + 1 + 1
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hjk : ⟨j + 1 + 1, hj⟩ ≤ ⟨k, hk⟩
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
⊢ map F f ⟨0, hi⟩ ⟨k, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨j + 1 + 1, hj⟩ hij ≫ map F f ⟨j + 1 + 1, hj⟩ ⟨k, hk⟩ hjk

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

Tactic:
cases i

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

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