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 : 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))
    (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 ⋯) ≪≫ shiftFunctorAdd' C 0 n n ⋯)) X)
      (NatTrans.app (Iso.inv (shiftFunctorAdd' C 0 n n ⋯)) X))
have dsimp : 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} (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 C n) (obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X))
    (NatTrans.app (Iso.inv (shiftFunctorAdd' C n 0 n sorry)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C 0 n n sorry)) X)
    (NatTrans.app (Iso.inv (shiftFunctorAdd' C 0 n n sorry)) X))
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 : 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} (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 C n) (obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X))
      (NatTrans.app (Iso.inv (shiftFunctorAdd' C n 0 n ⋯)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C 0 n n ⋯)) X)
      (NatTrans.app (Iso.inv (shiftFunctorAdd' C 0 n n ⋯)) 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} (shiftFunctor C n) X)
  (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X))
  (NatTrans.app (Iso.inv (shiftFunctorAdd' C n 0 n sorry)) X ≫
    CategoryStruct.comp (Y :=
      obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X))
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C 0 n n sorry)) X) (NatTrans.app (Iso.inv (shiftFunctorAdd' C 0 n n sorry)) X))
Tactic: rw [Category.assoc, Iso.hom_inv_id_app, Category.comp_id, shiftFunctorAdd'_add_zero_inv_app]
-- 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
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} (shiftFunctor C n) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X))
    (NatTrans.app (Iso.inv (shiftFunctorAdd' C n 0 n ⋯)) X ≫
      CategoryStruct.comp (Y :=
        obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X))
        (NatTrans.app (Iso.hom (shiftFunctorAdd' C 0 n n ⋯)) X) (NatTrans.app (Iso.inv (shiftFunctorAdd' C 0 n n ⋯)) X))
⊢ 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} (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 C n) (obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X))
      (NatTrans.app (Iso.inv (shiftFunctorAdd' C n 0 n ⋯)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C 0 n n ⋯)) X)
      (NatTrans.app (Iso.inv (shiftFunctorAdd' C 0 n n ⋯)) X))
have rw₁ : NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X) =
  NatTrans.app (Iso.inv (shiftFunctorAdd' C n 0 n sorry)) X ≫ 𝟙 (obj.{v, v, u, u} (shiftFunctor C n) X)
Tactic: rw [Category.assoc, Iso.hom_inv_id_app, Category.comp_id, shiftFunctorAdd'_add_zero_inv_app]
-- 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
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} (shiftFunctor C n) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X))
    (NatTrans.app (Iso.inv (shiftFunctorAdd' C n 0 n ⋯)) X ≫
      CategoryStruct.comp (Y :=
        obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X))
        (NatTrans.app (Iso.hom (shiftFunctorAdd' C 0 n n ⋯)) X) (NatTrans.app (Iso.inv (shiftFunctorAdd' C 0 n n ⋯)) X))
rw₁ :
  NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X) =
    NatTrans.app (Iso.inv (shiftFunctorAdd' C n 0 n ⋯)) X ≫ 𝟙 (obj.{v, v, u, u} (shiftFunctor C n) X)
⊢ 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} (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 C n) (obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X))
      (NatTrans.app (Iso.inv (shiftFunctorAdd' C n 0 n ⋯)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C 0 n n ⋯)) X)
      (NatTrans.app (Iso.inv (shiftFunctorAdd' C 0 n n ⋯)) 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} (shiftFunctor C n) X)
  (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X))
  (NatTrans.app (Iso.inv (shiftFunctorAdd' C n 0 n sorry)) X)
Tactic: rw [Category.assoc, Iso.hom_inv_id_app, Category.comp_id, shiftFunctorAdd'_add_zero_inv_app]
-- 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
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} (shiftFunctor C n) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X))
    (NatTrans.app (Iso.inv (shiftFunctorAdd' C n 0 n ⋯)) X ≫
      CategoryStruct.comp (Y :=
        obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X))
        (NatTrans.app (Iso.hom (shiftFunctorAdd' C 0 n n ⋯)) X) (NatTrans.app (Iso.inv (shiftFunctorAdd' C 0 n n ⋯)) X))
rw₁ :
  NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X) =
    NatTrans.app (Iso.inv (shiftFunctorAdd' C n 0 n ⋯)) X ≫ 𝟙 (obj.{v, v, u, u} (shiftFunctor C n) X)
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} (shiftFunctor C n) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X))
    (NatTrans.app (Iso.inv (shiftFunctorAdd' C n 0 n ⋯)) X)
⊢ 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} (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 C n) (obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X))
      (NatTrans.app (Iso.inv (shiftFunctorAdd' C n 0 n ⋯)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C 0 n n ⋯)) X)
      (NatTrans.app (Iso.inv (shiftFunctorAdd' C 0 n n ⋯)) 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} (shiftFunctor C n) X)
  (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (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))
Tactic: rw [Category.assoc, Iso.hom_inv_id_app, Category.comp_id, shiftFunctorAdd'_add_zero_inv_app]
-- 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} (𝟭 C) (obj.{v, v, u, u} (shiftFunctor C n) X) ⟶
      obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) (obj.{v, v, u, u} (shiftFunctor C n) X))
    (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X))
    (map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X) ≫
      NatTrans.app (Iso.inv (shiftFunctorComm C n 0)) X)
have rw : 𝟙 (obj.{v, v, u, u} (𝟭 C) (obj.{v, v, u, u} (shiftFunctor C n) X)) =
  map (shiftFunctor C n) (𝟙 (obj.{v, v, u, u} (𝟭 C) X))
Tactic: rw [← cancel_mono ((shiftFunctorZero C A).hom.app (X⟦n⟧)), Category.assoc, Iso.inv_hom_id_app,
    shiftFunctorZero_hom_app_shift, Iso.inv_hom_id_app_assoc, ← Functor.map_comp,
    Iso.inv_hom_id_app]
-- 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
⊢ 𝟙 (obj.{v, v, u, u} (𝟭 C) (obj.{v, v, u, u} (shiftFunctor C n) X)) =
    map (shiftFunctor C n) (𝟙 (obj.{v, v, u, u} (𝟭 C) X))
have dsimp : 𝟙 (obj.{v, v, u, u} (shiftFunctor C n) X) = map (shiftFunctor C n) (𝟙 X)
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 : C
n : A
⊢ 𝟙 (obj.{v, v, u, u} (shiftFunctor C n) X) = map (shiftFunctor C n) (𝟙 X)
have rw : Eq.{v + 1} (α := obj.{v, v, u, u} (shiftFunctor C n) X ⟶ obj.{v, v, u, u} (shiftFunctor C n) X)
  (𝟙 (obj.{v, v, u, u} (shiftFunctor C n) X)) (𝟙 (obj.{v, v, u, u} (shiftFunctor C n) X))
Tactic: rw [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
m₁ m₂ m₃ : A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C m₁ ⋙ shiftFunctor C (m₂ + m₃)) X ⟶
      obj.{v, v, u, u} (shiftFunctor C m₁) (obj.{v, v, u, u} (shiftFunctor C m₂ ⋙ shiftFunctor C m₃) X))
    (NatTrans.app (Iso.hom (shiftFunctorComm C m₁ (m₂ + m₃))) X ≫
      map (shiftFunctor C m₁) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ≫
      map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorComm C m₁ m₂)) X) ≫
        NatTrans.app (Iso.hom (shiftFunctorComm C m₁ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₂) X))
have rw : Eq.{v + 1} (α :=
  obj.{v, v, u, u} (shiftFunctor C m₁ ⋙ shiftFunctor C (m₂ + m₃)) X ⟶
    obj.{v, v, u, u} (shiftFunctor C m₃) (obj.{v, v, u, u} (shiftFunctor C m₁ ⋙ shiftFunctor C m₂) X))
  (((NatTrans.app (Iso.hom (shiftFunctorComm C m₁ (m₂ + m₃))) X ≫
        map (shiftFunctor C m₁) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₂) X)) ≫
    map (shiftFunctor C m₃) (NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₂)) X))
  (CategoryStruct.comp (Y :=
    obj.{v, v, u, u} (shiftFunctor C m₃) (obj.{v, v, u, u} (shiftFunctor C m₂ ⋙ shiftFunctor C m₁) X))
    ((NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ≫
        map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorComm C m₁ m₂)) X) ≫
          NatTrans.app (Iso.hom (shiftFunctorComm C m₁ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₂) X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₂) X))
    (map (shiftFunctor C m₃) (NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₂)) X)))
Tactic: rw [← cancel_mono ((shiftFunctorComm C m₁ m₃).inv.app (X⟦m₂⟧)),
    ← cancel_mono (((shiftFunctorComm C m₁ m₂).inv.app X)⟦m₃⟧')]
-- 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
m₁ m₂ m₃ : A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C m₁ ⋙ shiftFunctor C (m₂ + m₃)) X ⟶
      obj.{v, v, u, u} (shiftFunctor C m₃) (obj.{v, v, u, u} (shiftFunctor C m₁ ⋙ shiftFunctor C m₂) X))
    (((NatTrans.app (Iso.hom (shiftFunctorComm C m₁ (m₂ + m₃))) X ≫
          map (shiftFunctor C m₁) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₂) X)) ≫
      map (shiftFunctor C m₃) (NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₂)) X))
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u} (shiftFunctor C m₃) (obj.{v, v, u, u} (shiftFunctor C m₂ ⋙ shiftFunctor C m₁) X))
      ((NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ≫
          map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorComm C m₁ m₂)) X) ≫
            NatTrans.app (Iso.hom (shiftFunctorComm C m₁ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₂) X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₂) X))
      (map (shiftFunctor C m₃) (NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₂)) X)))
have simp : NatTrans.app (Iso.hom (shiftFunctorComm C m₁ (m₂ + m₃))) X ≫
    map (shiftFunctor C m₁) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) X) ≫
      NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₂) X) ≫
        map (shiftFunctor C m₃) (NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₂)) X) =
  NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ≫
    map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorComm C m₁ m₂)) X) ≫
      𝟙 (obj.{v, v, u, u} (shiftFunctor C m₁ ⋙ shiftFunctor C m₃) (obj.{v, v, u, u} (shiftFunctor C m₂) X)) ≫
        map (shiftFunctor C m₃) (NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₂)) X)
Tactic: simp only [Category.assoc, Iso.hom_inv_id_app]
-- 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
m₁ m₂ m₃ : A
X : C
⊢ NatTrans.app (Iso.hom (shiftFunctorComm C m₁ (m₂ + m₃))) X ≫
      map (shiftFunctor C m₁) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₂) X) ≫
          map (shiftFunctor C m₃) (NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₂)) X) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ≫
      map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorComm C m₁ m₂)) X) ≫
        𝟙 (obj.{v, v, u, u} (shiftFunctor C m₁ ⋙ shiftFunctor C m₃) (obj.{v, v, u, u} (shiftFunctor C m₂) X)) ≫
          map (shiftFunctor C m₃) (NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₂)) X)
have dsimp : NatTrans.app (Iso.hom (shiftFunctorComm C m₁ (m₂ + m₃))) X ≫
    map (shiftFunctor C m₁) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) X) ≫
      NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₂) X) ≫
        map (shiftFunctor C m₃) (NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₂)) X) =
  NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ≫
    map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorComm C m₁ m₂)) X) ≫
      𝟙
          (obj.{v, v, u, u} (shiftFunctor C m₃)
            (obj.{v, v, u, u} (shiftFunctor C m₁) (obj.{v, v, u, u} (shiftFunctor C m₂) X))) ≫
        map (shiftFunctor C m₃) (NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₂)) X)
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
m₁ m₂ m₃ : A
X : C
⊢ NatTrans.app (Iso.hom (shiftFunctorComm C m₁ (m₂ + m₃))) X ≫
      map (shiftFunctor C m₁) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₂) X) ≫
          map (shiftFunctor C m₃) (NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₂)) X) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ≫
      map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorComm C m₁ m₂)) X) ≫
        𝟙
            (obj.{v, v, u, u} (shiftFunctor C m₃)
              (obj.{v, v, u, u} (shiftFunctor C m₁) (obj.{v, v, u, u} (shiftFunctor C m₂) X))) ≫
          map (shiftFunctor C m₃) (NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₂)) X)
have simp : Eq.{v + 1} (α :=
  obj.{v, v, u, u} (shiftFunctor C (m₂ + m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ⟶
    obj.{v, v, u, u} (shiftFunctor C m₃)
      (obj.{v, v, u, u} (shiftFunctor C m₂) (obj.{v, v, u, u} (shiftFunctor C m₁) X)))
  (NatTrans.app (Iso.hom (shiftFunctorComm C m₁ (m₂ + m₃))) X ≫
    map (shiftFunctor C m₁) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) X) ≫
      NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₂) X) ≫
        map (shiftFunctor C m₃) (NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₂)) X))
  (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ≫
    map (shiftFunctor C m₃) (𝟙 (obj.{v, v, u, u} (shiftFunctor C m₁ ⋙ shiftFunctor C m₂) X)))
Tactic: simp only [Category.id_comp, ← Functor.map_comp, Iso.hom_inv_id_app]
-- 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
m₁ m₂ m₃ : A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C (m₂ + m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C m₃)
        (obj.{v, v, u, u} (shiftFunctor C m₂) (obj.{v, v, u, u} (shiftFunctor C m₁) X)))
    (NatTrans.app (Iso.hom (shiftFunctorComm C m₁ (m₂ + m₃))) X ≫
      map (shiftFunctor C m₁) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₂) X) ≫
          map (shiftFunctor C m₃) (NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₂)) X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ≫
      map (shiftFunctor C m₃) (𝟙 (obj.{v, v, u, u} (shiftFunctor C m₁ ⋙ shiftFunctor C m₂) X)))
have dsimp : Eq.{v + 1} (α :=
  obj.{v, v, u, u} (shiftFunctor C (m₂ + m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ⟶
    obj.{v, v, u, u} (shiftFunctor C m₃)
      (obj.{v, v, u, u} (shiftFunctor C m₂) (obj.{v, v, u, u} (shiftFunctor C m₁) X)))
  (NatTrans.app (Iso.hom (shiftFunctorComm C m₁ (m₂ + m₃))) X ≫
    map (shiftFunctor C m₁) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) X) ≫
      NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₂) X) ≫
        map (shiftFunctor C m₃) (NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₂)) X))
  (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ≫
    map (shiftFunctor C m₃) (𝟙 (obj.{v, v, u, u} (shiftFunctor C m₂) (obj.{v, v, u, u} (shiftFunctor C m₁) X))))
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
m₁ m₂ m₃ : A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C (m₂ + m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C m₃)
        (obj.{v, v, u, u} (shiftFunctor C m₂) (obj.{v, v, u, u} (shiftFunctor C m₁) X)))
    (NatTrans.app (Iso.hom (shiftFunctorComm C m₁ (m₂ + m₃))) X ≫
      map (shiftFunctor C m₁) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₂) X) ≫
          map (shiftFunctor C m₃) (NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₂)) X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ≫
      map (shiftFunctor C m₃) (𝟙 (obj.{v, v, u, u} (shiftFunctor C m₂) (obj.{v, v, u, u} (shiftFunctor C m₁) X))))
have simp : Eq.{v + 1} (α :=
  obj.{v, v, u, u} (shiftFunctor C (m₂ + m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ⟶
    obj.{v, v, u, u} (shiftFunctor C m₃)
      (obj.{v, v, u, u} (shiftFunctor C m₂) (obj.{v, v, u, u} (shiftFunctor C m₁) X)))
  (NatTrans.app
      (Iso.hom
        (Iso.symm (shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + (m₂ + m₃)) sorry) ≪≫
          shiftFunctorAdd' C (m₂ + m₃) m₁ (m₁ + (m₂ + m₃)) sorry))
      X ≫
    map (shiftFunctor C m₁) (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₂ m₃ (m₂ + m₃) sorry)) X) ≫
      NatTrans.app (Iso.inv (Iso.symm (shiftFunctorAdd' C m₁ m₃ (m₁ + m₃) sorry) ≪≫ shiftFunctorAdd' C m₃ m₁ (m₁ + m₃) sorry))
          (obj.{v, v, u, u} (shiftFunctor C m₂) X) ≫
        map (shiftFunctor C m₃)
          (NatTrans.app
            (Iso.inv (Iso.symm (shiftFunctorAdd' C m₁ m₂ (m₁ + m₂) sorry) ≪≫ shiftFunctorAdd' C m₂ m₁ (m₁ + m₂) sorry)) X))
  (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₂ m₃ (m₂ + m₃) sorry)) (obj.{v, v, u, u} (shiftFunctor C m₁) X))
Tactic: simp only [Functor.map_id, Category.comp_id,
    shiftFunctorComm_eq C _ _ _ rfl, ← shiftFunctorAdd'_eq_shiftFunctorAdd]