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 m : ℕ
F_1 G_1 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hj : i + 0 = i
hj' : i ≤ n
⊢ Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, ⋯⟩)
    (F.map' i i ⋯ hj' ≫ app ⟨i, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i i ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, ⋯⟩)
have zero : 𝟙 (F.obj (⟨i, sorry⟩ : Fin (n + 1))) ≫ app (⟨i, sorry⟩ : Fin (n + 1)) = app (⟨i, sorry⟩ : Fin (n + 1)) ≫ G.map' i i sorry hj'
Tactic: rw [F.map'_self i, G.map'_self i, id_comp, 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 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hj : i + 0 = i
hj' : i ≤ n
zero : 𝟙 (F.obj (⟨i, ⋯⟩ : Fin (n + 1))) ≫ app (⟨i, ⋯⟩ : Fin (n + 1)) = app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i i ⋯ hj'
⊢ Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, ⋯⟩)
    (F.map' i i ⋯ hj' ≫ app ⟨i, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i i ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, ⋯⟩)
have zero₁ : 𝟙 (F.obj (⟨i, sorry⟩ : Fin (n + 1))) ≫ app (⟨i, sorry⟩ : Fin (n + 1)) = app (⟨i, sorry⟩ : Fin (n + 1)) ≫ 𝟙 (G.obj ⟨i, sorry⟩)
Tactic: rw [F.map'_self i, G.map'_self i, id_comp, 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 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hj : i + 0 = i
hj' : i ≤ n
zero : 𝟙 (F.obj (⟨i, ⋯⟩ : Fin (n + 1))) ≫ app (⟨i, ⋯⟩ : Fin (n + 1)) = app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i i ⋯ hj'
zero₁ : 𝟙 (F.obj (⟨i, ⋯⟩ : Fin (n + 1))) ≫ app (⟨i, ⋯⟩ : Fin (n + 1)) = app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ 𝟙 (G.obj ⟨i, ⋯⟩)
⊢ Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, ⋯⟩)
    (F.map' i i ⋯ hj' ≫ app ⟨i, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i i ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, ⋯⟩)
have zero₂ : app ⟨i, sorry⟩ = app (⟨i, sorry⟩ : Fin (n + 1)) ≫ 𝟙 (G.obj (⟨i, sorry⟩ : Fin (n + 1)))
Tactic: rw [F.map'_self i, G.map'_self i, id_comp, 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 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hj : i + 0 = i
hj' : i ≤ n
zero : 𝟙 (F.obj (⟨i, ⋯⟩ : Fin (n + 1))) ≫ app (⟨i, ⋯⟩ : Fin (n + 1)) = app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i i ⋯ hj'
zero₁ : 𝟙 (F.obj (⟨i, ⋯⟩ : Fin (n + 1))) ≫ app (⟨i, ⋯⟩ : Fin (n + 1)) = app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ 𝟙 (G.obj ⟨i, ⋯⟩)
zero₂ : app ⟨i, ⋯⟩ = app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ 𝟙 (G.obj (⟨i, ⋯⟩ : Fin (n + 1)))
⊢ Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, ⋯⟩)
    (F.map' i i ⋯ hj' ≫ app ⟨i, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i i ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, ⋯⟩)
have zero₃ : Eq.{v_1 + 1} (α := F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, sorry⟩) (app ⟨i, sorry⟩) (app ⟨i, sorry⟩)
Tactic: rw [F.map'_self i, G.map'_self i, id_comp, 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 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
hk :
  ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
i j : ℕ
hj : i + (k + 1) = j
hj' : j ≤ n
⊢ Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
    (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
have succ : ∀ (hj_1 : i + k + 1 = j) (hj' : j ≤ n),
  Eq (α := F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, sorry⟩)
    (F.map' i j sorry hj' ≫ app ⟨j, sorry⟩ : F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, sorry⟩)
    (app (⟨i, sorry⟩ : Fin (n + 1)) ≫ G.map' i j sorry hj' : F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, sorry⟩)
Tactic: rw [← add_assoc] at hj
Cleared hypotheses: hj'
-- 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 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
hk :
  ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
i j : ℕ
hj_1 : i + (k + 1) = j
hj : i + k + 1 = j
hj' : j ≤ n
⊢ Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
    (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
have succ : ∀ (hj : i + (k + 1) = i + k + 1) (hj' : i + k + 1 ≤ n),
  Eq (α := F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, sorry⟩)
    (F.map' i (i + k + 1) sorry hj' ≫ app ⟨i + k + 1, sorry⟩ : F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, sorry⟩)
    (app (⟨i, sorry⟩ : Fin (n + 1)) ≫ G.map' i (i + k + 1) sorry hj' : F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, sorry⟩)
Tactic: subst hj
Cleared hypotheses: j, hj_1, hj, hj'
-- 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 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
hk :
  ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
i : ℕ
hj : i + (k + 1) = i + k + 1
hj' : i + k + 1 ≤ n
⊢ Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (F.map' i (i + k + 1) ⋯ hj' ≫ app ⟨i + k + 1, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i (i + k + 1) ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
have succ : Eq (α := F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, sorry⟩)
  (CategoryStruct.comp (Y := F.obj ⟨i + k, sorry⟩) (F.map' i (i + k) sorry sorry : F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ F.obj ⟨i + k, sorry⟩)
        (F.map' (i + k) (i + k + 1) sorry hj' : F.obj (⟨i + k, sorry⟩ : Fin (n + 1)) ⟶ F.obj ⟨i + k + 1, sorry⟩) ≫
      app ⟨i + k + 1, sorry⟩ :
    F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, sorry⟩)
  (app (⟨i, sorry⟩ : Fin (n + 1)) ≫ G.map' i (i + k + 1) sorry hj' : F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, sorry⟩)
Tactic: rw [F.map'_comp i (i + k) (i + k + 1), G.map'_comp i (i + k) (i + k + 1), assoc,
        w (i + k) (by valid), reassoc_of% (hk i (i + k) rfl (by valid))]
-- 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 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
hk :
  ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
i : ℕ
hj : i + (k + 1) = i + k + 1
hj' : i + k + 1 ≤ n
succ :
  Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (CategoryStruct.comp (Y := F.obj ⟨i + k, ⋯⟩)
          (F.map' i (i + k) ⋯ ⋯ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨i + k, ⋯⟩)
          (F.map' (i + k) (i + k + 1) ⋯ hj' : F.obj (⟨i + k, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨i + k + 1, ⋯⟩) ≫
        app ⟨i + k + 1, ⋯⟩ :
      F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i (i + k + 1) ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
⊢ Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (F.map' i (i + k + 1) ⋯ hj' ≫ app ⟨i + k + 1, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i (i + k + 1) ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
have succ₁ : Eq (α := F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, sorry⟩)
  (CategoryStruct.comp (Y := F.obj ⟨i + k, sorry⟩) (F.map' i (i + k) sorry sorry : F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ F.obj ⟨i + k, sorry⟩)
        (F.map' (i + k) (i + k + 1) sorry hj' : F.obj (⟨i + k, sorry⟩ : Fin (n + 1)) ⟶ F.obj ⟨i + k + 1, sorry⟩) ≫
      app ⟨i + k + 1, sorry⟩ :
    F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, sorry⟩)
  (app (⟨i, sorry⟩ : Fin (n + 1)) ≫
      CategoryStruct.comp (Y := G.obj ⟨i + k, sorry⟩)
        (G.map' i (i + k) sorry sorry : G.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k, sorry⟩)
        (G.map' (i + k) (i + k + 1) sorry hj' : G.obj (⟨i + k, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, sorry⟩) :
    F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, sorry⟩)
Tactic: rw [F.map'_comp i (i + k) (i + k + 1), G.map'_comp i (i + k) (i + k + 1), assoc,
        w (i + k) (by valid), reassoc_of% (hk i (i + k) rfl (by valid))]
-- 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 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
hk :
  ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
i : ℕ
hj : i + (k + 1) = i + k + 1
hj' : i + k + 1 ≤ n
succ :
  Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (CategoryStruct.comp (Y := F.obj ⟨i + k, ⋯⟩)
          (F.map' i (i + k) ⋯ ⋯ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨i + k, ⋯⟩)
          (F.map' (i + k) (i + k + 1) ⋯ hj' : F.obj (⟨i + k, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨i + k + 1, ⋯⟩) ≫
        app ⟨i + k + 1, ⋯⟩ :
      F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i (i + k + 1) ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
succ₁ :
  Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (CategoryStruct.comp (Y := F.obj ⟨i + k, ⋯⟩)
          (F.map' i (i + k) ⋯ ⋯ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨i + k, ⋯⟩)
          (F.map' (i + k) (i + k + 1) ⋯ hj' : F.obj (⟨i + k, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨i + k + 1, ⋯⟩) ≫
        app ⟨i + k + 1, ⋯⟩ :
      F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫
        CategoryStruct.comp (Y := G.obj ⟨i + k, ⋯⟩)
          (G.map' i (i + k) ⋯ ⋯ : G.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k, ⋯⟩)
          (G.map' (i + k) (i + k + 1) ⋯ hj' : G.obj (⟨i + k, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩) :
      F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
⊢ Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (F.map' i (i + k + 1) ⋯ hj' ≫ app ⟨i + k + 1, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i (i + k + 1) ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
have succ₂ : Eq (α := F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, sorry⟩)
  (CategoryStruct.comp (Y := F.obj ⟨i + k, sorry⟩) (F.map' i (i + k) sorry sorry : F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ F.obj ⟨i + k, sorry⟩)
      (F.map' (i + k) (i + k + 1) sorry hj' ≫ app ⟨i + k + 1, sorry⟩ :
        F.obj (⟨i + k, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, sorry⟩) :
    F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, sorry⟩)
  (app (⟨i, sorry⟩ : Fin (n + 1)) ≫
      CategoryStruct.comp (Y := G.obj ⟨i + k, sorry⟩)
        (G.map' i (i + k) sorry sorry : G.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k, sorry⟩)
        (G.map' (i + k) (i + k + 1) sorry hj' : G.obj (⟨i + k, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, sorry⟩) :
    F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, sorry⟩)
Tactic: rw [F.map'_comp i (i + k) (i + k + 1), G.map'_comp i (i + k) (i + k + 1), assoc,
        w (i + k) (by valid), reassoc_of% (hk i (i + k) rfl (by valid))]
-- 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 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
⊢ ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
have zero : ∀ (i j : ℕ) (hj : i + 0 = j) (hj' : j ≤ n),
  Eq (α := F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, sorry⟩)
    (F.map' i j sorry hj' ≫ app ⟨j, sorry⟩ : F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, sorry⟩)
    (app (⟨i, sorry⟩ : Fin (n + 1)) ≫ G.map' i j sorry hj' : F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, sorry⟩)
Tactic: induction k with intro i j hj hj'
    | zero =>
      simp only [add_zero] at hj
      obtain rfl := hj
      rw [F.map'_self i, G.map'_self i, id_comp, comp_id]
    | succ k hk =>
      rw [← add_assoc] at hj
      subst hj
      rw [F.map'_comp i (i + k) (i + k + 1), G.map'_comp i (i + k) (i + k + 1), assoc,
        w (i + k) (by valid), reassoc_of% (hk i (i + k) rfl (by valid))]
Cleared hypotheses: k
-- 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 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
zero zero₁ :
  ∀ (i j : ℕ) (hj : i + 0 = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
⊢ ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
have succ : ∀ (k : ℕ)
  (hk :
    ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
      Eq (α := F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, sorry⟩)
        (F.map' i j sorry hj' ≫ app ⟨j, sorry⟩ : F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, sorry⟩)
        (app (⟨i, sorry⟩ : Fin (n + 1)) ≫ G.map' i j sorry hj' : F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, sorry⟩))
  (i j : ℕ) (hj : i + (k + 1) = j) (hj' : j ≤ n),
  Eq (α := F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, sorry⟩)
    (F.map' i j sorry hj' ≫ app ⟨j, sorry⟩ : F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, sorry⟩)
    (app (⟨i, sorry⟩ : Fin (n + 1)) ≫ G.map' i j sorry hj' : F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, sorry⟩)
Tactic: induction k with intro i j hj hj'
    | zero =>
      simp only [add_zero] at hj
      obtain rfl := hj
      rw [F.map'_self i, G.map'_self i, id_comp, comp_id]
    | succ k hk =>
      rw [← add_assoc] at hj
      subst hj
      rw [F.map'_comp i (i + k) (i + k + 1), G.map'_comp i (i + k) (i + k + 1), assoc,
        w (i + k) (by valid), reassoc_of% (hk i (i + k) rfl (by valid))]
Cleared hypotheses: k
-- 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 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ≅ G.obj i
w :
  ∀ (i : ℕ) (hi : i < n),
    F.map' i (i + 1) ⋯ hi ≫ Iso.hom (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) = Iso.hom (app ⟨i, ⋯⟩) ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hi : i < n
⊢ G.map' i (i + 1) ⋯ hi ≫ Iso.inv (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) = Iso.inv (app ⟨i, ⋯⟩) ≫ F.map' i (i + 1) ⋯ hi
have rw : Iso.hom (app (⟨i, sorry⟩ : Fin (n + 1))) ≫ G.map' i (i + 1) sorry hi ≫ Iso.inv (app (⟨i + 1, sorry⟩ : Fin (n + 1))) =
  Iso.hom (app ⟨i, sorry⟩) ≫ Iso.inv (app (⟨i, sorry⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) sorry hi
Tactic: rw [← cancel_epi ((app _).hom), ← reassoc_of% (w i hi), Iso.hom_inv_id, comp_id,
      Iso.hom_inv_id_assoc]
-- 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 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ≅ G.obj i
w :
  ∀ (i : ℕ) (hi : i < n),
    F.map' i (i + 1) ⋯ hi ≫ Iso.hom (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) = Iso.hom (app ⟨i, ⋯⟩) ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hi : i < n
rw :
  Iso.hom (app (⟨i, ⋯⟩ : Fin (n + 1))) ≫ G.map' i (i + 1) ⋯ hi ≫ Iso.inv (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) =
    Iso.hom (app ⟨i, ⋯⟩) ≫ Iso.inv (app (⟨i, ⋯⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) ⋯ hi
⊢ G.map' i (i + 1) ⋯ hi ≫ Iso.inv (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) = Iso.inv (app ⟨i, ⋯⟩) ≫ F.map' i (i + 1) ⋯ hi
have rw₁ : F.map' i (i + 1) sorry hi ≫ Iso.hom (app (⟨i + 1, sorry⟩ : Fin (n + 1))) ≫ Iso.inv (app (⟨i + 1, sorry⟩ : Fin (n + 1))) =
  Iso.hom (app ⟨i, sorry⟩) ≫ Iso.inv (app (⟨i, sorry⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) sorry hi
Tactic: rw [← cancel_epi ((app _).hom), ← reassoc_of% (w i hi), Iso.hom_inv_id, comp_id,
      Iso.hom_inv_id_assoc]
-- 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 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ≅ G.obj i
w :
  ∀ (i : ℕ) (hi : i < n),
    F.map' i (i + 1) ⋯ hi ≫ Iso.hom (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) = Iso.hom (app ⟨i, ⋯⟩) ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hi : i < n
rw :
  Iso.hom (app (⟨i, ⋯⟩ : Fin (n + 1))) ≫ G.map' i (i + 1) ⋯ hi ≫ Iso.inv (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) =
    Iso.hom (app ⟨i, ⋯⟩) ≫ Iso.inv (app (⟨i, ⋯⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) ⋯ hi
rw₁ :
  F.map' i (i + 1) ⋯ hi ≫ Iso.hom (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) ≫ Iso.inv (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) =
    Iso.hom (app ⟨i, ⋯⟩) ≫ Iso.inv (app (⟨i, ⋯⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) ⋯ hi
⊢ G.map' i (i + 1) ⋯ hi ≫ Iso.inv (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) = Iso.inv (app ⟨i, ⋯⟩) ≫ F.map' i (i + 1) ⋯ hi
have rw₂ : F.map' i (i + 1) sorry hi ≫ 𝟙 (F.obj (⟨i + 1, sorry⟩ : Fin (n + 1))) =
  Iso.hom (app ⟨i, sorry⟩) ≫ Iso.inv (app (⟨i, sorry⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) sorry hi
Tactic: rw [← cancel_epi ((app _).hom), ← reassoc_of% (w i hi), Iso.hom_inv_id, comp_id,
      Iso.hom_inv_id_assoc]
-- 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 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ≅ G.obj i
w :
  ∀ (i : ℕ) (hi : i < n),
    F.map' i (i + 1) ⋯ hi ≫ Iso.hom (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) = Iso.hom (app ⟨i, ⋯⟩) ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hi : i < n
rw :
  Iso.hom (app (⟨i, ⋯⟩ : Fin (n + 1))) ≫ G.map' i (i + 1) ⋯ hi ≫ Iso.inv (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) =
    Iso.hom (app ⟨i, ⋯⟩) ≫ Iso.inv (app (⟨i, ⋯⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) ⋯ hi
rw₁ :
  F.map' i (i + 1) ⋯ hi ≫ Iso.hom (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) ≫ Iso.inv (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) =
    Iso.hom (app ⟨i, ⋯⟩) ≫ Iso.inv (app (⟨i, ⋯⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) ⋯ hi
rw₂ :
  F.map' i (i + 1) ⋯ hi ≫ 𝟙 (F.obj (⟨i + 1, ⋯⟩ : Fin (n + 1))) =
    Iso.hom (app ⟨i, ⋯⟩) ≫ Iso.inv (app (⟨i, ⋯⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) ⋯ hi
⊢ G.map' i (i + 1) ⋯ hi ≫ Iso.inv (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) = Iso.inv (app ⟨i, ⋯⟩) ≫ F.map' i (i + 1) ⋯ hi
have rw₃ : F.map' i (i + 1) sorry hi = Iso.hom (app ⟨i, sorry⟩) ≫ Iso.inv (app (⟨i, sorry⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) sorry hi
Tactic: rw [← cancel_epi ((app _).hom), ← reassoc_of% (w i hi), Iso.hom_inv_id, comp_id,
      Iso.hom_inv_id_assoc]
-- 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 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ≅ G.obj i
w :
  ∀ (i : ℕ) (hi : i < n),
    F.map' i (i + 1) ⋯ hi ≫ Iso.hom (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) = Iso.hom (app ⟨i, ⋯⟩) ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hi : i < n
rw :
  Iso.hom (app (⟨i, ⋯⟩ : Fin (n + 1))) ≫ G.map' i (i + 1) ⋯ hi ≫ Iso.inv (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) =
    Iso.hom (app ⟨i, ⋯⟩) ≫ Iso.inv (app (⟨i, ⋯⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) ⋯ hi
rw₁ :
  F.map' i (i + 1) ⋯ hi ≫ Iso.hom (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) ≫ Iso.inv (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) =
    Iso.hom (app ⟨i, ⋯⟩) ≫ Iso.inv (app (⟨i, ⋯⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) ⋯ hi
rw₂ :
  F.map' i (i + 1) ⋯ hi ≫ 𝟙 (F.obj (⟨i + 1, ⋯⟩ : Fin (n + 1))) =
    Iso.hom (app ⟨i, ⋯⟩) ≫ Iso.inv (app (⟨i, ⋯⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) ⋯ hi
rw₃ : F.map' i (i + 1) ⋯ hi = Iso.hom (app ⟨i, ⋯⟩) ≫ Iso.inv (app (⟨i, ⋯⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) ⋯ hi
⊢ G.map' i (i + 1) ⋯ hi ≫ Iso.inv (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) = Iso.inv (app ⟨i, ⋯⟩) ≫ F.map' i (i + 1) ⋯ hi
have rw₄ : F.map' i (i + 1) sorry hi = F.map' i (i + 1) sorry hi
Tactic: rw [← cancel_epi ((app _).hom), ← reassoc_of% (w i hi), Iso.hom_inv_id, comp_id,
      Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 0
φ φ' : F ⟶ G
h : app' φ 0 homMk₀._proof_1 = app' φ' 0 homMk₀._proof_1
⊢ φ = φ'
have w : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), φ.app i = φ'.app i
Tactic: ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 0
φ φ' : F ⟶ G
h : app' φ 0 homMk₀._proof_1 = app' φ' 0 homMk₀._proof_1
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
⊢ φ.app i = φ'.app i
have w : Eq (α :=
  F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ i) (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1))) ⟶
    G.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ i) ⟨0, sorry⟩))
  (φ.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ i) ⟨0, sorry⟩))
  (φ'.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ i) ⟨0, sorry⟩))
Tactic: fin_cases i
Cleared hypotheses: i