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 : 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 α.inv β.inv ⋯ ≫ homMkSucc α.hom β.hom w) 0 ⋯ = app' (𝟙 G) 0 ⋯
⊢ homMkSucc α.inv β.inv ⋯ ≫ homMkSucc α.hom β.hom w = 𝟙 G
have h₁ : Eq (α := Functor.obj δ₀Functor G ⟶ Functor.obj δ₀Functor G)
  (Functor.map δ₀Functor (homMkSucc α.inv β.inv sorry ≫ homMkSucc α.hom β.hom w)) (Functor.map δ₀Functor (𝟙 G))
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 G ⟶ Functor.obj δ₀Functor G)
    (Functor.map δ₀Functor (homMkSucc α.inv β.inv ⋯ ≫ homMkSucc α.hom β.hom w)) (Functor.map δ₀Functor (𝟙 G))
have h₁ : ∀ (i : ℕ) (hi : i < n + 1),
  Eq (α := (Functor.obj δ₀Functor G).obj (⟨i, hi⟩ : Fin (n + 1)) ⟶ (Functor.obj δ₀Functor G).obj ⟨i, hi⟩)
    (NatTrans.app (Functor.map δ₀Functor (homMkSucc α.inv β.inv sorry ≫ homMkSucc α.hom β.hom w)) ⟨i, hi⟩)
    (NatTrans.app (Functor.map δ₀Functor (𝟙 G)) ⟨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)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj ⟨1, ⋯⟩)
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨1, ⋯⟩)
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)
i : ℕ
hi : i < n + 1 + 1
⊢ F.obj (⟨i, hi⟩ : Fin (n + 1 + 1)) = G.obj ⟨i, hi⟩
have zero : ∀ (hi : 0 < n + 1 + 1), F.obj (⟨0, hi⟩ : Fin (n + 1 + 1)) = G.obj ⟨0, hi⟩
Tactic: rcases i with - | 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)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj ⟨1, ⋯⟩)
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨1, ⋯⟩)
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)
i : ℕ
hi : i < n + 1 + 1
zero : ∀ (hi : 0 < n + 1 + 1), F.obj (⟨0, hi⟩ : Fin (n + 1 + 1)) = G.obj ⟨0, hi⟩
⊢ F.obj (⟨i, hi⟩ : Fin (n + 1 + 1)) = G.obj ⟨i, hi⟩
have succ : ∀ (i : ℕ) (hi : i + 1 < n + 1 + 1), F.obj (⟨i + 1, hi⟩ : Fin (n + 1 + 1)) = G.obj ⟨i + 1, hi⟩
Tactic: rcases i with - | i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows.{v_1, u_1} C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj ⟨1, ⋯⟩)
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨1, ⋯⟩)
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)
⊢ F = G
have this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
Tactic: have : ∀ i, F.obj i = G.obj i := by
    intro ⟨i, hi⟩
    rcases i with - | i
    · exact h₀
    · exact Functor.congr_obj h ⟨i, 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 : ℕ
F G : ComposableArrows.{v_1, u_1} C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj ⟨1, ⋯⟩)
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨1, ⋯⟩)
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' (Iso.hom (eqToIso h)) 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (Iso.hom (eqToIso h₀) ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
have rw : (eqToHom h₀ ≫
      CategoryStruct.comp (Y := G.obj (⟨1, sorry⟩ : Fin (n + 1 + 1)))
        (G.map' 0 1 homMk₁._proof_2 sorry : G.obj (⟨0, sorry⟩ : Fin (n + 1 + 1)) ⟶ G.obj (⟨1, sorry⟩ : Fin (n + 1 + 1)))
        (eqToHom sorry : G.obj (⟨1, sorry⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0)) ≫
    app' (Iso.hom (eqToIso h)) 0 sorry =
  Iso.hom (eqToIso h₀) ≫ G.map' 0 1 homMk₁._proof_2 sorry
Tactic: rw [w]
-- 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)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj ⟨1, ⋯⟩)
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨1, ⋯⟩)
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)))
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)))
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0)) ≫
      app' (Iso.hom (eqToIso h)) 0 ⋯ =
    Iso.hom (eqToIso h₀) ≫ G.map' 0 1 homMk₁._proof_2 ⋯
have dsimp : Eq (α := F.obj 0 ⟶ G.obj 1)
  (CategoryStruct.comp (Y := F.obj 1)
      (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE sorry) : G.obj 0 ⟶ G.obj 1) (eqToHom sorry : G.obj 1 ⟶ F.obj 1))
      (NatTrans.app (eqToHom h) 0) :
    F.obj 0 ⟶ G.obj 1)
  (eqToHom h₀ ≫ G.map (homOfLE sorry) : F.obj 0 ⟶ G.obj 1)
Tactic: dsimp [app']
-- 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)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj ⟨1, ⋯⟩)
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨1, ⋯⟩)
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ Eq (α := F.obj 0 ⟶ G.obj 1)
    (CategoryStruct.comp (Y := F.obj 1)
        (eqToHom h₀ ≫
          CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (eqToHom ⋯ : G.obj 1 ⟶ F.obj 1))
        (NatTrans.app (eqToHom h) 0) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
have rw : Eq (α := F.obj 0 ⟶ G.obj 1)
  (CategoryStruct.comp (Y := F.obj 1)
      (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE sorry) : G.obj 0 ⟶ G.obj 1) (eqToHom sorry : G.obj 1 ⟶ F.obj 1))
      (eqToHom sorry) :
    F.obj 0 ⟶ G.obj 1)
  (eqToHom h₀ ≫ G.map (homOfLE sorry) : F.obj 0 ⟶ G.obj 1)
Tactic: rw [eqToHom_app, assoc, assoc, eqToHom_trans, eqToHom_refl, 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 : ℕ
F G : ComposableArrows.{v_1, u_1} C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj ⟨1, ⋯⟩)
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨1, ⋯⟩)
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
rw :
  Eq (α := F.obj 0 ⟶ G.obj 1)
    (CategoryStruct.comp (Y := F.obj 1)
        (eqToHom h₀ ≫
          CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (eqToHom ⋯ : G.obj 1 ⟶ F.obj 1))
        (eqToHom ⋯) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
⊢ Eq (α := F.obj 0 ⟶ G.obj 1)
    (CategoryStruct.comp (Y := F.obj 1)
        (eqToHom h₀ ≫
          CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (eqToHom ⋯ : G.obj 1 ⟶ F.obj 1))
        (NatTrans.app (eqToHom h) 0) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
have rw₁ : Eq (α := F.obj 0 ⟶ G.obj 1)
  (eqToHom h₀ ≫
      CategoryStruct.comp (Y := F.obj 1)
        (CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE sorry) : G.obj 0 ⟶ G.obj 1) (eqToHom sorry : G.obj 1 ⟶ F.obj 1))
        (eqToHom sorry) :
    F.obj 0 ⟶ G.obj 1)
  (eqToHom h₀ ≫ G.map (homOfLE sorry) : F.obj 0 ⟶ G.obj 1)
Tactic: rw [eqToHom_app, assoc, assoc, eqToHom_trans, eqToHom_refl, 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 : ℕ
F G : ComposableArrows.{v_1, u_1} C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj ⟨1, ⋯⟩)
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨1, ⋯⟩)
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
rw :
  Eq (α := F.obj 0 ⟶ G.obj 1)
    (CategoryStruct.comp (Y := F.obj 1)
        (eqToHom h₀ ≫
          CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (eqToHom ⋯ : G.obj 1 ⟶ F.obj 1))
        (eqToHom ⋯) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
rw₁ :
  Eq (α := F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := F.obj 1)
          (CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (eqToHom ⋯ : G.obj 1 ⟶ F.obj 1))
          (eqToHom ⋯) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
⊢ Eq (α := F.obj 0 ⟶ G.obj 1)
    (CategoryStruct.comp (Y := F.obj 1)
        (eqToHom h₀ ≫
          CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (eqToHom ⋯ : G.obj 1 ⟶ F.obj 1))
        (NatTrans.app (eqToHom h) 0) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
have rw₂ : Eq (α := F.obj 0 ⟶ G.obj 1)
  (eqToHom h₀ ≫
      CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE sorry) : G.obj 0 ⟶ G.obj 1)
        (CategoryStruct.comp (Y := F.obj 1) (eqToHom sorry) (eqToHom sorry) : G.obj 1 ⟶ G.obj 1) :
    F.obj 0 ⟶ G.obj 1)
  (eqToHom h₀ ≫ G.map (homOfLE sorry) : F.obj 0 ⟶ G.obj 1)
Tactic: rw [eqToHom_app, assoc, assoc, eqToHom_trans, eqToHom_refl, 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 : ℕ
F G : ComposableArrows.{v_1, u_1} C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj ⟨1, ⋯⟩)
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨1, ⋯⟩)
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
rw :
  Eq (α := F.obj 0 ⟶ G.obj 1)
    (CategoryStruct.comp (Y := F.obj 1)
        (eqToHom h₀ ≫
          CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (eqToHom ⋯ : G.obj 1 ⟶ F.obj 1))
        (eqToHom ⋯) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
rw₁ :
  Eq (α := F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := F.obj 1)
          (CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (eqToHom ⋯ : G.obj 1 ⟶ F.obj 1))
          (eqToHom ⋯) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
rw₂ :
  Eq (α := F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1)
          (CategoryStruct.comp (Y := F.obj 1) (eqToHom ⋯) (eqToHom ⋯) : G.obj 1 ⟶ G.obj 1) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
⊢ Eq (α := F.obj 0 ⟶ G.obj 1)
    (CategoryStruct.comp (Y := F.obj 1)
        (eqToHom h₀ ≫
          CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (eqToHom ⋯ : G.obj 1 ⟶ F.obj 1))
        (NatTrans.app (eqToHom h) 0) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
have rw₃ : Eq (α := F.obj 0 ⟶ G.obj 1)
  (eqToHom h₀ ≫
      CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE sorry) : G.obj 0 ⟶ G.obj 1) (eqToHom sorry : G.obj 1 ⟶ G.obj 1) :
    F.obj 0 ⟶ G.obj 1)
  (eqToHom h₀ ≫ G.map (homOfLE sorry) : F.obj 0 ⟶ G.obj 1)
Tactic: rw [eqToHom_app, assoc, assoc, eqToHom_trans, eqToHom_refl, 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 : ℕ
F G : ComposableArrows.{v_1, u_1} C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj ⟨1, ⋯⟩)
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨1, ⋯⟩)
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
rw :
  Eq (α := F.obj 0 ⟶ G.obj 1)
    (CategoryStruct.comp (Y := F.obj 1)
        (eqToHom h₀ ≫
          CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (eqToHom ⋯ : G.obj 1 ⟶ F.obj 1))
        (eqToHom ⋯) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
rw₁ :
  Eq (α := F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := F.obj 1)
          (CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (eqToHom ⋯ : G.obj 1 ⟶ F.obj 1))
          (eqToHom ⋯) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
rw₂ :
  Eq (α := F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1)
          (CategoryStruct.comp (Y := F.obj 1) (eqToHom ⋯) (eqToHom ⋯) : G.obj 1 ⟶ G.obj 1) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
rw₃ :
  Eq (α := F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (eqToHom ⋯ : G.obj 1 ⟶ G.obj 1) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
⊢ Eq (α := F.obj 0 ⟶ G.obj 1)
    (CategoryStruct.comp (Y := F.obj 1)
        (eqToHom h₀ ≫
          CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (eqToHom ⋯ : G.obj 1 ⟶ F.obj 1))
        (NatTrans.app (eqToHom h) 0) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
have rw₄ : eqToHom h₀ ≫
    CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE sorry) : G.obj 0 ⟶ G.obj 1) (𝟙 (G.obj 1) : G.obj 1 ⟶ G.obj 1) =
  eqToHom h₀ ≫ G.map (homOfLE sorry)
Tactic: rw [eqToHom_app, assoc, assoc, eqToHom_trans, eqToHom_refl, 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 : ℕ
F G : ComposableArrows.{v_1, u_1} C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj ⟨1, ⋯⟩)
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨1, ⋯⟩)
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
rw :
  Eq (α := F.obj 0 ⟶ G.obj 1)
    (CategoryStruct.comp (Y := F.obj 1)
        (eqToHom h₀ ≫
          CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (eqToHom ⋯ : G.obj 1 ⟶ F.obj 1))
        (eqToHom ⋯) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
rw₁ :
  Eq (α := F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := F.obj 1)
          (CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (eqToHom ⋯ : G.obj 1 ⟶ F.obj 1))
          (eqToHom ⋯) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
rw₂ :
  Eq (α := F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1)
          (CategoryStruct.comp (Y := F.obj 1) (eqToHom ⋯) (eqToHom ⋯) : G.obj 1 ⟶ G.obj 1) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
rw₃ :
  Eq (α := F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (eqToHom ⋯ : G.obj 1 ⟶ G.obj 1) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
rw₄ :
  eqToHom h₀ ≫
      CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (𝟙 (G.obj 1) : G.obj 1 ⟶ G.obj 1) =
    eqToHom h₀ ≫ G.map (homOfLE ⋯)
⊢ Eq (α := F.obj 0 ⟶ G.obj 1)
    (CategoryStruct.comp (Y := F.obj 1)
        (eqToHom h₀ ≫
          CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (eqToHom ⋯ : G.obj 1 ⟶ F.obj 1))
        (NatTrans.app (eqToHom h) 0) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
have rw₅ : Eq (α := F.obj 0 ⟶ G.obj 1) (eqToHom h₀ ≫ G.map (homOfLE sorry) : F.obj 0 ⟶ G.obj 1)
  (eqToHom h₀ ≫ G.map (homOfLE sorry) : F.obj 0 ⟶ G.obj 1)
Tactic: rw [eqToHom_app, assoc, assoc, eqToHom_trans, eqToHom_refl, 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 G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 2
app₀ : f.obj' 0 _proof_7 ≅ g.obj' 0 _proof_7
app₁ : f.obj' 1 _proof_8 ≅ g.obj' 1 _proof_8
app₂ : f.obj' 2 _proof_9 ≅ g.obj' 2 _proof_9
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_8
w₁ : f.map' 1 2 _proof_8 _proof_9 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_9
⊢ g.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_8
have rw : app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁.inv = app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_8
Tactic: rw [← cancel_epi app₀.hom, ← reassoc_of% w₀, app₁.hom_inv_id,
      comp_id, app₀.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 G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 2
app₀ : f.obj' 0 _proof_7 ≅ g.obj' 0 _proof_7
app₁ : f.obj' 1 _proof_8 ≅ g.obj' 1 _proof_8
app₂ : f.obj' 2 _proof_9 ≅ g.obj' 2 _proof_9
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_8
w₁ : f.map' 1 2 _proof_8 _proof_9 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_9
rw :
  app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁.inv = app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_8
⊢ g.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_8
have rw₁ : f.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁.hom ≫ app₁.inv = app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_8
Tactic: rw [← cancel_epi app₀.hom, ← reassoc_of% w₀, app₁.hom_inv_id,
      comp_id, app₀.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 G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 2
app₀ : f.obj' 0 _proof_7 ≅ g.obj' 0 _proof_7
app₁ : f.obj' 1 _proof_8 ≅ g.obj' 1 _proof_8
app₂ : f.obj' 2 _proof_9 ≅ g.obj' 2 _proof_9
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_8
w₁ : f.map' 1 2 _proof_8 _proof_9 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_9
rw :
  app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁.inv = app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_8
rw₁ :
  f.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁.hom ≫ app₁.inv = app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_8
⊢ g.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_8
have rw₂ : f.map' 0 1 homMk₁._proof_2 _proof_8 ≫ 𝟙 (f.obj' 1 _proof_8) = app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_8
Tactic: rw [← cancel_epi app₀.hom, ← reassoc_of% w₀, app₁.hom_inv_id,
      comp_id, app₀.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 G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 2
app₀ : f.obj' 0 _proof_7 ≅ g.obj' 0 _proof_7
app₁ : f.obj' 1 _proof_8 ≅ g.obj' 1 _proof_8
app₂ : f.obj' 2 _proof_9 ≅ g.obj' 2 _proof_9
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_8
w₁ : f.map' 1 2 _proof_8 _proof_9 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_9
rw :
  app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁.inv = app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_8
rw₁ :
  f.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁.hom ≫ app₁.inv = app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_8
rw₂ :
  f.map' 0 1 homMk₁._proof_2 _proof_8 ≫ 𝟙 (f.obj' 1 _proof_8) =
    app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_8
⊢ g.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_8
have rw₃ : f.map' 0 1 homMk₁._proof_2 _proof_8 = app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_8
Tactic: rw [← cancel_epi app₀.hom, ← reassoc_of% w₀, app₁.hom_inv_id,
      comp_id, app₀.hom_inv_id_assoc]