awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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))

Tactic:
rfl
-- 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 : DifferentialObject.{v, u, u_1} S C
w :
  autoParam
    (Hom.f { f := Functor.map (CategoryTheory.shiftFunctor C n) (Hom.f (𝟙 X)), comm := ⋯ } =
      Hom.f
        (𝟙
          { 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 }))
    ext._auto_1
⊢ { f := Functor.map (CategoryTheory.shiftFunctor C n) (Hom.f (𝟙 X)), comm := ⋯ } =
    𝟙
      { 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 }

Tactic:
ext1
-- 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 : DifferentialObject.{v, u, u_1} S C
w :
  autoParam
    (Functor.map (CategoryTheory.shiftFunctor C n) (𝟙 X.obj) =
      𝟙 (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj))
    ext._auto_1
⊢ autoParam
    (Hom.f { f := Functor.map (CategoryTheory.shiftFunctor C n) (Hom.f (𝟙 X)), comm := ⋯ } =
      Hom.f
        (𝟙
          { 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 }))
    ext._auto_1

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 : DifferentialObject.{v, u, u_1} S C
w w₁ :
  autoParam
    (Eq.{v + 1} (α :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj)
      (𝟙 (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj))
      (𝟙 (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj)))
    ext._auto_1
⊢ autoParam
    (Functor.map (CategoryTheory.shiftFunctor C n) (𝟙 X.obj) =
      𝟙 (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj))
    ext._auto_1

Tactic:
rw [Functor.map_id]

Premises used: CategoryTheory.Functor.map_id
-- 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 Z : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
g : Y ⟶ Z
w :
  autoParam
    (Eq.{v + 1} (α :=
      { 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 }.obj ⟶
        { obj := Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Z.obj,
            d := Functor.map (CategoryTheory.shiftFunctor C n) Z.d ≫ Iso.hom (shiftComm.{v, u, u_1} Z.obj 1 n),
            d_squared := ⋯ : DifferentialObject.{v, u, u_1} S C }.obj)
      (Hom.f { f := Functor.map (CategoryTheory.shiftFunctor C n) (f ≫ g).f, comm := ⋯ })
      (Hom.f
        (CategoryStruct.comp (Y :=
          { 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 := ⋯ })
          { f := Functor.map (CategoryTheory.shiftFunctor C n) f.f, comm := ⋯ }
          { f := Functor.map (CategoryTheory.shiftFunctor C n) g.f, comm := ⋯ })))
    ext._auto_1
⊢ Eq.{v + 1} (α :=
    { 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 } ⟶
      { obj := Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Z.obj,
        d := Functor.map (CategoryTheory.shiftFunctor C n) Z.d ≫ Iso.hom (shiftComm.{v, u, u_1} Z.obj 1 n),
        d_squared := ⋯ })
    { f := Functor.map (CategoryTheory.shiftFunctor C n) (f ≫ g).f, comm := ⋯ }
    (CategoryStruct.comp (Y :=
      { 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 := ⋯ })
      { f := Functor.map (CategoryTheory.shiftFunctor C n) f.f, comm := ⋯ }
      { f := Functor.map (CategoryTheory.shiftFunctor C n) g.f, comm := ⋯ })

Tactic:
ext1
-- 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 Z : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
g : Y ⟶ Z
w :
  autoParam
    (Eq (α :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Z.obj)
      (Functor.map (CategoryTheory.shiftFunctor C n) (f.f ≫ g.f))
      (Functor.map (CategoryTheory.shiftFunctor C n) f.f ≫ Functor.map (CategoryTheory.shiftFunctor C n) g.f))
    ext._auto_1
⊢ autoParam
    (Eq.{v + 1} (α :=
      { 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 }.obj ⟶
        { obj := Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Z.obj,
            d := Functor.map (CategoryTheory.shiftFunctor C n) Z.d ≫ Iso.hom (shiftComm.{v, u, u_1} Z.obj 1 n),
            d_squared := ⋯ : DifferentialObject.{v, u, u_1} S C }.obj)
      (Hom.f { f := Functor.map (CategoryTheory.shiftFunctor C n) (f ≫ g).f, comm := ⋯ })
      (Hom.f
        (CategoryStruct.comp (Y :=
          { 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 := ⋯ })
          { f := Functor.map (CategoryTheory.shiftFunctor C n) f.f, comm := ⋯ }
          { f := Functor.map (CategoryTheory.shiftFunctor C n) g.f, comm := ⋯ })))
    ext._auto_1

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 Z : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
g : Y ⟶ Z
w w₁ :
  autoParam
    (Eq (α :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Z.obj)
      (Functor.map (CategoryTheory.shiftFunctor C n) f.f ≫ Functor.map (CategoryTheory.shiftFunctor C n) g.f)
      (Functor.map (CategoryTheory.shiftFunctor C n) f.f ≫ Functor.map (CategoryTheory.shiftFunctor C n) g.f))
    ext._auto_1
⊢ autoParam
    (Eq (α :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Z.obj)
      (Functor.map (CategoryTheory.shiftFunctor C n) (f.f ≫ g.f))
      (Functor.map (CategoryTheory.shiftFunctor C n) f.f ≫ Functor.map (CategoryTheory.shiftFunctor C n) g.f))
    ext._auto_1

Tactic:
rw [Functor.map_comp]

Premises used: CategoryTheory.Functor.map_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
m n : S
refine_1 :
  ∀ (X : DifferentialObject.{v, u, u_1} S C),
    (Functor.obj (shiftFunctor C (m + n)) X).d ≫
        Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1) (Iso.hom (shiftAdd X.obj m n)) =
      Iso.hom (shiftAdd X.obj m n) ≫ (Functor.obj (shiftFunctor C m ⋙ shiftFunctor C n) X).d
refine_2 :
  ∀ {X Y : DifferentialObject.{v, u, u_1} S C} (f : X ⟶ Y),
    Eq (α := Functor.obj (shiftFunctor C (m + n)) X ⟶ Functor.obj (shiftFunctor C m ⋙ shiftFunctor C n) Y)
      (Functor.map (shiftFunctor C (m + n)) f ≫
        Iso.hom
          ((fun (X : DifferentialObject.{v, u, u_1} S C) ↦
              (mkIso (shiftAdd X.obj m n) ⋯ :
                Functor.obj (shiftFunctor C (m + n)) X ≅ Functor.obj (shiftFunctor C m ⋙ shiftFunctor C n) X))
            Y))
      (Iso.hom
          ((fun (X : DifferentialObject.{v, u, u_1} S C) ↦
              (mkIso (shiftAdd X.obj m n) ⋯ :
                Functor.obj (shiftFunctor C (m + n)) X ≅ Functor.obj (shiftFunctor C m ⋙ shiftFunctor C n) X))
            X) ≫
        Functor.map (shiftFunctor C m ⋙ shiftFunctor C n) f)
⊢ Iso (C := DifferentialObject.{v, u, u_1} S C ⥤ DifferentialObject.{v, u, u_1} S C) (shiftFunctor C (m + n))
    (shiftFunctor C m ⋙ shiftFunctor C n)

Tactic:
refine NatIso.ofComponents (fun X => mkIso (shiftAdd X.obj _ _) ?_) (fun f => ?_)

Premises used: CategoryTheory.DifferentialObject.mkIso, CategoryTheory.NatIso.ofComponents
-- 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
m n : S
X : DifferentialObject.{v, u, u_1} S C
refine_1 :
  Eq (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (m + 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)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) X.obj)))
    ((Functor.map (CategoryTheory.shiftFunctor C (m + n)) X.d ≫
          NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 (m + n))) X.obj) ≫
        Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m n)) X.obj) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (m + 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)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) X.obj)))
    (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m n)) X.obj ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n)
            (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 m) X.obj)))
          (Functor.map (CategoryTheory.shiftFunctor C n)
            (Functor.map (CategoryTheory.shiftFunctor C m) X.d ≫
              NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 m)) X.obj))
          (NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 n))
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) X.obj)) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (m + 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)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) X.obj)))
⊢ (Functor.obj (shiftFunctor C (m + n)) X).d ≫
      Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1) (Iso.hom (shiftAdd X.obj m n)) =
    Iso.hom (shiftAdd X.obj m n) ≫ (Functor.obj (shiftFunctor C m ⋙ shiftFunctor C n) X).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
m n : S
X : DifferentialObject.{v, u, u_1} S C
refine_1 :
  Eq (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m ⋙ 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)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) X.obj)))
    (Functor.map (CategoryTheory.shiftFunctor C m ⋙ CategoryTheory.shiftFunctor C n) X.d ≫
      NatTrans.app (Iso.inv (CategoryTheory.shiftFunctorAdd C m n))
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1) X.obj) ≫
        NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 (m + n))) X.obj ≫
          Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
            (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m n)) X.obj))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n)
        (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 m) X.obj)))
      (Functor.map (CategoryTheory.shiftFunctor C n)
        (Functor.map (CategoryTheory.shiftFunctor C m) X.d ≫
          NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 m)) X.obj))
      (NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 n))
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) X.obj)))
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m ⋙ 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)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) X.obj)))
    (NatTrans.app (Iso.inv (CategoryTheory.shiftFunctorAdd C m n)) X.obj ≫
      Functor.map (CategoryTheory.shiftFunctor C (m + n)) X.d ≫
        NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 (m + n))) X.obj ≫
          Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
            (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m n)) X.obj))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n)
        (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 m) X.obj)))
      (Functor.map (CategoryTheory.shiftFunctor C n)
        (Functor.map (CategoryTheory.shiftFunctor C m) X.d ≫
          NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 m)) X.obj))
      (NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 n))
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) X.obj)))

Tactic:
rw [← NatTrans.naturality_assoc]

Premises used: CategoryTheory.NatTrans.naturality_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
m n : S
X : DifferentialObject.{v, u, u_1} S C
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) 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)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) X.obj)))
    (Functor.map (CategoryTheory.shiftFunctor C n) (Functor.map (CategoryTheory.shiftFunctor C m) X.d) ≫
        NatTrans.app (Iso.inv (CategoryTheory.shiftFunctorAdd C m n))
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1) X.obj) ≫
          NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 (m + n))) X.obj ≫
            Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
              (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m n)) X.obj) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) 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)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) X.obj)))
    (CategoryStruct.comp (Y :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n)
          (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 m) X.obj)))
        (Functor.map (CategoryTheory.shiftFunctor C n)
          (Functor.map (CategoryTheory.shiftFunctor C m) X.d ≫
            NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 m)) X.obj))
        (NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 n))
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) X.obj)) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) 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)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) X.obj)))

Tactic:
simp only [Functor.map_comp, Category.assoc,
      shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app 1 m n X.obj,
      Iso.inv_hom_id_app_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app, CategoryTheory.DifferentialObject.obj, CategoryTheory.Functor.map_comp, OfNat.ofNat, CategoryTheory.Iso.inv_hom_id_app_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
m n : S
X Y : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
refine_2 :
  autoParam
    (Eq (α := (Functor.obj (shiftFunctor C (m + n)) X).obj ⟶ (Functor.obj (shiftFunctor C m ⋙ shiftFunctor C n) Y).obj)
      (Hom.f
        (Functor.map (shiftFunctor C (m + n)) f ≫
          Iso.hom
            ((fun (X : DifferentialObject.{v, u, u_1} S C) ↦
                (mkIso (shiftAdd X.obj m n) ⋯ :
                  Functor.obj (shiftFunctor C (m + n)) X ≅ Functor.obj (shiftFunctor C m ⋙ shiftFunctor C n) X))
              Y)))
      (Hom.f
        (Iso.hom
            ((fun (X : DifferentialObject.{v, u, u_1} S C) ↦
                (mkIso (shiftAdd X.obj m n) ⋯ :
                  Functor.obj (shiftFunctor C (m + n)) X ≅ Functor.obj (shiftFunctor C m ⋙ shiftFunctor C n) X))
              X) ≫
          Functor.map (shiftFunctor C m ⋙ shiftFunctor C n) f)))
    ext._auto_1
⊢ Eq (α := Functor.obj (shiftFunctor C (m + n)) X ⟶ Functor.obj (shiftFunctor C m ⋙ shiftFunctor C n) Y)
    (Functor.map (shiftFunctor C (m + n)) f ≫
      Iso.hom
        ((fun (X : DifferentialObject.{v, u, u_1} S C) ↦
            (mkIso (shiftAdd X.obj m n) ⋯ :
              Functor.obj (shiftFunctor C (m + n)) X ≅ Functor.obj (shiftFunctor C m ⋙ shiftFunctor C n) X))
          Y))
    (Iso.hom
        ((fun (X : DifferentialObject.{v, u, u_1} S C) ↦
            (mkIso (shiftAdd X.obj m n) ⋯ :
              Functor.obj (shiftFunctor C (m + n)) X ≅ Functor.obj (shiftFunctor C m ⋙ shiftFunctor C n) X))
          X) ≫
      Functor.map (shiftFunctor C m ⋙ shiftFunctor C n) f)

Tactic:
ext
-- 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
m n : S
X Y : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
refine_2 :
  autoParam
    (Eq (α :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (m + n)) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) Y.obj))
      (Functor.map (CategoryTheory.shiftFunctor C (m + n)) f.f ≫
        NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m n)) Y.obj)
      (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m n)) X.obj ≫
        Functor.map (CategoryTheory.shiftFunctor C n) (Functor.map (CategoryTheory.shiftFunctor C m) f.f)))
    ext._auto_1
⊢ autoParam
    (Eq (α := (Functor.obj (shiftFunctor C (m + n)) X).obj ⟶ (Functor.obj (shiftFunctor C m ⋙ shiftFunctor C n) Y).obj)
      (Hom.f
        (Functor.map (shiftFunctor C (m + n)) f ≫
          Iso.hom
            ((fun (X : DifferentialObject.{v, u, u_1} S C) ↦
                (mkIso (shiftAdd X.obj m n) ⋯ :
                  Functor.obj (shiftFunctor C (m + n)) X ≅ Functor.obj (shiftFunctor C m ⋙ shiftFunctor C n) X))
              Y)))
      (Hom.f
        (Iso.hom
            ((fun (X : DifferentialObject.{v, u, u_1} S C) ↦
                (mkIso (shiftAdd X.obj m n) ⋯ :
                  Functor.obj (shiftFunctor C (m + n)) X ≅ Functor.obj (shiftFunctor C m ⋙ shiftFunctor C n) X))
              X) ≫
          Functor.map (shiftFunctor C m ⋙ shiftFunctor C n) f)))
    ext._auto_1

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
m n : S
X Y : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
⊢ autoParam
    (Eq (α :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (m + n)) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) Y.obj))
      (Functor.map (CategoryTheory.shiftFunctor C (m + n)) f.f ≫
        NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m n)) Y.obj)
      (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m n)) X.obj ≫
        Functor.map (CategoryTheory.shiftFunctor C n) (Functor.map (CategoryTheory.shiftFunctor C m) f.f)))
    ext._auto_1

Tactic:
NatTrans.naturality _ _

Premises used: CategoryTheory.NatTrans.naturality