awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.DifferentialObject
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
D : Type u'
inst_4 : Category.{v', u'} D
inst_5 : HasZeroMorphisms.{v', u'} D
inst_6 : HasShift.{v', u', u_1} D S
F : Functor.{v, v', u, u'} C D
η : shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F ⟶ F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1
hF : ∀ (c c' : C), Eq (α := F.obj c ⟶ F.obj c') (F.map 0) 0
X Y : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
rw rw₁ : F.map f.f ≫ F.map Y.d ≫ η.app Y.obj = F.map f.f ≫ F.map Y.d ≫ η.app Y.obj
⊢ (F.map f.f ≫ F.map Y.d) ≫ η.app Y.obj = F.map f.f ≫ F.map Y.d ≫ η.app Y.obj

Tactic:
rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.DifferentialObject
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
D : Type u'
inst_4 : Category.{v', u'} D
inst_5 : HasZeroMorphisms.{v', u'} D
inst_6 : HasShift.{v', u', u_1} D S
F : Functor.{v, v', u, u'} C D
η : shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F ⟶ F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1
hF : ∀ (c c' : C), Eq (α := F.obj c ⟶ F.obj c') (F.map 0) 0
X : DifferentialObject.{v, u, u_1} S C
w :
  autoParam
    (DifferentialObject.Hom.f { f := F.map (DifferentialObject.Hom.f (𝟙 X)), comm := ⋯ } =
      DifferentialObject.Hom.f
        (𝟙 { obj := F.obj X.obj, d := F.map X.d ≫ η.app X.obj, d_squared := ⋯ : DifferentialObject.{v', u', u_1} S D }))
    DifferentialObject.ext._auto_1
⊢ { f := F.map (DifferentialObject.Hom.f (𝟙 X)), comm := ⋯ } =
    𝟙 { obj := F.obj X.obj, d := F.map X.d ≫ η.app X.obj, d_squared := ⋯ : DifferentialObject.{v', u', u_1} S D }

Tactic:
ext
-- Module: Mathlib.CategoryTheory.DifferentialObject
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
D : Type u'
inst_4 : Category.{v', u'} D
inst_5 : HasZeroMorphisms.{v', u'} D
inst_6 : HasShift.{v', u', u_1} D S
F : Functor.{v, v', u, u'} C D
η : shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F ⟶ F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1
hF : ∀ (c c' : C), Eq (α := F.obj c ⟶ F.obj c') (F.map 0) 0
X : DifferentialObject.{v, u, u_1} S C
⊢ autoParam
    (DifferentialObject.Hom.f { f := F.map (DifferentialObject.Hom.f (𝟙 X)), comm := ⋯ } =
      DifferentialObject.Hom.f
        (𝟙 { obj := F.obj X.obj, d := F.map X.d ≫ η.app X.obj, d_squared := ⋯ : DifferentialObject.{v', u', u_1} S D }))
    DifferentialObject.ext._auto_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.DifferentialObject
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
D : Type u'
inst_4 : Category.{v', u'} D
inst_5 : HasZeroMorphisms.{v', u'} D
inst_6 : HasShift.{v', u', u_1} D S
F : Functor.{v, v', u, u'} C D
η : shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F ⟶ F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1
hF : ∀ (c c' : C), Eq (α := F.obj c ⟶ F.obj c') (F.map 0) 0
X Y Z : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
g : Y ⟶ Z
w :
  autoParam
    (Eq.{v' + 1} (α :=
      { obj := F.obj X.obj, d := F.map X.d ≫ η.app X.obj, d_squared := ⋯ : DifferentialObject.{v', u', u_1} S D }.obj ⟶
        { obj := F.obj Z.obj, d := F.map Z.d ≫ η.app Z.obj, d_squared := ⋯ : DifferentialObject.{v', u', u_1} S D }.obj)
      (DifferentialObject.Hom.f { f := F.map (f ≫ g).f, comm := ⋯ })
      (DifferentialObject.Hom.f
        (CategoryStruct.comp (Y := { obj := F.obj Y.obj, d := F.map Y.d ≫ η.app Y.obj, d_squared := ⋯ })
          { f := F.map f.f, comm := ⋯ } { f := F.map g.f, comm := ⋯ })))
    DifferentialObject.ext._auto_1
⊢ Eq.{v' + 1} (α :=
    { obj := F.obj X.obj, d := F.map X.d ≫ η.app X.obj, d_squared := ⋯ : DifferentialObject.{v', u', u_1} S D } ⟶
      { obj := F.obj Z.obj, d := F.map Z.d ≫ η.app Z.obj, d_squared := ⋯ })
    { f := F.map (f ≫ g).f, comm := ⋯ }
    (CategoryStruct.comp (Y := { obj := F.obj Y.obj, d := F.map Y.d ≫ η.app Y.obj, d_squared := ⋯ })
      { f := F.map f.f, comm := ⋯ } { f := F.map g.f, comm := ⋯ })

Tactic:
ext
-- Module: Mathlib.CategoryTheory.DifferentialObject
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
D : Type u'
inst_4 : Category.{v', u'} D
inst_5 : HasZeroMorphisms.{v', u'} D
inst_6 : HasShift.{v', u', u_1} D S
F : Functor.{v, v', u, u'} C D
η : shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F ⟶ F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1
hF : ∀ (c c' : C), Eq (α := F.obj c ⟶ F.obj c') (F.map 0) 0
X Y Z : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
g : Y ⟶ Z
⊢ autoParam
    (Eq.{v' + 1} (α :=
      { obj := F.obj X.obj, d := F.map X.d ≫ η.app X.obj, d_squared := ⋯ : DifferentialObject.{v', u', u_1} S D }.obj ⟶
        { obj := F.obj Z.obj, d := F.map Z.d ≫ η.app Z.obj, d_squared := ⋯ : DifferentialObject.{v', u', u_1} S D }.obj)
      (DifferentialObject.Hom.f { f := F.map (f ≫ g).f, comm := ⋯ })
      (DifferentialObject.Hom.f
        (CategoryStruct.comp (Y := { obj := F.obj Y.obj, d := F.map Y.d ≫ η.app Y.obj, d_squared := ⋯ })
          { f := F.map f.f, comm := ⋯ } { f := F.map g.f, comm := ⋯ })))
    DifferentialObject.ext._auto_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.DifferentialObject
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasShift.{v, u, u_1} C S
inst_5 : Functor.PreservesZeroMorphisms.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := S) 1)
X : DifferentialObject.{v, u, u_1} S C
f : { obj := 0, d := 0, d_squared := ⋯ } ⟶ X
⊢ f = default

Tactic:
ext
-- Module: Mathlib.CategoryTheory.DifferentialObject
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasShift.{v, u, u_1} C S
inst_5 : Functor.PreservesZeroMorphisms.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := S) 1)
X : DifferentialObject.{v, u, u_1} S C
f : X ⟶ { obj := 0, d := 0, d_squared := ⋯ }
⊢ f = default

Tactic:
ext
-- Module: Mathlib.CategoryTheory.DifferentialObject
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type (u + 1)
inst_1 : LargeCategory C
inst_2 : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst_3 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_4 : ConcreteCategory C FC (CC := CC)
inst_5 : HasShift C S
X Y : DifferentialObject S C
f : X ⟶ Y
⊢ X.d ≫
      Functor.map (shiftFunctor.{u, u + 1, u_1} C (A := S) 1)
        (ConcreteCategory.ofHom (FC := FC) (CC := CC) (ConcreteCategory.hom (FC := FC) (CC := CC) f.f)) =
    ConcreteCategory.ofHom (FC := FC) (CC := CC) (ConcreteCategory.hom (FC := FC) (CC := CC) f.f) ≫ Y.d

Tactic:
simp [ConcreteCategory.ofHom_hom]

Premises used: CategoryTheory.ConcreteCategory.ofHom_hom
-- Module: Mathlib.CategoryTheory.DifferentialObject
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type (u + 1)
inst_1 : LargeCategory C
inst_2 : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst_3 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_4 : ConcreteCategory C FC (CC := CC)
inst_5 : HasShift C S
X Y : DifferentialObject S C
f : HomSubtype S C (FC := FC) (CC := CC) X Y
⊢ X.d ≫
      Functor.map (shiftFunctor.{u, u + 1, u_1} C (A := S) 1)
        (ConcreteCategory.ofHom (FC := FC) (CC := CC) (↑f : FC X.obj Y.obj)) =
    ConcreteCategory.ofHom (FC := FC) (CC := CC) (↑f : FC X.obj Y.obj) ≫ Y.d

Tactic:
simpa [ConcreteCategory.hom_ofHom] using f.2

Premises used: CategoryTheory.ConcreteCategory.hom_ofHom, Subtype.property
-- Module: Mathlib.CategoryTheory.DifferentialObject
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type (u + 1)
inst_1 : LargeCategory C
inst_2 : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst_3 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_4 : ConcreteCategory C FC (CC := CC)
inst_5 : HasShift C S
X Y : DifferentialObject S C
x : HomSubtype S C (FC := FC) (CC := CC) X Y
dsimp :
  Subtype.mk (p := fun (f : FC X.obj Y.obj) ↦
      X.d ≫ Functor.map (shiftFunctor.{u, u + 1, u_1} C (A := S) 1) (ConcreteCategory.ofHom (FC := FC) (CC := CC) f) =
        ConcreteCategory.ofHom (FC := FC) (CC := CC) f ≫ Y.d)
      (@ConcreteCategory.hom _ inst_1 FC CC _ _ _ _
        (ConcreteCategory.ofHom (FC := FC) (CC := CC) (↑x : FC X.obj Y.obj)))
      ⋯ =
    x
⊢ Subtype.mk (p := fun (f : FC X.obj Y.obj) ↦
      X.d ≫ Functor.map (shiftFunctor.{u, u + 1, u_1} C (A := S) 1) (ConcreteCategory.ofHom (FC := FC) (CC := CC) f) =
        ConcreteCategory.ofHom (FC := FC) (CC := CC) f ≫ Y.d)
      (ConcreteCategory.hom (FC := FC) (CC := CC)
        { f := ConcreteCategory.ofHom (FC := FC) (CC := CC) (↑x : FC X.obj Y.obj), comm := ⋯ : X.Hom Y }.f)
      ⋯ =
    x

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.DifferentialObject
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type (u + 1)
inst_1 : LargeCategory C
inst_2 : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst_3 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_4 : ConcreteCategory C FC (CC := CC)
inst_5 : HasShift C S
X Y : DifferentialObject S C
x : HomSubtype S C (FC := FC) (CC := CC) X Y
a :
  (↑(Subtype.mk (p := fun (f : FC X.obj Y.obj) ↦
          X.d ≫
              Functor.map (shiftFunctor.{u, u + 1, u_1} C (A := S) 1) (ConcreteCategory.ofHom (FC := FC) (CC := CC) f) =
            ConcreteCategory.ofHom (FC := FC) (CC := CC) f ≫ Y.d)
          (@ConcreteCategory.hom _ inst_1 FC CC _ _ _ _
            (ConcreteCategory.ofHom (FC := FC) (CC := CC) (↑x : FC X.obj Y.obj)))
          ⋯) :
      FC X.obj Y.obj) =
    (↑x : FC X.obj Y.obj)
⊢ Subtype.mk (p := fun (f : FC X.obj Y.obj) ↦
      X.d ≫ Functor.map (shiftFunctor.{u, u + 1, u_1} C (A := S) 1) (ConcreteCategory.ofHom (FC := FC) (CC := CC) f) =
        ConcreteCategory.ofHom (FC := FC) (CC := CC) f ≫ Y.d)
      (@ConcreteCategory.hom _ inst_1 FC CC _ _ _ _
        (ConcreteCategory.ofHom (FC := FC) (CC := CC) (↑x : FC X.obj Y.obj)))
      ⋯ =
    x

Tactic:
ext
-- Module: Mathlib.CategoryTheory.DifferentialObject
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type (u + 1)
inst_1 : LargeCategory C
inst_2 : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst_3 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_4 : ConcreteCategory C FC (CC := CC)
inst_5 : HasShift C S
X Y : DifferentialObject S C
x : HomSubtype S C (FC := FC) (CC := CC) X Y
⊢ (↑(Subtype.mk (p := fun (f : FC X.obj Y.obj) ↦
          X.d ≫
              Functor.map (shiftFunctor.{u, u + 1, u_1} C (A := S) 1) (ConcreteCategory.ofHom (FC := FC) (CC := CC) f) =
            ConcreteCategory.ofHom (FC := FC) (CC := CC) f ≫ Y.d)
          (@ConcreteCategory.hom _ inst_1 FC CC _ _ _ _
            (ConcreteCategory.ofHom (FC := FC) (CC := CC) (↑x : FC X.obj Y.obj)))
          ⋯) :
      FC X.obj Y.obj) =
    (↑x : FC X.obj Y.obj)

Tactic:
simp [ConcreteCategory.hom_ofHom]

Premises used: CategoryTheory.ConcreteCategory.hom_ofHom
-- Module: Mathlib.CategoryTheory.DifferentialObject
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type (u + 1)
inst_1 : LargeCategory C
inst_2 : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst_3 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_4 : ConcreteCategory C FC (CC := CC)
inst_5 : HasShift C S
X Y : DifferentialObject S C
x : X ⟶ Y
w :
  ConcreteCategory.hom (FC := FC) (CC := CC)
      {
          f :=
            ConcreteCategory.ofHom (FC := FC) (CC := CC)
              (↑(Subtype.mk (p := fun (f : FC X.obj Y.obj) ↦
                    X.d ≫
                        Functor.map (shiftFunctor.{u, u + 1, u_1} C (A := S) 1)
                          (ConcreteCategory.ofHom (FC := FC) (CC := CC) f) =
                      ConcreteCategory.ofHom (FC := FC) (CC := CC) f ≫ Y.d)
                    (ConcreteCategory.hom (FC := FC) (CC := CC) x.f) ⋯) :
                FC X.obj Y.obj),
          comm := ⋯ : X.Hom Y }.f =
    ConcreteCategory.hom (FC := FC) (CC := CC) x.f
⊢ {
      f :=
        ConcreteCategory.ofHom (FC := FC) (CC := CC)
          (↑(Subtype.mk (p := fun (f : FC X.obj Y.obj) ↦
                X.d ≫
                    Functor.map (shiftFunctor.{u, u + 1, u_1} C (A := S) 1)
                      (ConcreteCategory.ofHom (FC := FC) (CC := CC) f) =
                  ConcreteCategory.ofHom (FC := FC) (CC := CC) f ≫ Y.d)
                (ConcreteCategory.hom (FC := FC) (CC := CC) x.f) ⋯) :
            FC X.obj Y.obj),
      comm := ⋯ : X.Hom Y } =
    x

Tactic:
ext
-- Module: Mathlib.CategoryTheory.DifferentialObject
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type (u + 1)
inst_1 : LargeCategory C
inst_2 : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst_3 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_4 : ConcreteCategory C FC (CC := CC)
inst_5 : HasShift C S
X Y : DifferentialObject S C
x : X ⟶ Y
⊢ ConcreteCategory.hom (FC := FC) (CC := CC)
      {
          f :=
            ConcreteCategory.ofHom (FC := FC) (CC := CC)
              (↑(Subtype.mk (p := fun (f : FC X.obj Y.obj) ↦
                    X.d ≫
                        Functor.map (shiftFunctor.{u, u + 1, u_1} C (A := S) 1)
                          (ConcreteCategory.ofHom (FC := FC) (CC := CC) f) =
                      ConcreteCategory.ofHom (FC := FC) (CC := CC) f ≫ Y.d)
                    (ConcreteCategory.hom (FC := FC) (CC := CC) x.f) ⋯) :
                FC X.obj Y.obj),
          comm := ⋯ : X.Hom Y }.f =
    ConcreteCategory.hom (FC := FC) (CC := CC) x.f

Tactic:
simp [ConcreteCategory.ofHom_hom]

Premises used: CategoryTheory.ConcreteCategory.ofHom_hom
-- Module: Mathlib.CategoryTheory.DifferentialObject
Goal:
S : Type u_1
inst : AddCommGroupWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
n : S
X Y : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
dsimp :
  Eq (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj))
    ((Functor.map (CategoryTheory.shiftFunctor C n) X.d ≫
          NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 n)) X.obj) ≫
        Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (Functor.map (CategoryTheory.shiftFunctor C n) f.f) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj))
    (Functor.map (CategoryTheory.shiftFunctor C n) f.f ≫
        Functor.map (CategoryTheory.shiftFunctor C n) Y.d ≫
          NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 n)) Y.obj :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj))
⊢ { obj := Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj,
          d := Functor.map (CategoryTheory.shiftFunctor C n) X.d ≫ Iso.hom (shiftComm.{v, u, u_1} X.obj 1 n),
          d_squared := ⋯ : DifferentialObject.{v, u, u_1} S C }.d ≫
      Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
        (Functor.map (CategoryTheory.shiftFunctor C n) f.f) =
    Functor.map (CategoryTheory.shiftFunctor C n) f.f ≫
      { obj := Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj,
          d := Functor.map (CategoryTheory.shiftFunctor C n) Y.d ≫ Iso.hom (shiftComm.{v, u, u_1} Y.obj 1 n),
          d_squared := ⋯ : DifferentialObject.{v, u, u_1} S C }.d

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.DifferentialObject
Goal:
S : Type u_1
inst : AddCommGroupWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
n : S
X Y : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
rw :
  Eq (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj))
    (Functor.map (CategoryTheory.shiftFunctor C n) X.d ≫
        NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 n)) X.obj ≫
          Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
            (Functor.map (CategoryTheory.shiftFunctor C n) f.f) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj))
    (Functor.map (CategoryTheory.shiftFunctor C n) f.f ≫
        Functor.map (CategoryTheory.shiftFunctor C n) Y.d ≫
          NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 n)) Y.obj :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj))
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj))
    ((Functor.map (CategoryTheory.shiftFunctor C n) X.d ≫
          NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 n)) X.obj) ≫
        Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (Functor.map (CategoryTheory.shiftFunctor C n) f.f) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj))
    (Functor.map (CategoryTheory.shiftFunctor C n) f.f ≫
        Functor.map (CategoryTheory.shiftFunctor C n) Y.d ≫
          NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 n)) Y.obj :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj))

Tactic:
rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.DifferentialObject
Goal:
S : Type u_1
inst : AddCommGroupWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
n : S
X Y : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
erw :
  Eq (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj))
    (Functor.map (CategoryTheory.shiftFunctor C n) X.d ≫
        Functor.map (CategoryTheory.shiftFunctor C n)
            (Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1) f.f) ≫
          Iso.hom (shiftComm.{v, u, u_1} Y.obj 1 n) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj))
    (Functor.map (CategoryTheory.shiftFunctor C n) f.f ≫
        Functor.map (CategoryTheory.shiftFunctor C n) Y.d ≫
          NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 n)) Y.obj :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj))
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj))
    (Functor.map (CategoryTheory.shiftFunctor C n) X.d ≫
        NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 n)) X.obj ≫
          Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
            (Functor.map (CategoryTheory.shiftFunctor C n) f.f) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj))
    (Functor.map (CategoryTheory.shiftFunctor C n) f.f ≫
        Functor.map (CategoryTheory.shiftFunctor C n) Y.d ≫
          NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 n)) Y.obj :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj))

Tactic:
erw [shiftComm_hom_comp]

Premises used: CategoryTheory.shiftComm_hom_comp
-- Module: Mathlib.CategoryTheory.DifferentialObject
Goal:
S : Type u_1
inst : AddCommGroupWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
n : S
X Y : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
rw :
  Eq (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj))
    (Functor.map (CategoryTheory.shiftFunctor C n) f.f ≫
        Functor.map (CategoryTheory.shiftFunctor C n) Y.d ≫ Iso.hom (shiftComm.{v, u, u_1} Y.obj 1 n) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj))
    (Functor.map (CategoryTheory.shiftFunctor C n) f.f ≫
        Functor.map (CategoryTheory.shiftFunctor C n) Y.d ≫
          NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 n)) Y.obj :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj))
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj))
    (Functor.map (CategoryTheory.shiftFunctor C n) X.d ≫
        Functor.map (CategoryTheory.shiftFunctor C n)
            (Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1) f.f) ≫
          Iso.hom (shiftComm.{v, u, u_1} Y.obj 1 n) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj))
    (Functor.map (CategoryTheory.shiftFunctor C n) f.f ≫
        Functor.map (CategoryTheory.shiftFunctor C n) Y.d ≫
          NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 n)) Y.obj :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj))

Tactic:
rw [← Functor.map_comp_assoc, f.comm, Functor.map_comp_assoc]

Premises used: CategoryTheory.Functor.map_comp_assoc, CategoryTheory.DifferentialObject.Hom.comm