-- Mathlib/CategoryTheory/Functor/OfSequence.lean
@[reassoc]
lemma map_comp (i j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k) :
    map f i k (hij.trans hjk) = map f i j hij ≫ map f j k hjk

Proof state:
case succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
i : ℕ
hi :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k),
    map f i k ⋯ = map f i j hij ≫ map f j k hjk
⊢ ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : i + 1 ≤ j) (hjk : j ≤ k),
    map f (i + 1) k ⋯ = map f (i + 1) j hij ≫ map f j k hjk

Tactic:
rintro X f (_|j) (_|k)

Result:
case succ.zero.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
i : ℕ
hi :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k),
    map f i k ⋯ = map f i j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
⊢ ∀ (hij : i + 1 ≤ 0) (hjk : 0 ≤ 0), map f (i + 1) 0 ⋯ = map f (i + 1) 0 hij ≫ map f 0 0 hjk

case succ.zero.succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
i : ℕ
hi :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k),
    map f i k ⋯ = map f i j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
k : ℕ
⊢ ∀ (hij : i + 1 ≤ 0) (hjk : 0 ≤ k + 1), map f (i + 1) (k + 1) ⋯ = map f (i + 1) 0 hij ≫ map f 0 (k + 1) hjk

case succ.succ.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
i : ℕ
hi :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k),
    map f i k ⋯ = map f i j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
j : ℕ
⊢ ∀ (hij : i + 1 ≤ j + 1) (hjk : j + 1 ≤ 0), map f (i + 1) 0 ⋯ = map f (i + 1) (j + 1) hij ≫ map f (j + 1) 0 hjk

case succ.succ.succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
i : ℕ
hi :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k),
    map f i k ⋯ = map f i j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
j k : ℕ
⊢ ∀ (hij : i + 1 ≤ j + 1) (hjk : j + 1 ≤ k + 1),
    map f (i + 1) (k + 1) ⋯ = map f (i + 1) (j + 1) hij ≫ map f (j + 1) (k + 1) hjk

Proof state:
case zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
⊢ ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk

Tactic:
intros X f j

Result:
case zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
j : ℕ
⊢ ∀ (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k), map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk

Proof state:
case zero.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
k : ℕ
hij : 0 ≤ 0
hjk : 0 ≤ k
⊢ map f 0 k ⋯ = map f 0 0 hij ≫ map f 0 k hjk

Tactic:
rw [map_id, id_comp]

Result:
no goals

Proof state:
case zero.succ.succ.succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
k : ℕ
hij : 0 ≤ j + 1
hjk : j + 1 ≤ k + 1 + 1
⊢ map f 0 (k + 1 + 1) ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) (k + 1 + 1) hjk

Tactic:
simp only [map, Nat.reduceAdd]

Result:
case zero.succ.succ.succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
k : ℕ
hij : 0 ≤ j + 1
hjk : j + 1 ≤ k + 1 + 1
⊢ f 0 ≫ map (fun n => f (n + 1)) 0 (k + 1) ⋯ = map f 0 (j + 1) hij ≫ map (fun n => f (n + 1)) j (k + 1) ⋯

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hij : 0 ≤ j + 1
hjk : j + 1 ≤ 0 + 1
⊢ j = 0

Tactic:
omega

Result:
no goals

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

Tactic:
revert X f j k

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
i : ℕ
⊢ ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k),
    map f i k ⋯ = map f i j hij ≫ map f j k hjk

Proof state:
case zero.succ.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hij : 0 ≤ j + 1
hjk : j + 1 ≤ 0
⊢ map f 0 0 ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) 0 hjk

Tactic:
omega

Result:
no goals

Proof state:
case zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
j : ℕ
⊢ ∀ (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k), map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk

Tactic:
revert X f

Result:
case zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
j : ℕ
⊢ ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk

Proof state:
case zero.succ.succ.succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
k : ℕ
hij : 0 ≤ j + 1
hjk : j + 1 ≤ k + 1 + 1
⊢ f 0 ≫ map (fun n => f (n + 1)) 0 j ⋯ ≫ map (fun n => f (n + 1)) j (k + 1) ⋯ =
    map f 0 (j + 1) hij ≫ map (fun n => f (n + 1)) j (k + 1) ⋯

Tactic:
obtain _|j := j

Result:
case zero.succ.succ.succ.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
k : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ 0) (hjk : 0 ≤ k),
    map f 0 k ⋯ = map f 0 0 hij ≫ map f 0 k hjk
hij : 0 ≤ 0 + 1
hjk : 0 + 1 ≤ k + 1 + 1
⊢ f 0 ≫ map (fun n => f (n + 1)) 0 0 ⋯ ≫ map (fun n => f (n + 1)) 0 (k + 1) ⋯ =
    map f 0 (0 + 1) hij ≫ map (fun n => f (n + 1)) 0 (k + 1) ⋯

case zero.succ.succ.succ.succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
k j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j + 1) (hjk : j + 1 ≤ k),
    map f 0 k ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) k hjk
hij : 0 ≤ j + 1 + 1
hjk : j + 1 + 1 ≤ k + 1 + 1
⊢ f 0 ≫ map (fun n => f (n + 1)) 0 (j + 1) ⋯ ≫ map (fun n => f (n + 1)) (j + 1) (k + 1) ⋯ =
    map f 0 (j + 1 + 1) hij ≫ map (fun n => f (n + 1)) (j + 1) (k + 1) ⋯

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
k : ℕ
hij : 0 ≤ j + 1
hjk : j + 1 ≤ k + 1 + 1
⊢ j ≤ k + 1

Tactic:
omega

Result:
no goals

Proof state:
case succ.zero.succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
i : ℕ
hi :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k),
    map f i k ⋯ = map f i j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
k : ℕ
⊢ ∀ (hij : i + 1 ≤ 0) (hjk : 0 ≤ k + 1), map f (i + 1) (k + 1) ⋯ = map f (i + 1) 0 hij ≫ map f 0 (k + 1) hjk

Tactic:
omega

Result:
no goals

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

Tactic:
omega

Result:
no goals

Proof state:
case succ.zero.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
i : ℕ
hi :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k),
    map f i k ⋯ = map f i j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
⊢ ∀ (hij : i + 1 ≤ 0) (hjk : 0 ≤ 0), map f (i + 1) 0 ⋯ = map f (i + 1) 0 hij ≫ map f 0 0 hjk

Tactic:
omega

Result:
no goals