awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
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 (FC := FC) (CC := CC)
        { f := ConcreteCategory.ofHom (FC := FC) (CC := CC) (↑x : FC X.obj Y.obj), comm := ⋯ : X.Hom Y }.f)
      ⋯ =
    x
have 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)))
    sorry =
  x
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
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)))
      ⋯ =
    x
have 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)))
        sorry) :
    FC X.obj Y.obj) =
  (↑x : FC X.obj Y.obj)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
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
⊢ {
      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
have 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) sorry) :
              FC X.obj Y.obj),
        comm := sorry : X.Hom Y }.f =
  ConcreteCategory.hom (FC := FC) (CC := CC) x.f
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
n : S
X Y : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
⊢ { 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
have 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))
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
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) 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))
have 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))
Tactic: rw [Category.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
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) 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))
have 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))
Tactic: erw [shiftComm_hom_comp]
-- 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 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) 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))
have 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))
Tactic: rw [← Functor.map_comp_assoc, f.comm, Functor.map_comp_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
n : S
X : DifferentialObject.{v, u, u_1} S C
⊢ { 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 }
have w : autoParam
  (Hom.f { f := Functor.map (CategoryTheory.shiftFunctor C n) (Hom.f (𝟙 X)), comm := sorry } =
    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 := sorry : DifferentialObject.{v, u, u_1} S C }))
  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 { 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
have 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
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
n : S
X : DifferentialObject.{v, u, u_1} S C
⊢ autoParam
    (Functor.map (CategoryTheory.shiftFunctor C n) (𝟙 X.obj) =
      𝟙 (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj))
    ext._auto_1
have 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
Tactic: rw [Functor.map_id]
-- 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 Y Z : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
g : Y ⟶ Z
⊢ 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 := ⋯ })
have 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 := sorry : 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 := sorry : DifferentialObject.{v, u, u_1} S C }.obj)
    (Hom.f { f := Functor.map (CategoryTheory.shiftFunctor C n) (f ≫ g).f, comm := sorry })
    (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 := sorry })
        { f := Functor.map (CategoryTheory.shiftFunctor C n) f.f, comm := sorry }
        { f := Functor.map (CategoryTheory.shiftFunctor C n) g.f, comm := sorry })))
  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 Y Z : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
g : Y ⟶ Z
⊢ 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
have 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
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
n : S
X Y Z : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
g : Y ⟶ Z
⊢ 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
have 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
Tactic: rw [Functor.map_comp]
-- 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
⊢ 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_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
Tactic: refine NatIso.ofComponents (fun X => mkIso (shiftAdd X.obj _ _) ?_) (fun f => ?_)