awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
rw :
  𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)) =
    map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
          (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        𝟙
            (obj.{v, v, u, u} (shiftFunctor C n)
              (obj.{v, v, u, u} (shiftFunctor C m)
                (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)))) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
              (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
            map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X)
⊢ 𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)) =
    map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
          (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        map (shiftFunctor C n)
            (𝟙
              (obj.{v, v, u, u} (shiftFunctor C m)
                (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)))) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
              (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
            map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X)
have rw₁ : 𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)) =
  map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' sorry)) X) ≫
    NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
        (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
          (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' sorry)) X)
Tactic: rw [Functor.map_id, Category.id_comp, Iso.hom_inv_id_app_assoc,
    ← Functor.map_comp, Iso.hom_inv_id_app, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
rw :
  𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)) =
    map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
          (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        𝟙
            (obj.{v, v, u, u} (shiftFunctor C n)
              (obj.{v, v, u, u} (shiftFunctor C m)
                (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)))) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
              (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
            map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X)
rw₁ :
  𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)) =
    map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
          (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
            (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X)
⊢ 𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)) =
    map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
          (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        map (shiftFunctor C n)
            (𝟙
              (obj.{v, v, u, u} (shiftFunctor C m)
                (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)))) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
              (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
            map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X)
have rw₂ : 𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)) =
  map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' sorry)) X) ≫
    map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' sorry)) X)
Tactic: rw [Functor.map_id, Category.id_comp, Iso.hom_inv_id_app_assoc,
    ← Functor.map_comp, Iso.hom_inv_id_app, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
rw :
  𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)) =
    map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
          (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        𝟙
            (obj.{v, v, u, u} (shiftFunctor C n)
              (obj.{v, v, u, u} (shiftFunctor C m)
                (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)))) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
              (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
            map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X)
rw₁ :
  𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)) =
    map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
          (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
            (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X)
rw₂ :
  𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)) =
    map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
      map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X)
⊢ 𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)) =
    map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
          (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        map (shiftFunctor C n)
            (𝟙
              (obj.{v, v, u, u} (shiftFunctor C m)
                (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)))) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
              (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
            map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X)
have rw₃ : 𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)) =
  map (shiftFunctor C p)
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' sorry)) X ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' sorry)) X)
Tactic: rw [Functor.map_id, Category.id_comp, Iso.hom_inv_id_app_assoc,
    ← Functor.map_comp, Iso.hom_inv_id_app, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
i j k : A
h rw : i + j = k
⊢ j + i = k
have rw₁ : k = k
Tactic: rw [add_comm j i, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
i j k : A
h : i + j = k
⊢ Eq (α :=
    Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C i ⋙ shiftFunctor C j) (shiftFunctor C j ⋙ shiftFunctor C i))
    (shiftFunctorComm C i j) (Iso.symm (shiftFunctorAdd' C i j k h) ≪≫ shiftFunctorAdd' C j i k ⋯)
have subst : Eq (α :=
  Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C i ⋙ shiftFunctor C j) (shiftFunctor C j ⋙ shiftFunctor C i))
  (shiftFunctorComm C i j) (Iso.symm (shiftFunctorAdd' C i j (i + j) sorry) ≪≫ shiftFunctorAdd' C j i (i + j) sorry)
Tactic: subst h
Cleared hypotheses: k, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
i j : A
⊢ Eq (α :=
    Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C i ⋙ shiftFunctor C j) (shiftFunctor C j ⋙ shiftFunctor C i))
    (shiftFunctorComm C i j) (Iso.symm (shiftFunctorAdd' C i j (i + j) ⋯) ≪≫ shiftFunctorAdd' C j i (i + j) ⋯)
have rw : Eq (α :=
  Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C i ⋙ shiftFunctor C j) (shiftFunctor C j ⋙ shiftFunctor C i))
  (shiftFunctorComm C i j) (Iso.symm (shiftFunctorAdd C i j) ≪≫ shiftFunctorAdd' C j i (i + j) sorry)
Tactic: rw [shiftFunctorAdd'_eq_shiftFunctorAdd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
i : A
⊢ Eq (α :=
    Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C i ⋙ shiftFunctor C i) (shiftFunctor C i ⋙ shiftFunctor C i))
    (shiftFunctorComm C i i) (Iso.refl (shiftFunctor C i ⋙ shiftFunctor C i))
have rw : Eq (α :=
  Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C i ⋙ shiftFunctor C i) (shiftFunctor C i ⋙ shiftFunctor C i))
  (Iso.symm (shiftFunctorAdd' C i i (i + i) sorry) ≪≫ shiftFunctorAdd' C i i (i + i) sorry)
  (Iso.refl (shiftFunctor C i ⋙ shiftFunctor C i))
Tactic: rw [shiftFunctorComm_eq C i i (i + i) rfl, Iso.symm_self_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
i : A
rw :
  Eq (α :=
    Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C i ⋙ shiftFunctor C i) (shiftFunctor C i ⋙ shiftFunctor C i))
    (Iso.symm (shiftFunctorAdd' C i i (i + i) ⋯) ≪≫ shiftFunctorAdd' C i i (i + i) ⋯)
    (Iso.refl (shiftFunctor C i ⋙ shiftFunctor C i))
⊢ Eq (α :=
    Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C i ⋙ shiftFunctor C i) (shiftFunctor C i ⋙ shiftFunctor C i))
    (shiftFunctorComm C i i) (Iso.refl (shiftFunctor C i ⋙ shiftFunctor C i))
have rw₁ : Eq (α :=
  Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C i ⋙ shiftFunctor C i) (shiftFunctor C i ⋙ shiftFunctor C i))
  (Iso.refl (shiftFunctor C i ⋙ shiftFunctor C i)) (Iso.refl (shiftFunctor C i ⋙ shiftFunctor C i))
Tactic: rw [shiftFunctorComm_eq C i i (i + i) rfl, Iso.symm_self_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
i j : A
⊢ Eq (α :=
    Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C j ⋙ shiftFunctor C i) (shiftFunctor C i ⋙ shiftFunctor C j))
    (Iso.symm (shiftFunctorComm C i j)) (shiftFunctorComm C j i)
have w : Eq (α :=
  Quiver.Hom (V := Functor.{v, v, u, u} C C) (shiftFunctor C j ⋙ shiftFunctor C i)
    (shiftFunctor C i ⋙ shiftFunctor C j))
  (Iso.hom (Iso.symm (shiftFunctorComm C i j))) (Iso.hom (shiftFunctorComm C j i))
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
i j : A
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v, v, u, u} C C) (shiftFunctor C j ⋙ shiftFunctor C i)
      (shiftFunctor C i ⋙ shiftFunctor C j))
    (Iso.inv (shiftFunctorComm C i j)) (Iso.hom (shiftFunctorComm C j i))
have w : Eq (α :=
  Quiver.Hom (V := Functor.{v, v, u, u} C C) (shiftFunctor C j ⋙ shiftFunctor C i)
    (shiftFunctor C i ⋙ shiftFunctor C j))
  (Iso.inv (Iso.symm (shiftFunctorAdd' C i j (i + j) sorry) ≪≫ shiftFunctorAdd' C j i (i + j) sorry))
  (Iso.hom (Iso.symm (shiftFunctorAdd' C j i (i + j) sorry) ≪≫ shiftFunctorAdd' C i j (i + j) sorry))
Tactic: rw [shiftFunctorComm_eq C i j (i + j) rfl, shiftFunctorComm_eq C j i (i + j) (add_comm j i)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
X : C
i j : A
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) X) ≅
      obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X))
    (Iso.symm (shiftComm X i j)) (shiftComm X j i)
have w : Eq.{v + 1} (α :=
  obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) X) ⟶
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X))
  (Iso.hom (Iso.symm (shiftComm X i j))) (Iso.hom (shiftComm X j i))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
i j : A
⊢ Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) Y))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f))
    (Iso.hom (shiftComm X i j) ≫ map (shiftFunctor C i) (map (shiftFunctor C j) f) ≫ Iso.hom (shiftComm Y j i))
have erw : Eq (α :=
  obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) Y))
  (map (shiftFunctor C j) (map (shiftFunctor C i) f))
  (map (shiftFunctor C i ⋙ shiftFunctor C j) f ≫
    NatTrans.app (Iso.hom (shiftFunctorComm C i j)) Y ≫ Iso.hom (Iso.symm (shiftComm Y i j)))
Tactic: erw [← shiftComm_symm Y i j, ← ((shiftFunctorComm C i j).hom.naturality_assoc f)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
i j : A
⊢ Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) Y))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f))
    (map (shiftFunctor C i ⋙ shiftFunctor C j) f ≫
      NatTrans.app (Iso.hom (shiftFunctorComm C i j)) Y ≫ Iso.hom (Iso.symm (shiftComm Y i j)))
have dsimp : Eq (α :=
  obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) Y))
  (map (shiftFunctor C j) (map (shiftFunctor C i) f))
  (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫
    NatTrans.app (Iso.hom (shiftFunctorComm C i j)) Y ≫ NatTrans.app (Iso.inv (shiftFunctorComm C i j)) Y)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
i j : A
⊢ Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) Y))
    (Iso.hom (shiftComm X i j) ≫ map (shiftFunctor C i) (map (shiftFunctor C j) f))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
have rw : Eq (α :=
  obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
    obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) Y))
  (Iso.hom (shiftComm X i j) ≫
    Iso.hom (shiftComm X j i) ≫ map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
  (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
Tactic: rw [shiftComm', ← shiftComm_symm, Iso.symm_hom, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
i j : A
rw :
  Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) Y))
    (Iso.hom (shiftComm X i j) ≫
      Iso.hom (shiftComm X j i) ≫ map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
⊢ Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) Y))
    (Iso.hom (shiftComm X i j) ≫ map (shiftFunctor C i) (map (shiftFunctor C j) f))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
have rw₁ : Eq (α :=
  obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
    obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) Y))
  (Iso.hom (Iso.symm (shiftComm X j i)) ≫
    Iso.hom (shiftComm X j i) ≫ map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
  (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
Tactic: rw [shiftComm', ← shiftComm_symm, Iso.symm_hom, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
i j : A
rw :
  Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) Y))
    (Iso.hom (shiftComm X i j) ≫
      Iso.hom (shiftComm X j i) ≫ map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
rw₁ :
  Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) Y))
    (Iso.hom (Iso.symm (shiftComm X j i)) ≫
      Iso.hom (shiftComm X j i) ≫ map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
⊢ Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) Y))
    (Iso.hom (shiftComm X i j) ≫ map (shiftFunctor C i) (map (shiftFunctor C j) f))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
have rw₂ : Eq (α :=
  obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
    obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) Y))
  (Iso.inv (shiftComm X j i) ≫
    Iso.hom (shiftComm X j i) ≫ map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
  (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
Tactic: rw [shiftComm', ← shiftComm_symm, Iso.symm_hom, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
i j : A
rw :
  Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) Y))
    (Iso.hom (shiftComm X i j) ≫
      Iso.hom (shiftComm X j i) ≫ map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
rw₁ :
  Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) Y))
    (Iso.hom (Iso.symm (shiftComm X j i)) ≫
      Iso.hom (shiftComm X j i) ≫ map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
rw₂ :
  Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) Y))
    (Iso.inv (shiftComm X j i) ≫
      Iso.hom (shiftComm X j i) ≫ map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
⊢ Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) Y))
    (Iso.hom (shiftComm X i j) ≫ map (shiftFunctor C i) (map (shiftFunctor C j) f))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
have rw₃ : Eq (α :=
  obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
    obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) Y))
  (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
  (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
Tactic: rw [shiftComm', ← shiftComm_symm, Iso.symm_hom, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
X : C
n : A
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) (obj.{v, v, u, u} (shiftFunctor C n) X) ⟶
      obj.{v, v, u, u} (𝟭 C) (obj.{v, v, u, u} (shiftFunctor C n) X))
    (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X))
    (NatTrans.app (Iso.hom (shiftFunctorComm C n 0)) X ≫
      map (shiftFunctor C n) (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X))
have rw : Eq.{v + 1} (α :=
  obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) (obj.{v, v, u, u} (shiftFunctor C n) X) ⟶
    obj.{v, v, u, u} (𝟭 C) (obj.{v, v, u, u} (shiftFunctor C n) X))
  (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X))
  (CategoryStruct.comp (Y := obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0 ⋙ shiftFunctor C n) X)
    (NatTrans.app (Iso.hom (Iso.symm (shiftFunctorAdd' C n 0 n sorry) ≪≫ shiftFunctorAdd' C 0 n n sorry)) X)
    (NatTrans.app (Iso.inv (shiftFunctorAdd' C 0 n n sorry)) X))
Tactic: rw [← shiftFunctorAdd'_zero_add_inv_app n X, shiftFunctorComm_eq C n 0 n (add_zero n)]