awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
B : Type u_5
inst_2 : AddCommMonoid B
inst_3 : HasShift.{v_1, u_1, u_5} C B
inst_4 : HasShift.{v_2, u_2, u_5} D B
inst_5 : F.CommShift B
X : C
a b : B
eq :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)))
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) X) ⟶
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b ⋙ shiftFunctor C a) X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorComm C a b)) X))
    (CategoryStruct.comp (Y := (F ⋙ shiftFunctor D b).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.hom (shiftFunctorComm D a b)) (F.obj X) ≫
          map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
            NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
have simp : Eq (α :=
  F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) X) ⟶
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b ⋙ shiftFunctor C a) X))
  (F.map (NatTrans.app (Iso.hom (shiftFunctorComm C a b)) X))
  (CategoryStruct.comp (Y := (F ⋙ shiftFunctor D b).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
    (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
    (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
      NatTrans.app (Iso.hom (Iso.symm (shiftFunctorAdd' D a b (a + b) sorry) ≪≫ shiftFunctorAdd' D b a (a + b) sorry))
          (F.obj X) ≫
        map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
          NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
Tactic: simp only [shiftFunctorComm_eq D a b _ rfl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
B : Type u_5
inst_2 : AddCommMonoid B
inst_3 : HasShift.{v_1, u_1, u_5} C B
inst_4 : HasShift.{v_2, u_2, u_5} D B
inst_5 : F.CommShift B
X : C
a b : B
eq :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)))
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) X) ⟶
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b ⋙ shiftFunctor C a) X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorComm C a b)) X))
    (CategoryStruct.comp (Y := (F ⋙ shiftFunctor D b).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.hom (Iso.symm (shiftFunctorAdd' D a b (a + b) ⋯) ≪≫ shiftFunctorAdd' D b a (a + b) ⋯))
            (F.obj X) ≫
          map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
            NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
have dsimp : Eq (α :=
  F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
  (F.map (NatTrans.app (Iso.hom (shiftFunctorComm C a b)) X))
  (CategoryStruct.comp (Y :=
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
    (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
      (NatTrans.app (Iso.inv (shiftFunctorAdd' D a b (a + b) sorry)) (F.obj X) ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd' D b a (a + b) sorry)) (F.obj X)) ≫
        map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
          NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
B : Type u_5
inst_2 : AddCommMonoid B
inst_3 : HasShift.{v_1, u_1, u_5} C B
inst_4 : HasShift.{v_2, u_2, u_5} D B
inst_5 : F.CommShift B
X : C
a b : B
eq :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)))
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorComm C a b)) X))
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        (NatTrans.app (Iso.inv (shiftFunctorAdd' D a b (a + b) ⋯)) (F.obj X) ≫
            NatTrans.app (Iso.hom (shiftFunctorAdd' D b a (a + b) ⋯)) (F.obj X)) ≫
          map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
            NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
have simp : Eq (α :=
  F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
  (F.map (NatTrans.app (Iso.hom (Iso.symm (shiftFunctorAdd C a b) ≪≫ shiftFunctorAdd' C b a (a + b) sorry)) X))
  (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫
    CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
      (NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
      (NatTrans.app (Iso.hom (shiftFunctorAdd' D b a (a + b) sorry)) (F.obj X) ≫
        map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
          NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
Tactic: simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, Category.assoc,
    ← reassoc_of% eq, shiftFunctorComm_eq C a b _ rfl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
B : Type u_5
inst_2 : AddCommMonoid B
inst_3 : HasShift.{v_1, u_1, u_5} C B
inst_4 : HasShift.{v_2, u_2, u_5} D B
inst_5 : F.CommShift B
X : C
a b : B
eq :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)))
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
    (F.map (NatTrans.app (Iso.hom (Iso.symm (shiftFunctorAdd C a b) ≪≫ shiftFunctorAdd' C b a (a + b) ⋯)) X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫
      CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
        (NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
        (NatTrans.app (Iso.hom (shiftFunctorAdd' D b a (a + b) ⋯)) (F.obj X) ≫
          map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
            NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
have dsimp : Eq (α :=
  F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
  (F.map
    (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C b a (a + b) sorry)) X))
  (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫
    CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
      (NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
      (NatTrans.app (Iso.hom (shiftFunctorAdd' D b a (a + b) sorry)) (F.obj X) ≫
        map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
          NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
B : Type u_5
inst_2 : AddCommMonoid B
inst_3 : HasShift.{v_1, u_1, u_5} C B
inst_4 : HasShift.{v_2, u_2, u_5} D B
inst_5 : F.CommShift B
X : C
a b : B
eq :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)))
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
    (F.map
      (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C b a (a + b) ⋯)) X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫
      CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
        (NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
        (NatTrans.app (Iso.hom (shiftFunctorAdd' D b a (a + b) ⋯)) (F.obj X) ≫
          map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
            NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
have rw : Eq (α :=
  F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
  (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C b a (a + b) sorry)) X))
  (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫
    CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
      (NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
      (NatTrans.app (Iso.hom (shiftFunctorAdd' D b a (a + b) sorry)) (F.obj X) ≫
        map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
          NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
Tactic: rw [Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
inst_5 : F.CommShift A
X : C
a b : A
h : a + b = 0
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) X) ⟶ F.obj (obj.{v_1, v_1, u_1, u_1} (𝟭 C) X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C a b h)) X))
    (CategoryStruct.comp (Y := (F ⋙ shiftFunctor D b).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a b h)) (F.obj X)))
have dsimp : Eq (α := F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶ F.obj X)
  (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C a b 0 h)) X ≫ NatTrans.app (Iso.hom (shiftFunctorZero C A)) X))
  (CategoryStruct.comp (Y :=
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
    (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' D a b 0 h)) (F.obj X) ≫
        NatTrans.app (Iso.hom (shiftFunctorZero D A)) (F.obj X)))
Tactic: dsimp [shiftFunctorCompIsoId]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
inst_5 : F.CommShift A
X : C
a b : A
h : a + b = 0
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶ F.obj X)
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C a b 0 h)) X ≫ NatTrans.app (Iso.hom (shiftFunctorZero C A)) X))
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' D a b 0 h)) (F.obj X) ≫
          NatTrans.app (Iso.hom (shiftFunctorZero D A)) (F.obj X)))
have eq : Eq (α := (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ F).obj X ⟶ (F ⋙ shiftFunctor.{v_2, u_2, u_4} D (A := A) 0).obj X)
  (NatTrans.app (Iso.hom (commShiftIso F 0)) X)
  (NatTrans.app (Iso.hom (CommShift.isoAdd' h (commShiftIso F a) (commShiftIso F b))) X)
Tactic: have eq := NatTrans.congr_app (congr_arg Iso.hom (F.commShiftIso_add' h)) X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
inst_5 : F.CommShift A
X : C
a b : A
h : a + b = 0
eq :
  Eq (α :=
    (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ F).obj X ⟶ (F ⋙ shiftFunctor.{v_2, u_2, u_4} D (A := A) 0).obj X)
    (NatTrans.app (Iso.hom (commShiftIso F 0)) X)
    (NatTrans.app (Iso.hom (CommShift.isoAdd' h (commShiftIso F a) (commShiftIso F b))) X)
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶ F.obj X)
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C a b 0 h)) X ≫ NatTrans.app (Iso.hom (shiftFunctorZero C A)) X))
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' D a b 0 h)) (F.obj X) ≫
          NatTrans.app (Iso.hom (shiftFunctorZero D A)) (F.obj X)))
have eq₁ : Eq (α :=
  F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) X) ⟶
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_4} D (A := A) 0) (F.obj X))
  (F.map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X) ≫ NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
  (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b 0 h)) X) ≫
    CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' D a b 0 h)) (F.obj X)))
Tactic: simp only [commShiftIso_zero, comp_obj, CommShift.isoZero_hom_app,
    CommShift.isoAdd'_hom_app] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
inst_5 : F.CommShift A
X : C
a b : A
h : a + b = 0
eq :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) X) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_4} D (A := A) 0) (F.obj X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X) ≫ NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b 0 h)) X) ≫
      CategoryStruct.comp (Y :=
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
        (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
        (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' D a b 0 h)) (F.obj X)))
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶ F.obj X)
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C a b 0 h)) X ≫ NatTrans.app (Iso.hom (shiftFunctorZero C A)) X))
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' D a b 0 h)) (F.obj X) ≫
          NatTrans.app (Iso.hom (shiftFunctorZero D A)) (F.obj X)))
have rw : Eq (α := F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) X) ⟶ F.obj X)
  (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b 0 h)) X) ≫
    F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C a b 0 h)) X) ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X))
  (F.map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X) ≫
    CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_4} D (A := A) 0) (F.obj X))
      (NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
      (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (F.obj X)))
Tactic: rw [← cancel_epi (F.map ((shiftFunctorAdd' C a b 0 h).hom.app X)), ← reassoc_of% eq, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
inst_5 : F.CommShift A
X : C
a b : A
h : a + b = 0
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ⟶ F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C a b h)) X))
    (CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a ⋙ shiftFunctor D b) (F.obj X))
      (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D a b h)) (F.obj X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.inv (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
have rw : 𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) X)) =
  CategoryStruct.comp (Y := (F ⋙ shiftFunctor D b).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a b h)) (F.obj X)) ≫
    CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a ⋙ shiftFunctor D b) (F.obj X))
      (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D a b h)) (F.obj X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.inv (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
Tactic: rw [← cancel_epi (F.map ((shiftFunctorCompIsoId C a b h).hom.app X)), ← F.map_comp,
    Iso.hom_inv_id_app, F.map_id, map_shiftFunctorCompIsoId_hom_app]