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
F G : ComposableArrows.{v_1, u_1} C 0
f : F ⟶ G
⊢ IsIso f ↔ IsIso (X := F.obj 0) (f.app 0)
have rw : (∀ (X : Fin (HAdd.hAdd (α := ℕ) 0 1)), IsIso (f.app X)) ↔ IsIso (X := F.obj 0) (f.app 0)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- 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 : F ⟶ G
h : IsIso (X := F.obj 0) (f.app 0)
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
⊢ IsIso (f.app i)
have 0 : IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ i) ⟨0, sorry⟩))
  (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ i) ⟨0, sorry⟩))
Tactic: fin_cases i
Cleared hypotheses: i
-- 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 1
left : F.obj' 0 homMk₁._proof_2 ⟶ G.obj' 0 homMk₁._proof_2
right : F.obj' 1 homMk₁._proof_3 ⟶ G.obj' 1 homMk₁._proof_3
w : F.map' 0 1 homMk₁._proof_2 homMk₁._proof_3 ≫ right = left ≫ G.map' 0 1 homMk₁._proof_2 homMk₁._proof_3
i : ℕ
hi : i < 1
⊢ F.map' i (i + 1) ⋯ hi ≫
      (fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
          (match (motive := (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) → F.obj i ⟶ G.obj i) i with
            | ⟨0, isLt⟩ => left
            | ⟨1, isLt⟩ => right :
            F.obj i ⟶ G.obj i))
        ⟨i + 1, ⋯⟩ =
    (fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
          (match (motive := (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) → F.obj i ⟶ G.obj i) i with
            | ⟨0, isLt⟩ => left
            | ⟨1, isLt⟩ => right :
            F.obj i ⟶ G.obj i))
        (⟨i, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ≫
      G.map' i (i + 1) ⋯ hi
have obtain : ∀ (hi : LT.lt (α := ℕ) 0 1),
  Eq (α := F.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, sorry⟩)
    (F.map' 0 (HAdd.hAdd (α := ℕ) 0 1) sorry hi ≫
        (fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
            (match (motive := (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) → F.obj i ⟶ G.obj i) i with
              | ⟨0, isLt⟩ => left
              | ⟨1, isLt⟩ => right :
              F.obj i ⟶ G.obj i))
          ⟨HAdd.hAdd (α := ℕ) 0 1, sorry⟩ :
      F.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, sorry⟩)
    (CategoryStruct.comp (Y := G.obj ⟨0, sorry⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
              (match (motive := (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) → F.obj i ⟶ G.obj i) i with
                | ⟨0, isLt⟩ => left
                | ⟨1, isLt⟩ => right :
                F.obj i ⟶ G.obj i))
            ⟨0, sorry⟩ :
          F.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ G.obj ⟨0, sorry⟩)
        (G.map' 0 (HAdd.hAdd (α := ℕ) 0 1) sorry hi :
          G.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, sorry⟩) :
      F.obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, sorry⟩)
Tactic: obtain rfl : i = 0 := by simpa using hi
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
F G : ComposableArrows.{v_1, u_1} C 1
φ φ' : F ⟶ G
h₀ : app' φ 0 homMk₁._proof_2 = app' φ' 0 homMk₁._proof_2
h₁ : app' φ 1 homMk₁._proof_3 = app' φ' 1 homMk₁._proof_3
⊢ φ = φ'
have w : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 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
n m : ℕ
F_1 G_1 : ComposableArrows.{v_1, u_1} C n
F G : ComposableArrows.{v_1, u_1} C 1
left : F.obj' 0 homMk₁._proof_2 ≅ G.obj' 0 homMk₁._proof_2
right : F.obj' 1 homMk₁._proof_3 ≅ G.obj' 1 homMk₁._proof_3
w : F.map' 0 1 homMk₁._proof_2 homMk₁._proof_3 ≫ right.hom = left.hom ≫ G.map' 0 1 homMk₁._proof_2 homMk₁._proof_3
⊢ G.map' 0 1 homMk₁._proof_2 homMk₁._proof_3 ≫ right.inv = left.inv ≫ F.map' 0 1 homMk₁._proof_2 homMk₁._proof_3
have rw : G.map' 0 1 homMk₁._proof_2 homMk₁._proof_3 ≫ 𝟙 (G.obj' 1 homMk₁._proof_3) = G.map' 0 1 homMk₁._proof_2 homMk₁._proof_3
Tactic: rw [← cancel_mono right.hom, assoc, assoc, w, right.inv_hom_id, left.inv_hom_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 1
f : F ⟶ G
⊢ IsIso f ↔ IsIso (X := F.obj 0) (f.app 0) ∧ IsIso (X := F.obj 1) (f.app 1)
have rw : (∀ (X : Fin (HAdd.hAdd (α := ℕ) 1 1)), IsIso (f.app X)) ↔
  IsIso (X := F.obj 0) (f.app 0) ∧ IsIso (X := F.obj 1) (f.app 1)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- 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 1
f : F ⟶ G
h : IsIso (X := F.obj 0) (f.app 0) ∧ IsIso (X := F.obj 1) (f.app 1)
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ IsIso (f.app i)
have 0 : IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, sorry⟩))
  (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, sorry⟩))
Tactic: fin_cases i
Cleared hypotheses: 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 1
f : F ⟶ G
h : IsIso (X := F.obj 0) (f.app 0) ∧ IsIso (X := F.obj 1) (f.app 1)
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
0 :
  IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩))
    (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩))
⊢ IsIso (f.app i)
have 1 : IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, sorry⟩))
  (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, sorry⟩))
Tactic: fin_cases i
Cleared hypotheses: 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 1
f : F ⟶ G
h : IsIso (X := F.obj 0) (f.app 0) ∧ IsIso (X := F.obj 1) (f.app 1)
⊢ IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩))
    (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩))
have 0 : IsIso (X := F.obj 0) (f.app 0) →
  IsIso (X := F.obj 1) (f.app 1) →
    IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, sorry⟩))
      (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, sorry⟩))
Tactic: tauto
Cleared hypotheses: h
-- 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 1
f : F ⟶ G
h : IsIso (X := F.obj 0) (f.app 0) ∧ IsIso (X := F.obj 1) (f.app 1)
⊢ IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, ⋯⟩))
    (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, ⋯⟩))
have 1 : IsIso (X := F.obj 0) (f.app 0) →
  IsIso (X := F.obj 1) (f.app 1) →
    IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, sorry⟩))
      (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, sorry⟩))
Tactic: tauto
Cleared hypotheses: h
-- 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 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ F.obj i = G.obj i
have 0 : F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) =
  G.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: 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 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
0 :
  F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) =
    G.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩)
⊢ F.obj i = G.obj i
have 1 : F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) =
  G.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: 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 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ (isoMk₁ (eqToIso left) (eqToIso right) ⋯).hom.app i = eqToHom ⋯
have 0 : Eq (α :=
  F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) ⟶
    G.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, sorry⟩))
  ((isoMk₁ (eqToIso left) (eqToIso right) sorry).hom.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, sorry⟩)) (eqToHom sorry)
Tactic: fin_cases i
Cleared hypotheses: 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 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
0 :
  Eq (α :=
    F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) ⟶
      G.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩))
    ((isoMk₁ (eqToIso left) (eqToIso right) ⋯).hom.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩))
    (eqToHom ⋯)
⊢ (isoMk₁ (eqToIso left) (eqToIso right) ⋯).hom.app i = eqToHom ⋯
have 1 : Eq (α :=
  F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) ⟶
    G.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, sorry⟩))
  ((isoMk₁ (eqToIso left) (eqToIso right) sorry).hom.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, sorry⟩)) (eqToHom sorry)
Tactic: fin_cases i
Cleared hypotheses: i
-- 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
i : Fin (n + 1 + 1)
⊢ map F f i i ⋯ = 𝟙 (obj F X i)
have zero : ∀ (hi : 0 < n + 1 + 1), map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨0, hi⟩ : Fin (n + 1 + 1)) sorry = 𝟙 (obj F X ⟨0, hi⟩)
Tactic: obtain ⟨_ | _, hi⟩ := i
Cleared hypotheses: i
-- 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
i : Fin (n + 1 + 1)
zero : ∀ (hi : 0 < n + 1 + 1), map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨0, hi⟩ : Fin (n + 1 + 1)) ⋯ = 𝟙 (obj F X ⟨0, hi⟩)
⊢ map F f i i ⋯ = 𝟙 (obj F X i)
have succ : ∀ (n_1 : ℕ) (hi : n_1 + 1 < n + 1 + 1),
  map F f (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) sorry = 𝟙 (obj F X ⟨n_1 + 1, hi⟩)
Tactic: obtain ⟨_ | _, hi⟩ := i
Cleared hypotheses: i
-- 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
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
have obtain : ∀ (i : ℕ) (hi : i < n + 1 + 1) (hij : (⟨i, hi⟩ : Fin (n + 1 + 1)) ≤ j),
  map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) k sorry = map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) j hij ≫ map F f j k hjk
Tactic: obtain ⟨i, hi⟩ := i
Cleared hypotheses: i, 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 k : Fin (n + 1 + 1)
hjk : j ≤ k
i : ℕ
hi : i < n + 1 + 1
hij : (⟨i, hi⟩ : Fin (n + 1 + 1)) ≤ j
⊢ map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) k ⋯ = map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) j hij ≫ map F f j k hjk
have obtain : ∀ (j : ℕ) (hj : j < n + 1 + 1) (hjk : (⟨j, hj⟩ : Fin (n + 1 + 1)) ≤ k) (hij : (⟨i, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j, hj⟩),
  map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) k sorry =
    map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) (⟨j, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j, hj⟩ k hjk
Tactic: obtain ⟨j, hj⟩ := j
Cleared hypotheses: j, 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 : Fin (n + 1 + 1)
i : ℕ
hi : i < n + 1 + 1
j : ℕ
hj : j < n + 1 + 1
hjk : (⟨j, hj⟩ : Fin (n + 1 + 1)) ≤ k
hij : (⟨i, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j, hj⟩
⊢ map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) k ⋯ =
    map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) (⟨j, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j, hj⟩ k hjk
have obtain : ∀ (k : ℕ) (hk : k < n + 1 + 1) (hjk : (⟨j, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩),
  map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) (⟨k, hk⟩ : Fin (n + 1 + 1)) sorry =
    map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) (⟨j, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j, hj⟩ ⟨k, hk⟩ hjk
Tactic: obtain ⟨k, hk⟩ := k
Cleared hypotheses: k, 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
i : ℕ
hi : i < n + 1 + 1
j : ℕ
hj : j < n + 1 + 1
hij : (⟨i, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j, hj⟩
k : ℕ
hk : k < n + 1 + 1
hjk : (⟨j, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩
⊢ map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) (⟨k, hk⟩ : Fin (n + 1 + 1)) ⋯ =
    map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) (⟨j, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j, hj⟩ ⟨k, hk⟩ hjk
have zero : ∀ (hi : 0 < n + 1 + 1) (hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j, hj⟩),
  map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨k, hk⟩ : Fin (n + 1 + 1)) sorry =
    map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨j, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j, hj⟩ ⟨k, hk⟩ hjk
Tactic: cases i
Cleared hypotheses: i, hi, 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
i : ℕ
hi : i < n + 1 + 1
j : ℕ
hj : j < n + 1 + 1
hij : (⟨i, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j, hj⟩
k : ℕ
hk : k < n + 1 + 1
hjk : (⟨j, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩
zero :
  ∀ (hi : 0 < n + 1 + 1) (hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j, 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, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j, hj⟩ ⟨k, hk⟩ hjk
⊢ map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) (⟨k, hk⟩ : Fin (n + 1 + 1)) ⋯ =
    map F f (⟨i, hi⟩ : Fin (n + 1 + 1)) (⟨j, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j, hj⟩ ⟨k, hk⟩ hjk
have succ : ∀ (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)) sorry =
    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
Tactic: cases i
Cleared hypotheses: i, hi, 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⟩
hi : 0 < n + 1 + 1
hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j, 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, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j, hj⟩ ⟨k, hk⟩ hjk
have zero : ∀ (hj : 0 < n + 1 + 1) (hjk : (⟨0, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩) (hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨0, hj⟩),
  map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨k, hk⟩ : Fin (n + 1 + 1)) sorry =
    map F f (⟨0, 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⟩
hi : 0 < n + 1 + 1
hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j, hj⟩
zero :
  ∀ (hj : 0 < n + 1 + 1) (hjk : (⟨0, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩) (hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨0, 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)) (⟨0, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨0, hj⟩ ⟨k, 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, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j, hj⟩ ⟨k, hk⟩ hjk
have zero₁ : ∀ (hj : HAdd.hAdd (α := ℕ) 0 1 < n + 1 + 1) (hjk : (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩)
  (hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩),
  map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨k, hk⟩ : Fin (n + 1 + 1)) sorry =
    map F f (⟨0, hi⟩ : Fin (n + 1 + 1)) (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
      map F f ⟨HAdd.hAdd (α := ℕ) 0 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
j : ℕ
hj : j < n + 1 + 1
k : ℕ
hk : k < n + 1 + 1
hjk : (⟨j, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩
hi : 0 < n + 1 + 1
hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j, hj⟩
zero :
  ∀ (hj : 0 < n + 1 + 1) (hjk : (⟨0, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩) (hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨0, 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)) (⟨0, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨0, hj⟩ ⟨k, hk⟩ hjk
zero₁ :
  ∀ (hj : HAdd.hAdd (α := ℕ) 0 1 < n + 1 + 1) (hjk : (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩)
    (hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨HAdd.hAdd (α := ℕ) 0 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)) (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
        map F f ⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ ⟨k, 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, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨j, hj⟩ ⟨k, hk⟩ hjk
have zero₂ : ∀ (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)) 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, 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
hi hj : 0 < n + 1 + 1
hjk : (⟨0, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩
hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨0, 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)) (⟨0, hj⟩ : Fin (n + 1 + 1)) hij ≫ map F f ⟨0, hj⟩ ⟨k, hk⟩ hjk
have zero : map F f 0 (⟨k, hk⟩ : Fin (n + 1 + 1)) sorry = 𝟙 X ≫ map F f 0 (⟨k, hk⟩ : Fin (n + 1 + 1)) hjk
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
k : ℕ
hk : k < n + 1 + 1
hi hj : 0 < n + 1 + 1
hjk : (⟨0, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩
hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨0, hj⟩
⊢ map F f 0 (⟨k, hk⟩ : Fin (n + 1 + 1)) ⋯ = 𝟙 X ≫ map F f 0 (⟨k, hk⟩ : Fin (n + 1 + 1)) hjk
have zero : map F f 0 (⟨k, hk⟩ : Fin (n + 1 + 1)) sorry = map F f 0 ⟨k, hk⟩ hjk
Tactic: rw [id_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
k : ℕ
hk : k < n + 1 + 1
hi : 0 < n + 1 + 1
hj : HAdd.hAdd (α := ℕ) 0 1 < n + 1 + 1
hjk : (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩
hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨HAdd.hAdd (α := ℕ) 0 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)) (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
      map F f ⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ ⟨k, hk⟩ hjk
have zero : ∀ (hk : 0 < n + 1 + 1) (hjk : (⟨HAdd.hAdd (α := ℕ) 0 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)) (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
      map F f ⟨HAdd.hAdd (α := ℕ) 0 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
hj : HAdd.hAdd (α := ℕ) 0 1 < n + 1 + 1
hjk : (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩
hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩
zero :
  ∀ (hk : 0 < n + 1 + 1) (hjk : (⟨HAdd.hAdd (α := ℕ) 0 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)) (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
        map F f ⟨HAdd.hAdd (α := ℕ) 0 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)) (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
      map F f ⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ ⟨k, hk⟩ hjk
have zero₁ : ∀ (hk : HAdd.hAdd (α := ℕ) 0 1 < n + 1 + 1)
  (hjk : (⟨HAdd.hAdd (α := ℕ) 0 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)) (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
      map F f ⟨HAdd.hAdd (α := ℕ) 0 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
hj : HAdd.hAdd (α := ℕ) 0 1 < n + 1 + 1
hjk : (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) ≤ ⟨k, hk⟩
hij : (⟨0, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩
zero :
  ∀ (hk : 0 < n + 1 + 1) (hjk : (⟨HAdd.hAdd (α := ℕ) 0 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)) (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
        map F f ⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ ⟨0, hk⟩ hjk
zero₁ :
  ∀ (hk : HAdd.hAdd (α := ℕ) 0 1 < n + 1 + 1)
    (hjk : (⟨HAdd.hAdd (α := ℕ) 0 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)) (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
        map F f ⟨HAdd.hAdd (α := ℕ) 0 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)) (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
      map F f ⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ ⟨k, hk⟩ hjk
have zero₂ : ∀ (k : ℕ) (hk : k + 1 + 1 < n + 1 + 1) (hjk : (⟨HAdd.hAdd (α := ℕ) 0 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)) (⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ : Fin (n + 1 + 1)) hij ≫
      map F f ⟨HAdd.hAdd (α := ℕ) 0 1, hj⟩ ⟨k + 1 + 1, hk⟩ hjk
Tactic: obtain _ | _ | k := k
Cleared hypotheses: k, hk, hjk