awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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⟩
⊢ 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
have 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)) sorry =
    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: obtain _ | _ | k := k
Cleared hypotheses: k, hk, hjk
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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
⊢ 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
have 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)) sorry =
    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: obtain _ | _ | k := k
Cleared hypotheses: k, hk, hjk
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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
⊢ 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
have 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)) sorry =
    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: obtain _ | _ | k := k
Cleared hypotheses: k, hk, hjk
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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⟩
⊢ 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
have zero : f ≫ F.map (homOfLE sorry) = (f ≫ F.map (homOfLE sorry)) ≫ F.map (homOfLE sorry)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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⟩
⊢ f ≫ F.map (homOfLE ⋯) = (f ≫ F.map (homOfLE ⋯)) ≫ F.map (homOfLE ⋯)
have zero : f ≫ F.map (homOfLE sorry) = f ≫ F.map (homOfLE sorry) ≫ F.map (homOfLE sorry)
Tactic: rw [assoc, ← F.map_comp, homOfLE_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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 ⋯)
⊢ f ≫ F.map (homOfLE ⋯) = (f ≫ F.map (homOfLE ⋯)) ≫ F.map (homOfLE ⋯)
have zero₁ : f ≫ F.map (homOfLE sorry) = f ≫ F.map (homOfLE sorry ≫ homOfLE sorry)
Tactic: rw [assoc, ← F.map_comp, homOfLE_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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 ⋯)
⊢ f ≫ F.map (homOfLE ⋯) = (f ≫ F.map (homOfLE ⋯)) ≫ F.map (homOfLE ⋯)
have zero₂ : f ≫ F.map (homOfLE sorry) = f ≫ F.map (homOfLE sorry)
Tactic: rw [assoc, ← F.map_comp, homOfLE_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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⟩
⊢ 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
have 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)) sorry =
    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: obtain _ | j := j
Cleared hypotheses: j, hj, hjk, hij
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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
⊢ 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
have 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)) sorry =
    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 _ | j := j
Cleared hypotheses: j, hj, hjk, hij
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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⟩
⊢ 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
have 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)) sorry =
    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: obtain _ | k := k
Cleared hypotheses: k, hk, hjk
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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
⊢ 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
have 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)) sorry =
    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: obtain _ | k := k
Cleared hypotheses: k, hk, hjk
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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⟩
⊢ 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
have succ : Eq (α := F.obj (⟨n_1, sorry⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, sorry⟩)
  (F.map (homOfLE sorry) : F.obj (⟨n_1, sorry⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, sorry⟩)
  (F.map (homOfLE sorry) ≫ F.map (homOfLE sorry) : F.obj (⟨n_1, sorry⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, sorry⟩)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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⟩
⊢ 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, ⋯⟩)
have succ : Eq (α := F.obj (⟨n_1, sorry⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, sorry⟩)
  (F.map (homOfLE sorry) : F.obj (⟨n_1, sorry⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, sorry⟩)
  (F.map (homOfLE sorry ≫ homOfLE sorry) : F.obj (⟨n_1, sorry⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, sorry⟩)
Tactic: rw [← F.map_comp, homOfLE_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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, ⋯⟩)
⊢ 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, ⋯⟩)
have succ₁ : Eq (α := F.obj (⟨n_1, sorry⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, sorry⟩)
  (F.map (homOfLE sorry) : F.obj (⟨n_1, sorry⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, sorry⟩)
  (F.map (homOfLE sorry) : F.obj (⟨n_1, sorry⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, sorry⟩)
Tactic: rw [← F.map_comp, homOfLE_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 : ComposableArrows.{v_1, u_1} C n
F G : ComposableArrows.{v_1, u_1} C (n + 1)
α : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯
β : F.δ₀ ⟶ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
i : ℕ
hi : i < n + 1
⊢ F.map' i (i + 1) ⋯ hi ≫
      (fun (i : Fin (n + 1 + 1)) ↦
          (match (motive := (i : Fin (n + 1 + 1)) → F.obj i ⟶ G.obj i) i with
            | ⟨0, isLt⟩ => α
            | ⟨i.succ, hi⟩ => app' β i ⋯ :
            F.obj i ⟶ G.obj i))
        ⟨i + 1, ⋯⟩ =
    (fun (i : Fin (n + 1 + 1)) ↦
          (match (motive := (i : Fin (n + 1 + 1)) → F.obj i ⟶ G.obj i) i with
            | ⟨0, isLt⟩ => α
            | ⟨i.succ, hi⟩ => app' β i ⋯ :
            F.obj i ⟶ G.obj i))
        (⟨i, ⋯⟩ : Fin (n + 1 + 1)) ≫
      G.map' i (i + 1) ⋯ hi
have zero : ∀ (hi : 0 < n + 1),
  Eq (α := F.obj (⟨0, sorry⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, sorry⟩)
    (F.map' 0 (HAdd.hAdd (α := ℕ) 0 1) sorry hi ≫
        (fun (i : Fin (n + 1 + 1)) ↦
            (match (motive := (i : Fin (n + 1 + 1)) → F.obj i ⟶ G.obj i) i with
              | ⟨0, isLt⟩ => α
              | ⟨i.succ, hi⟩ => app' β i sorry :
              F.obj i ⟶ G.obj i))
          ⟨HAdd.hAdd (α := ℕ) 0 1, sorry⟩ :
      F.obj (⟨0, sorry⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, sorry⟩)
    (CategoryStruct.comp (Y := G.obj ⟨0, sorry⟩)
        ((fun (i : Fin (n + 1 + 1)) ↦
              (match (motive := (i : Fin (n + 1 + 1)) → F.obj i ⟶ G.obj i) i with
                | ⟨0, isLt⟩ => α
                | ⟨i.succ, hi⟩ => app' β i sorry :
                F.obj i ⟶ G.obj i))
            ⟨0, sorry⟩ :
          F.obj (⟨0, sorry⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨0, sorry⟩)
        (G.map' 0 (HAdd.hAdd (α := ℕ) 0 1) sorry hi :
          G.obj (⟨0, sorry⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, sorry⟩) :
      F.obj (⟨0, sorry⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, sorry⟩)
Tactic: obtain _ | i := i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows.{v_1, u_1} C (n + 1)
f g : F ⟶ G
h₀ : app' f 0 ⋯ = app' g 0 ⋯
h₁ : Eq (α := Functor.obj δ₀Functor F ⟶ Functor.obj δ₀Functor G) (Functor.map δ₀Functor f) (Functor.map δ₀Functor g)
⊢ f = g
have w : ∀ (i : ℕ) (hi : i < n + 1 + 1),
  Eq (α := F.obj (⟨i, hi⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i, hi⟩) (f.app ⟨i, hi⟩) (g.app ⟨i, hi⟩)
Tactic: ext ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows.{v_1, u_1} C (n + 1)
f g : F ⟶ G
h₀ : app' f 0 ⋯ = app' g 0 ⋯
h₁ : Eq (α := Functor.obj δ₀Functor F ⟶ Functor.obj δ₀Functor G) (Functor.map δ₀Functor f) (Functor.map δ₀Functor g)
i : ℕ
hi : i < n + 1 + 1
⊢ Eq (α := F.obj (⟨i, hi⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i, hi⟩) (f.app ⟨i, hi⟩) (g.app ⟨i, hi⟩)
have w : ∀ (hi : 0 < n + 1 + 1), Eq (α := F.obj (⟨0, hi⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨0, hi⟩) (f.app ⟨0, hi⟩) (g.app ⟨0, hi⟩)
Tactic: obtain _ | i := i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows.{v_1, u_1} C (n + 1)
f g : F ⟶ G
h₀ : app' f 0 ⋯ = app' g 0 ⋯
h₁ : Eq (α := Functor.obj δ₀Functor F ⟶ Functor.obj δ₀Functor G) (Functor.map δ₀Functor f) (Functor.map δ₀Functor g)
i : ℕ
hi : i < n + 1 + 1
w : ∀ (hi : 0 < n + 1 + 1), Eq (α := F.obj (⟨0, hi⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨0, hi⟩) (f.app ⟨0, hi⟩) (g.app ⟨0, hi⟩)
⊢ Eq (α := F.obj (⟨i, hi⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i, hi⟩) (f.app ⟨i, hi⟩) (g.app ⟨i, hi⟩)
have w₁ : ∀ (i : ℕ) (hi : i + 1 < n + 1 + 1),
  Eq (α := F.obj (⟨i + 1, hi⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i + 1, hi⟩) (f.app ⟨i + 1, hi⟩) (g.app ⟨i + 1, hi⟩)
Tactic: obtain _ | i := i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 : ComposableArrows.{v_1, u_1} C n
F G : ComposableArrows.{v_1, u_1} C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β.hom 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α.hom ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
⊢ Eq (α := G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj' 0 ⋯)
    (G.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β.inv 0 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj' 0 ⋯)
    (α.inv ≫ F.map' 0 1 homMk₁._proof_2 ⋯ : G.obj' 0 ⋯ ⟶ F.obj ⟨1, ⋯⟩)
have rw : Eq (α := F.obj' 0 sorry ⟶ F.δ₀.obj' 0 sorry)
  (CategoryStruct.comp (Y := F.obj ⟨1, sorry⟩)
      (F.map' 0 1 homMk₁._proof_2 sorry : F.obj (⟨0, sorry⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, sorry⟩)
      (𝟙 (F.δ₀.obj (⟨0, sorry⟩ : Fin (n + 1))) : F.δ₀.obj (⟨0, sorry⟩ : Fin (n + 1)) ⟶ F.δ₀.obj (⟨0, sorry⟩ : Fin (n + 1))) :
    F.obj (⟨0, sorry⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj' 0 sorry)
  (F.map' 0 1 homMk₁._proof_2 sorry : F.obj (⟨0, sorry⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, sorry⟩)
Tactic: rw [← cancel_epi α.hom, ← reassoc_of% w, α.hom_inv_id_assoc, β.hom_inv_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 : ComposableArrows.{v_1, u_1} C n
F G : ComposableArrows.{v_1, u_1} C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β.hom 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α.hom ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
⊢ Eq (α := F.obj' 0 ⋯ ⟶ F.δ₀.obj' 0 ⋯)
    (CategoryStruct.comp (Y := F.obj ⟨1, ⋯⟩)
        (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
        (𝟙 (F.δ₀.obj (⟨0, ⋯⟩ : Fin (n + 1))) : F.δ₀.obj (⟨0, ⋯⟩ : Fin (n + 1)) ⟶ F.δ₀.obj (⟨0, ⋯⟩ : Fin (n + 1))) :
      F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
have dsimp : Eq (α := F.obj 0 ⟶ F.obj 1)
  (CategoryStruct.comp (Y := F.obj 1) (F.map (homOfLE sorry) : F.obj 0 ⟶ F.obj 1) (𝟙 (F.obj 1) : F.obj 1 ⟶ F.obj 1) :
    F.obj 0 ⟶ F.obj 1)
  (F.map (homOfLE sorry) : F.obj 0 ⟶ F.obj 1)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 : ComposableArrows.{v_1, u_1} C n
F G : ComposableArrows.{v_1, u_1} C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β.hom 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α.hom ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
⊢ Eq (α := F.obj 0 ⟶ F.obj 1)
    (CategoryStruct.comp (Y := F.obj 1) (F.map (homOfLE ⋯) : F.obj 0 ⟶ F.obj 1) (𝟙 (F.obj 1) : F.obj 1 ⟶ F.obj 1) :
      F.obj 0 ⟶ F.obj 1)
    (F.map (homOfLE ⋯) : F.obj 0 ⟶ F.obj 1)
have rw : Eq (α := F.obj 0 ⟶ F.obj 1) (F.map (homOfLE sorry) : F.obj 0 ⟶ F.obj 1) (F.map (homOfLE sorry) : F.obj 0 ⟶ F.obj 1)
Tactic: rw [comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 : ComposableArrows.{v_1, u_1} C n
F G : ComposableArrows.{v_1, u_1} C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β.hom 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α.hom ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
⊢ homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv ⋯ = 𝟙 F
have h₀ : app' (homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv sorry) 0 sorry = app' (𝟙 F) 0 sorry
Tactic: apply hom_ext_succ
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 : ComposableArrows.{v_1, u_1} C n
F G : ComposableArrows.{v_1, u_1} C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β.hom 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α.hom ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
h₀ : app' (homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv ⋯) 0 ⋯ = app' (𝟙 F) 0 ⋯
⊢ homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv ⋯ = 𝟙 F
have h₁ : Eq (α := Functor.obj δ₀Functor F ⟶ Functor.obj δ₀Functor F)
  (Functor.map δ₀Functor (homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv sorry)) (Functor.map δ₀Functor (𝟙 F))
Tactic: apply hom_ext_succ
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 : ComposableArrows.{v_1, u_1} C n
F G : ComposableArrows.{v_1, u_1} C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β.hom 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α.hom ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
⊢ Eq (α := Functor.obj δ₀Functor F ⟶ Functor.obj δ₀Functor F)
    (Functor.map δ₀Functor (homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv ⋯)) (Functor.map δ₀Functor (𝟙 F))
have h₁ : ∀ (i : ℕ) (hi : i < n + 1),
  Eq (α := (Functor.obj δ₀Functor F).obj (⟨i, hi⟩ : Fin (n + 1)) ⟶ (Functor.obj δ₀Functor F).obj ⟨i, hi⟩)
    (NatTrans.app (Functor.map δ₀Functor (homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv sorry)) ⟨i, hi⟩)
    (NatTrans.app (Functor.map δ₀Functor (𝟙 F)) ⟨i, hi⟩)
Tactic: ext ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 : ComposableArrows.{v_1, u_1} C n
F G : ComposableArrows.{v_1, u_1} C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β.hom 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α.hom ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
⊢ homMkSucc α.inv β.inv ⋯ ≫ homMkSucc α.hom β.hom w = 𝟙 G
have h₀ : app' (homMkSucc α.inv β.inv sorry ≫ homMkSucc α.hom β.hom w) 0 sorry = app' (𝟙 G) 0 sorry
Tactic: apply hom_ext_succ