awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
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
⊢ 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)
have 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) sorry :
              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) sorry :
              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: refine NatIso.ofComponents (fun X => mkIso (shiftAdd X.obj _ _) ?_) (fun f => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
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
⊢ (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
have 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)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
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 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)))
have 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)))
Tactic: rw [← NatTrans.naturality_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
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
⊢ 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)
have 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) sorry :
                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) sorry :
                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: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
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 (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
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
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
⊢ 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))
have 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
Tactic: refine NatIso.ofComponents (fun X => mkIso ((shiftFunctorZero C S).app X.obj) ?_) (fun f => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
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
⊢ 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))
have 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) sorry :
              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) sorry :
              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)
Tactic: refine NatIso.ofComponents (fun X => mkIso ((shiftFunctorZero C S).app X.obj) ?_) (fun f => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
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
⊢ (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
have 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)
Tactic: erw [← NatTrans.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
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
⊢ (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)
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
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
⊢ 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)
have 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 sorry ≫
        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: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
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
⊢ 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
have 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 sorry ≫
        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₃) sorry)) X.obj ≫
      NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m₂ m₃))
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m₁) X.obj)
Tactic: convert! shiftFunctorAdd_assoc_hom_app m₁ m₂ m₃ X.obj
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
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))
⊢ (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)
have 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 sorry) ≫
      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 sorry) 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: dsimp [shiftFunctorAdd']
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
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
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd C 0 n)) X =
    eqToHom ⋯ ≫ Functor.map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftZero C)) X)
have w : autoParam
  (Hom.f (NatTrans.app (Iso.hom (shiftFunctorAdd C 0 n)) X) =
    Hom.f (eqToHom sorry ≫ Functor.map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftZero C)) X)))
  ext._auto_1
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
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
⊢ 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
have 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 sorry ≫ Functor.map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftZero C)) X)))
    (eqToHom sorry ≫ Functor.map (CategoryTheory.shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorZero C S)) X.obj))
Tactic: convert! shiftFunctorAdd_zero_add_hom_app n X.obj
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
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
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd C n 0)) X =
    eqToHom ⋯ ≫ NatTrans.app (Iso.inv (shiftZero C)) (Functor.obj (shiftFunctor C n) X)
have w : autoParam
  (Hom.f (NatTrans.app (Iso.hom (shiftFunctorAdd C n 0)) X) =
    Hom.f (eqToHom sorry ≫ NatTrans.app (Iso.inv (shiftZero C)) (Functor.obj (shiftFunctor C n) X)))
  ext._auto_1
Tactic: ext1