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
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:
exact NatTrans.naturality _ _

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

Tactic:
refine NatIso.ofComponents (fun X => mkIso ((shiftFunctorZero C S).app 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
X : DifferentialObject.{v, u, u_1} S C
refine_1 :
  (Functor.obj (shiftFunctor C 0) X).d ≫
      Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
        (Iso.hom (Iso.app (shiftFunctorZero C S) X.obj)) =
    Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 0)
        (Functor.obj (𝟭 (DifferentialObject.{v, u, u_1} S C)) X).2 ≫
      NatTrans.app (Iso.hom (shiftFunctorZero C S))
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (Functor.obj (𝟭 (DifferentialObject.{v, u, u_1} S C)) X).1)
⊢ (Functor.obj (shiftFunctor C 0) X).d ≫
      Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
        (Iso.hom (Iso.app (shiftFunctorZero C S) X.obj)) =
    Iso.hom (Iso.app (shiftFunctorZero C S) X.obj) ≫ (Functor.obj (𝟭 (DifferentialObject.{v, u, u_1} S C)) X).d

Tactic:
erw [← NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality
-- 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
X : DifferentialObject.{v, u, u_1} S C
refine_1 :
  Eq (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 0) X.obj ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1) X.obj)
    (CategoryStruct.comp (Y :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 0) X.obj))
        (Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 0) X.d ≫
          NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C (A := S) 1 0)) X.obj)
        (Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (NatTrans.app (Iso.hom (shiftFunctorZero C S)) X.obj)) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 0) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1) X.obj)
    (Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 0) X.2 ≫
        NatTrans.app (Iso.hom (shiftFunctorZero C S))
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1) X.1) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 0) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1) X.1)
⊢ (Functor.obj (shiftFunctor C 0) X).d ≫
      Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
        (Iso.hom (Iso.app (shiftFunctorZero C S) X.obj)) =
    Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 0)
        (Functor.obj (𝟭 (DifferentialObject.{v, u, u_1} S C)) X).2 ≫
      NatTrans.app (Iso.hom (shiftFunctorZero C S))
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (Functor.obj (𝟭 (DifferentialObject.{v, u, u_1} S C)) X).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
X : DifferentialObject.{v, u, u_1} S C
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 0) X.obj ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1) X.obj)
    (CategoryStruct.comp (Y :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 0) X.obj))
        (Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 0) X.d ≫
          NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C (A := S) 1 0)) X.obj)
        (Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (NatTrans.app (Iso.hom (shiftFunctorZero C S)) X.obj)) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 0) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1) X.obj)
    (Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 0) X.2 ≫
        NatTrans.app (Iso.hom (shiftFunctorZero C S))
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1) X.1) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 0) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1) X.1)

Tactic:
simp only [shiftFunctorZero_hom_app_shift, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.shiftFunctorZero_hom_app_shift
-- 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₁ m₂ m₃ : S
X : DifferentialObject.{v, u, u_1} S C
w :
  autoParam
    (Hom.f
        (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X ≫
          Functor.map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X)) =
      (eqToHom ⋯ ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X ≫
            NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (Functor.obj (shiftFunctor C m₁) X)).f)
    ext._auto_1
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X ≫
      Functor.map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X) =
    eqToHom ⋯ ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (Functor.obj (shiftFunctor C m₁) X)

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
m₁ m₂ m₃ : S
X : DifferentialObject.{v, u, u_1} S C
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (m₁ + m₂ + m₃)) X.obj ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₃)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₁ ⋙ CategoryTheory.shiftFunctor C m₂) X.obj))
    (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C (m₁ + m₂) m₃)) X.obj ≫
        Functor.map (CategoryTheory.shiftFunctor C m₃)
          (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m₁ m₂)) X.obj) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (m₁ + m₂ + m₃)) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₃)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₁ ⋙ CategoryTheory.shiftFunctor C m₂) X.obj))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯)) X.obj ≫
        NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m₂ m₃))
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₁) X.obj) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (m₁ + m₂ + m₃)) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₂ ⋙ CategoryTheory.shiftFunctor C m₃)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₁) X.obj))

Tactic:
shiftFunctorAdd_assoc_hom_app m₁ m₂ m₃ X.obj

Premises used: CategoryTheory.DifferentialObject.obj, CategoryTheory.shiftFunctorAdd_assoc_hom_app
-- 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₁ m₂ m₃ : S
X : DifferentialObject.{v, u, u_1} S C
h :
  ((Functor.obj (shiftFunctor C (m₁ + m₂ + m₃)) X).obj ⟶
        (Functor.obj (shiftFunctor C m₃) (Functor.obj (shiftFunctor C m₁ ⋙ shiftFunctor C m₂) X)).obj) =
      (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (m₁ + m₂ + m₃)) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₃)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₁ ⋙ CategoryTheory.shiftFunctor C m₂) X.obj)) →
    (eqToHom ⋯ ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X ≫
            NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (Functor.obj (shiftFunctor C m₁) X)).f =
      NatTrans.app (Iso.hom (shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯)) X.obj ≫
        NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m₂ m₃))
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₁) X.obj)
⊢ autoParam
    (Hom.f
        (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X ≫
          Functor.map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X)) =
      (eqToHom ⋯ ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X ≫
            NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (Functor.obj (shiftFunctor C m₁) X)).f)
    ext._auto_1

Tactic:
convert! shiftFunctorAdd_assoc_hom_app m₁ m₂ m₃ X.obj

Premises used: CategoryTheory.DifferentialObject.obj, CategoryTheory.shiftFunctorAdd_assoc_hom_app
-- 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₁ m₂ m₃ : S
X : DifferentialObject.{v, u, u_1} S C
e_1 :
  ((Functor.obj (shiftFunctor C (m₁ + m₂ + m₃)) X).obj ⟶
      (Functor.obj (shiftFunctor C m₃) (Functor.obj (shiftFunctor C m₁ ⋙ shiftFunctor C m₂) X)).obj) =
    (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (m₁ + m₂ + m₃)) X.obj ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₃)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₁ ⋙ CategoryTheory.shiftFunctor C m₂) X.obj))
h :
  Eq (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (m₁ + m₂ + m₃)) X.obj ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₃)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₂)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₁) X.obj)))
    (Hom.f (eqToHom ⋯) ≫
        NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m₁ (m₂ + m₃))) X.obj ≫
          NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m₂ m₃))
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₁) X.obj) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (m₁ + m₂ + m₃)) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₃)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₂)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₁) X.obj)))
    ((NatTrans.app (eqToHom ⋯) X.obj ≫ NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m₁ (m₂ + m₃))) X.obj) ≫
        NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m₂ m₃))
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₁) X.obj) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (m₁ + m₂ + m₃)) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₃)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₂)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₁) X.obj)))
⊢ (eqToHom ⋯ ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (Functor.obj (shiftFunctor C m₁) X)).f =
    NatTrans.app (Iso.hom (shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯)) X.obj ≫
      NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m₂ m₃))
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₁) X.obj)

Tactic:
dsimp [shiftFunctorAdd']

Premises used: CategoryTheory.shiftFunctorAdd'
-- 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₁ m₂ m₃ : S
X : DifferentialObject.{v, u, u_1} S C
e_1 :
  ((Functor.obj (shiftFunctor C (m₁ + m₂ + m₃)) X).obj ⟶
      (Functor.obj (shiftFunctor C m₃) (Functor.obj (shiftFunctor C m₁ ⋙ shiftFunctor C m₂) X)).obj) =
    (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (m₁ + m₂ + m₃)) X.obj ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₃)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₁ ⋙ CategoryTheory.shiftFunctor C m₂) X.obj))
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (m₁ + m₂ + m₃)) X.obj ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₃)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₂)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₁) X.obj)))
    (Hom.f (eqToHom ⋯) ≫
        NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m₁ (m₂ + m₃))) X.obj ≫
          NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m₂ m₃))
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₁) X.obj) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (m₁ + m₂ + m₃)) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₃)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₂)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₁) X.obj)))
    ((NatTrans.app (eqToHom ⋯) X.obj ≫ NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m₁ (m₂ + m₃))) X.obj) ≫
        NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m₂ m₃))
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₁) X.obj) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (m₁ + m₂ + m₃)) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₃)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₂)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₁) X.obj)))

Tactic:
simp
-- 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 (NatTrans.app (Iso.hom (shiftFunctorAdd C 0 n)) X) =
      Hom.f (eqToHom ⋯ ≫ Functor.map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftZero C)) X)))
    ext._auto_1
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd C 0 n)) X =
    eqToHom ⋯ ≫ Functor.map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftZero C)) X)

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
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (0 + n)) X.obj ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 0 ⋙ CategoryTheory.shiftFunctor C n)
        X.obj)
    (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C 0 n)) X.obj)
    (eqToHom ⋯ ≫ Functor.map (CategoryTheory.shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorZero C S)) X.obj))

Tactic:
shiftFunctorAdd_zero_add_hom_app n X.obj

Premises used: CategoryTheory.shiftFunctorAdd_zero_add_hom_app, CategoryTheory.DifferentialObject.obj
-- 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
h :
  ((Functor.obj (shiftFunctor C (0 + n)) X).obj ⟶ (Functor.obj (shiftFunctor C 0 ⋙ shiftFunctor C n) X).obj) =
      (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (0 + n)) X.obj ⟶
        Functor.obj.{v, v, u, u}
          (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 0 ⋙ CategoryTheory.shiftFunctor C n) X.obj) →
    Eq (α := (Functor.obj (shiftFunctor C (0 + n)) X).obj ⟶ (Functor.obj (shiftFunctor C 0 ⋙ shiftFunctor C n) X).obj)
      (Hom.f (eqToHom ⋯ ≫ Functor.map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftZero C)) X)))
      (eqToHom ⋯ ≫ Functor.map (CategoryTheory.shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorZero C S)) X.obj))
⊢ autoParam
    (Hom.f (NatTrans.app (Iso.hom (shiftFunctorAdd C 0 n)) X) =
      Hom.f (eqToHom ⋯ ≫ Functor.map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftZero C)) X)))
    ext._auto_1

Tactic:
convert! shiftFunctorAdd_zero_add_hom_app n X.obj

Premises used: CategoryTheory.shiftFunctorAdd_zero_add_hom_app, CategoryTheory.DifferentialObject.obj
-- 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
e_1 :
  ((Functor.obj (shiftFunctor C (0 + n)) X).obj ⟶ (Functor.obj (shiftFunctor C 0 ⋙ shiftFunctor C n) X).obj) =
    (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (0 + n)) X.obj ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 0 ⋙ CategoryTheory.shiftFunctor C n)
        X.obj)
⊢ Eq (α := (Functor.obj (shiftFunctor C (0 + n)) X).obj ⟶ (Functor.obj (shiftFunctor C 0 ⋙ shiftFunctor C n) X).obj)
    (Hom.f (eqToHom ⋯ ≫ Functor.map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftZero C)) X)))
    (eqToHom ⋯ ≫ Functor.map (CategoryTheory.shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorZero C S)) X.obj))

Tactic:
simp
-- 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 (NatTrans.app (Iso.hom (shiftFunctorAdd C n 0)) X) =
      Hom.f (eqToHom ⋯ ≫ NatTrans.app (Iso.inv (shiftZero C)) (Functor.obj (shiftFunctor C n) X)))
    ext._auto_1
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd C n 0)) X =
    eqToHom ⋯ ≫ NatTrans.app (Iso.inv (shiftZero C)) (Functor.obj (shiftFunctor C n) X)

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
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (n + 0)) X.obj ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n ⋙ CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 0)
        X.obj)
    (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C n 0)) X.obj)
    (eqToHom ⋯ ≫
      NatTrans.app (Iso.inv (shiftFunctorZero C S)) (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj))

Tactic:
shiftFunctorAdd_add_zero_hom_app n X.obj

Premises used: CategoryTheory.DifferentialObject.obj, CategoryTheory.shiftFunctorAdd_add_zero_hom_app
-- 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
h :
  ((Functor.obj (shiftFunctor C (n + 0)) X).obj ⟶ (Functor.obj (shiftFunctor C n ⋙ shiftFunctor C 0) X).obj) =
      (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (n + 0)) X.obj ⟶
        Functor.obj.{v, v, u, u}
          (CategoryTheory.shiftFunctor C n ⋙ CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 0) X.obj) →
    Hom.f (eqToHom ⋯ ≫ NatTrans.app (Iso.inv (shiftZero C)) (Functor.obj (shiftFunctor C n) X)) =
      eqToHom ⋯ ≫
        NatTrans.app (Iso.inv (shiftFunctorZero C S)) (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj)
⊢ autoParam
    (Hom.f (NatTrans.app (Iso.hom (shiftFunctorAdd C n 0)) X) =
      Hom.f (eqToHom ⋯ ≫ NatTrans.app (Iso.inv (shiftZero C)) (Functor.obj (shiftFunctor C n) X)))
    ext._auto_1

Tactic:
convert! shiftFunctorAdd_add_zero_hom_app n X.obj

Premises used: CategoryTheory.DifferentialObject.obj, CategoryTheory.shiftFunctorAdd_add_zero_hom_app
-- 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
e_1 :
  ((Functor.obj (shiftFunctor C (n + 0)) X).obj ⟶ (Functor.obj (shiftFunctor C n ⋙ shiftFunctor C 0) X).obj) =
    (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (n + 0)) X.obj ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n ⋙ CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 0)
        X.obj)
⊢ Hom.f (eqToHom ⋯ ≫ NatTrans.app (Iso.inv (shiftZero C)) (Functor.obj (shiftFunctor C n) X)) =
    eqToHom ⋯ ≫
      NatTrans.app (Iso.inv (shiftFunctorZero C S)) (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj)

Tactic:
simp