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
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
X Y : DifferentialObject.{v, u, u_1} S C
f : X.obj ≅ Y.obj
hf : X.d ≫ Functor.map (shiftFunctor.{v, u, u_1} C (A := S) 1) f.hom = f.hom ≫ Y.d
⊢ Y.d ≫ Functor.map (shiftFunctor.{v, u, u_1} C (A := S) 1) f.inv = f.inv ≫ X.d
have rw : Y.d ≫ Iso.inv (Functor.mapIso (shiftFunctor.{v, u, u_1} C (A := S) 1) f) = f.inv ≫ X.d
Tactic: rw [← Functor.mapIso_inv, Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp, Functor.mapIso_hom,
      hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
X Y : DifferentialObject.{v, u, u_1} S C
f : X.obj ≅ Y.obj
hf : X.d ≫ Functor.map (shiftFunctor.{v, u, u_1} C (A := S) 1) f.hom = f.hom ≫ Y.d
rw : Y.d ≫ Iso.inv (Functor.mapIso (shiftFunctor.{v, u, u_1} C (A := S) 1) f) = f.inv ≫ X.d
⊢ Y.d ≫ Functor.map (shiftFunctor.{v, u, u_1} C (A := S) 1) f.inv = f.inv ≫ X.d
have rw₁ : Y.d = (f.inv ≫ X.d) ≫ Iso.hom (Functor.mapIso (shiftFunctor.{v, u, u_1} C (A := S) 1) f)
Tactic: rw [← Functor.mapIso_inv, Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp, Functor.mapIso_hom,
      hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
X Y : DifferentialObject.{v, u, u_1} S C
f : X.obj ≅ Y.obj
hf : X.d ≫ Functor.map (shiftFunctor.{v, u, u_1} C (A := S) 1) f.hom = f.hom ≫ Y.d
rw : Y.d ≫ Iso.inv (Functor.mapIso (shiftFunctor.{v, u, u_1} C (A := S) 1) f) = f.inv ≫ X.d
rw₁ : Y.d = (f.inv ≫ X.d) ≫ Iso.hom (Functor.mapIso (shiftFunctor.{v, u, u_1} C (A := S) 1) f)
⊢ Y.d ≫ Functor.map (shiftFunctor.{v, u, u_1} C (A := S) 1) f.inv = f.inv ≫ X.d
have rw₂ : Y.d = f.inv ≫ X.d ≫ Iso.hom (Functor.mapIso (shiftFunctor.{v, u, u_1} C (A := S) 1) f)
Tactic: rw [← Functor.mapIso_inv, Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp, Functor.mapIso_hom,
      hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
X Y : DifferentialObject.{v, u, u_1} S C
f : X.obj ≅ Y.obj
hf : X.d ≫ Functor.map (shiftFunctor.{v, u, u_1} C (A := S) 1) f.hom = f.hom ≫ Y.d
rw : Y.d ≫ Iso.inv (Functor.mapIso (shiftFunctor.{v, u, u_1} C (A := S) 1) f) = f.inv ≫ X.d
rw₁ : Y.d = (f.inv ≫ X.d) ≫ Iso.hom (Functor.mapIso (shiftFunctor.{v, u, u_1} C (A := S) 1) f)
rw₂ : Y.d = f.inv ≫ X.d ≫ Iso.hom (Functor.mapIso (shiftFunctor.{v, u, u_1} C (A := S) 1) f)
⊢ Y.d ≫ Functor.map (shiftFunctor.{v, u, u_1} C (A := S) 1) f.inv = f.inv ≫ X.d
have rw₃ : f.hom ≫ Y.d = X.d ≫ Iso.hom (Functor.mapIso (shiftFunctor.{v, u, u_1} C (A := S) 1) f)
Tactic: rw [← Functor.mapIso_inv, Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp, Functor.mapIso_hom,
      hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
X Y : DifferentialObject.{v, u, u_1} S C
f : X.obj ≅ Y.obj
hf : X.d ≫ Functor.map (shiftFunctor.{v, u, u_1} C (A := S) 1) f.hom = f.hom ≫ Y.d
rw : Y.d ≫ Iso.inv (Functor.mapIso (shiftFunctor.{v, u, u_1} C (A := S) 1) f) = f.inv ≫ X.d
rw₁ : Y.d = (f.inv ≫ X.d) ≫ Iso.hom (Functor.mapIso (shiftFunctor.{v, u, u_1} C (A := S) 1) f)
rw₂ : Y.d = f.inv ≫ X.d ≫ Iso.hom (Functor.mapIso (shiftFunctor.{v, u, u_1} C (A := S) 1) f)
rw₃ : f.hom ≫ Y.d = X.d ≫ Iso.hom (Functor.mapIso (shiftFunctor.{v, u, u_1} C (A := S) 1) f)
⊢ Y.d ≫ Functor.map (shiftFunctor.{v, u, u_1} C (A := S) 1) f.inv = f.inv ≫ X.d
have rw₄ : f.hom ≫ Y.d = X.d ≫ Functor.map (shiftFunctor.{v, u, u_1} C (A := S) 1) f.hom
Tactic: rw [← Functor.mapIso_inv, Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp, Functor.mapIso_hom,
      hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
X Y : DifferentialObject.{v, u, u_1} S C
f : X.obj ≅ Y.obj
hf : X.d ≫ Functor.map (shiftFunctor.{v, u, u_1} C (A := S) 1) f.hom = f.hom ≫ Y.d
rw : Y.d ≫ Iso.inv (Functor.mapIso (shiftFunctor.{v, u, u_1} C (A := S) 1) f) = f.inv ≫ X.d
rw₁ : Y.d = (f.inv ≫ X.d) ≫ Iso.hom (Functor.mapIso (shiftFunctor.{v, u, u_1} C (A := S) 1) f)
rw₂ : Y.d = f.inv ≫ X.d ≫ Iso.hom (Functor.mapIso (shiftFunctor.{v, u, u_1} C (A := S) 1) f)
rw₃ : f.hom ≫ Y.d = X.d ≫ Iso.hom (Functor.mapIso (shiftFunctor.{v, u, u_1} C (A := S) 1) f)
rw₄ : f.hom ≫ Y.d = X.d ≫ Functor.map (shiftFunctor.{v, u, u_1} C (A := S) 1) f.hom
⊢ Y.d ≫ Functor.map (shiftFunctor.{v, u, u_1} C (A := S) 1) f.inv = f.inv ≫ X.d
have rw₅ : f.hom ≫ Y.d = f.hom ≫ Y.d
Tactic: rw [← Functor.mapIso_inv, Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp, Functor.mapIso_hom,
      hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
X Y : DifferentialObject.{v, u, u_1} S C
f : X.obj ≅ Y.obj
hf : X.d ≫ Functor.map (shiftFunctor.{v, u, u_1} C (A := S) 1) f.hom = f.hom ≫ Y.d
⊢ { f := f.hom, comm := hf : X.Hom Y } ≫ { f := f.inv, comm := ⋯ } = 𝟙 X
have w : autoParam (Hom.f ({ f := f.hom, comm := hf : X.Hom Y } ≫ { f := f.inv, comm := sorry }) = Hom.f (𝟙 X)) ext._auto_1
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
X Y : DifferentialObject.{v, u, u_1} S C
f : X.obj ≅ Y.obj
hf : X.d ≫ Functor.map (shiftFunctor.{v, u, u_1} C (A := S) 1) f.hom = f.hom ≫ Y.d
⊢ autoParam (Hom.f ({ f := f.hom, comm := hf : X.Hom Y } ≫ { f := f.inv, comm := ⋯ }) = Hom.f (𝟙 X)) ext._auto_1
have w : autoParam (f.hom ≫ f.inv = 𝟙 X.obj) ext._auto_1
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
X Y : DifferentialObject.{v, u, u_1} S C
f : X.obj ≅ Y.obj
hf : X.d ≫ Functor.map (shiftFunctor.{v, u, u_1} C (A := S) 1) f.hom = f.hom ≫ Y.d
⊢ { f := f.inv, comm := ⋯ : Y.Hom X } ≫ { f := f.hom, comm := hf } = 𝟙 Y
have w : autoParam (Hom.f ({ f := f.inv, comm := sorry : Y.Hom X } ≫ { f := f.hom, comm := hf }) = Hom.f (𝟙 Y)) ext._auto_1
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
X Y : DifferentialObject.{v, u, u_1} S C
f : X.obj ≅ Y.obj
hf : X.d ≫ Functor.map (shiftFunctor.{v, u, u_1} C (A := S) 1) f.hom = f.hom ≫ Y.d
⊢ autoParam (Hom.f ({ f := f.inv, comm := ⋯ : Y.Hom X } ≫ { f := f.hom, comm := hf }) = Hom.f (𝟙 Y)) ext._auto_1
have w : autoParam (f.inv ≫ f.hom = 𝟙 Y.obj) ext._auto_1
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
D : Type u'
inst_4 : Category.{v', u'} D
inst_5 : HasZeroMorphisms.{v', u'} D
inst_6 : HasShift.{v', u', u_1} D S
F : Functor.{v, v', u, u'} C D
η : shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F ⟶ F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1
hF : ∀ (c c' : C), Eq (α := F.obj c ⟶ F.obj c') (F.map 0) 0
X : DifferentialObject.{v, u, u_1} S C
⊢ (F.map X.d ≫ η.app X.obj) ≫ map (shiftFunctor.{v', u', u_1} D (A := S) 1) (F.map X.d ≫ η.app X.obj) = 0
have rw : (F.map X.d ≫ η.app X.obj) ≫
    (F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1).map X.d ≫
      map (shiftFunctor.{v', u', u_1} D (A := S) 1) (η.app X.obj) =
  0
Tactic: rw [Functor.map_comp, ← Functor.comp_map F (shiftFunctor D (1 : S))]
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
D : Type u'
inst_4 : Category.{v', u'} D
inst_5 : HasZeroMorphisms.{v', u'} D
inst_6 : HasShift.{v', u', u_1} D S
F : Functor.{v, v', u, u'} C D
η : shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F ⟶ F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1
hF : ∀ (c c' : C), Eq (α := F.obj c ⟶ F.obj c') (F.map 0) 0
X : DifferentialObject.{v, u, u_1} S C
| η.app X.obj ≫ (F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1).map X.d
have a : (shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F).map X.d ≫
  η.app (obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := S) 1) X.obj)
Tactic: rw [← η.naturality X.d]
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
D : Type u'
inst_4 : Category.{v', u'} D
inst_5 : HasZeroMorphisms.{v', u'} D
inst_6 : HasShift.{v', u', u_1} D S
F : Functor.{v, v', u, u'} C D
η : shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F ⟶ F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1
hF : ∀ (c c' : C), Eq (α := F.obj c ⟶ F.obj c') (F.map 0) 0
X : DifferentialObject.{v, u, u_1} S C
⊢ (F.map X.d ≫ η.app X.obj) ≫
      (F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1).map X.d ≫
        map (shiftFunctor.{v', u', u_1} D (A := S) 1) (η.app X.obj) =
    0
have slice_lhs : F.map X.d ≫
    ((shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F).map X.d ≫
        η.app (obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := S) 1) X.obj)) ≫
      map (shiftFunctor.{v', u', u_1} D (A := S) 1) (η.app X.obj) =
  0
Tactic: slice_lhs 2 3 => rw [← η.naturality X.d]
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
D : Type u'
inst_4 : Category.{v', u'} D
inst_5 : HasZeroMorphisms.{v', u'} D
inst_6 : HasShift.{v', u', u_1} D S
F : Functor.{v, v', u, u'} C D
η : shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F ⟶ F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1
hF : ∀ (c c' : C), Eq (α := F.obj c ⟶ F.obj c') (F.map 0) 0
X : DifferentialObject.{v, u, u_1} S C
⊢ F.map X.d ≫
      ((shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F).map X.d ≫
          η.app (obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := S) 1) X.obj)) ≫
        map (shiftFunctor.{v', u', u_1} D (A := S) 1) (η.app X.obj) =
    0
have rw : F.map X.d ≫
    (F.map (map (shiftFunctor.{v, u, u_1} C (A := S) 1) X.d) ≫
        η.app (obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := S) 1) X.obj)) ≫
      map (shiftFunctor.{v', u', u_1} D (A := S) 1) (η.app X.obj) =
  0
Tactic: rw [Functor.comp_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
D : Type u'
inst_4 : Category.{v', u'} D
inst_5 : HasZeroMorphisms.{v', u'} D
inst_6 : HasShift.{v', u', u_1} D S
F : Functor.{v, v', u, u'} C D
η : shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F ⟶ F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1
hF : ∀ (c c' : C), Eq (α := F.obj c ⟶ F.obj c') (F.map 0) 0
X : DifferentialObject.{v, u, u_1} S C
| F.map X.d ≫ F.map (map (shiftFunctor.{v, u, u_1} C (A := S) 1) X.d)
have a : 0
Tactic: rw [← F.map_comp, X.d_squared, hF]
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
D : Type u'
inst_4 : Category.{v', u'} D
inst_5 : HasZeroMorphisms.{v', u'} D
inst_6 : HasShift.{v', u', u_1} D S
F : Functor.{v, v', u, u'} C D
η : shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F ⟶ F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1
hF : ∀ (c c' : C), Eq (α := F.obj c ⟶ F.obj c') (F.map 0) 0
X : DifferentialObject.{v, u, u_1} S C
⊢ F.map X.d ≫
      (F.map (map (shiftFunctor.{v, u, u_1} C (A := S) 1) X.d) ≫
          η.app (obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := S) 1) X.obj)) ≫
        map (shiftFunctor.{v', u', u_1} D (A := S) 1) (η.app X.obj) =
    0
have slice_lhs : Eq (α :=
  F.obj X.obj ⟶
    obj.{v', v', u', u'} (shiftFunctor.{v', u', u_1} D (A := S) 1)
      (obj.{v', v', u', u'} (shiftFunctor.{v', u', u_1} D (A := S) 1) (F.obj X.obj)))
  ((0 ≫ η.app (obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := S) 1) X.obj)) ≫
    map (shiftFunctor.{v', u', u_1} D (A := S) 1) (η.app X.obj))
  0
Tactic: slice_lhs 1 2 => rw [← F.map_comp, X.d_squared, hF]
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
D : Type u'
inst_4 : Category.{v', u'} D
inst_5 : HasZeroMorphisms.{v', u'} D
inst_6 : HasShift.{v', u', u_1} D S
F : Functor.{v, v', u, u'} C D
η : shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F ⟶ F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1
hF : ∀ (c c' : C), Eq (α := F.obj c ⟶ F.obj c') (F.map 0) 0
X : DifferentialObject.{v, u, u_1} S C
⊢ Eq (α :=
    F.obj X.obj ⟶
      obj.{v', v', u', u'} (shiftFunctor.{v', u', u_1} D (A := S) 1)
        (obj.{v', v', u', u'} (shiftFunctor.{v', u', u_1} D (A := S) 1) (F.obj X.obj)))
    ((0 ≫ η.app (obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := S) 1) X.obj)) ≫
      map (shiftFunctor.{v', u', u_1} D (A := S) 1) (η.app X.obj))
    0
have rw : Eq (α :=
  F.obj X.obj ⟶
    obj.{v', v', u', u'} (shiftFunctor.{v', u', u_1} D (A := S) 1)
      (obj.{v', v', u', u'} (shiftFunctor.{v', u', u_1} D (A := S) 1) (F.obj X.obj)))
  (0 ≫ map (shiftFunctor.{v', u', u_1} D (A := S) 1) (η.app X.obj)) 0
Tactic: rw [zero_comp, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
D : Type u'
inst_4 : Category.{v', u'} D
inst_5 : HasZeroMorphisms.{v', u'} D
inst_6 : HasShift.{v', u', u_1} D S
F : Functor.{v, v', u, u'} C D
η : shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F ⟶ F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1
hF : ∀ (c c' : C), Eq (α := F.obj c ⟶ F.obj c') (F.map 0) 0
X : DifferentialObject.{v, u, u_1} S C
rw :
  Eq (α :=
    F.obj X.obj ⟶
      obj.{v', v', u', u'} (shiftFunctor.{v', u', u_1} D (A := S) 1)
        (obj.{v', v', u', u'} (shiftFunctor.{v', u', u_1} D (A := S) 1) (F.obj X.obj)))
    (0 ≫ map (shiftFunctor.{v', u', u_1} D (A := S) 1) (η.app X.obj)) 0
⊢ Eq (α :=
    F.obj X.obj ⟶
      obj.{v', v', u', u'} (shiftFunctor.{v', u', u_1} D (A := S) 1)
        (obj.{v', v', u', u'} (shiftFunctor.{v', u', u_1} D (A := S) 1) (F.obj X.obj)))
    ((0 ≫ η.app (obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := S) 1) X.obj)) ≫
      map (shiftFunctor.{v', u', u_1} D (A := S) 1) (η.app X.obj))
    0
have rw₁ : Eq.{v' + 1} (α :=
  F.obj X.obj ⟶
    obj.{v', v', u', u'} (shiftFunctor.{v', u', u_1} D (A := S) 1)
      (obj.{v', v', u', u'} (shiftFunctor.{v', u', u_1} D (A := S) 1) (F.obj X.obj)))
  0 0
Tactic: rw [zero_comp, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
D : Type u'
inst_4 : Category.{v', u'} D
inst_5 : HasZeroMorphisms.{v', u'} D
inst_6 : HasShift.{v', u', u_1} D S
F : Functor.{v, v', u, u'} C D
η : shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F ⟶ F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1
hF : ∀ (c c' : C), Eq (α := F.obj c ⟶ F.obj c') (F.map 0) 0
X Y : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
⊢ { obj := F.obj X.obj, d := F.map X.d ≫ η.app X.obj, d_squared := ⋯ : DifferentialObject.{v', u', u_1} S D }.d ≫
      map (shiftFunctor.{v', u', u_1} D (A := S) 1) (F.map f.f) =
    F.map f.f ≫ { obj := F.obj Y.obj, d := F.map Y.d ≫ η.app Y.obj, d_squared := ⋯ }.d
have dsimp : (F.map X.d ≫ η.app X.obj) ≫ map (shiftFunctor.{v', u', u_1} D (A := S) 1) (F.map f.f) =
  F.map f.f ≫ F.map Y.d ≫ η.app Y.obj
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
D : Type u'
inst_4 : Category.{v', u'} D
inst_5 : HasZeroMorphisms.{v', u'} D
inst_6 : HasShift.{v', u', u_1} D S
F : Functor.{v, v', u, u'} C D
η : shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F ⟶ F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1
hF : ∀ (c c' : C), Eq (α := F.obj c ⟶ F.obj c') (F.map 0) 0
X Y : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
| η.app X.obj ≫ map (shiftFunctor.{v', u', u_1} D (A := S) 1) (F.map f.f)
have a : (shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F).map f.f ≫ η.app Y.obj
Tactic: rw [← Functor.comp_map F (shiftFunctor D (1 : S)), ← η.naturality f.f]
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
D : Type u'
inst_4 : Category.{v', u'} D
inst_5 : HasZeroMorphisms.{v', u'} D
inst_6 : HasShift.{v', u', u_1} D S
F : Functor.{v, v', u, u'} C D
η : shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F ⟶ F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1
hF : ∀ (c c' : C), Eq (α := F.obj c ⟶ F.obj c') (F.map 0) 0
X Y : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
⊢ (F.map X.d ≫ η.app X.obj) ≫ map (shiftFunctor.{v', u', u_1} D (A := S) 1) (F.map f.f) =
    F.map f.f ≫ F.map Y.d ≫ η.app Y.obj
have slice_lhs : F.map X.d ≫ (shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F).map f.f ≫ η.app Y.obj = F.map f.f ≫ F.map Y.d ≫ η.app Y.obj
Tactic: slice_lhs 2 3 => rw [← Functor.comp_map F (shiftFunctor D (1 : S)), ← η.naturality f.f]
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
D : Type u'
inst_4 : Category.{v', u'} D
inst_5 : HasZeroMorphisms.{v', u'} D
inst_6 : HasShift.{v', u', u_1} D S
F : Functor.{v, v', u, u'} C D
η : shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F ⟶ F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1
hF : ∀ (c c' : C), Eq (α := F.obj c ⟶ F.obj c') (F.map 0) 0
X Y : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
| F.map X.d ≫ (shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F).map f.f
have a : F.map f.f ≫ F.map Y.d
Tactic: rw [Functor.comp_map, ← F.map_comp, f.comm, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
D : Type u'
inst_4 : Category.{v', u'} D
inst_5 : HasZeroMorphisms.{v', u'} D
inst_6 : HasShift.{v', u', u_1} D S
F : Functor.{v, v', u, u'} C D
η : shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F ⟶ F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1
hF : ∀ (c c' : C), Eq (α := F.obj c ⟶ F.obj c') (F.map 0) 0
X Y : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
⊢ F.map X.d ≫ (shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F).map f.f ≫ η.app Y.obj = F.map f.f ≫ F.map Y.d ≫ η.app Y.obj
have slice_lhs : (F.map f.f ≫ F.map Y.d) ≫ η.app Y.obj = F.map f.f ≫ F.map Y.d ≫ η.app Y.obj
Tactic: slice_lhs 1 2 => rw [Functor.comp_map, ← F.map_comp, f.comm, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
D : Type u'
inst_4 : Category.{v', u'} D
inst_5 : HasZeroMorphisms.{v', u'} D
inst_6 : HasShift.{v', u', u_1} D S
F : Functor.{v, v', u, u'} C D
η : shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F ⟶ F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1
hF : ∀ (c c' : C), Eq (α := F.obj c ⟶ F.obj c') (F.map 0) 0
X Y : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
⊢ (F.map f.f ≫ F.map Y.d) ≫ η.app Y.obj = F.map f.f ≫ F.map Y.d ≫ η.app Y.obj
have rw : F.map f.f ≫ F.map Y.d ≫ η.app Y.obj = F.map f.f ≫ F.map Y.d ≫ η.app Y.obj
Tactic: rw [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
D : Type u'
inst_4 : Category.{v', u'} D
inst_5 : HasZeroMorphisms.{v', u'} D
inst_6 : HasShift.{v', u', u_1} D S
F : Functor.{v, v', u, u'} C D
η : shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F ⟶ F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1
hF : ∀ (c c' : C), Eq (α := F.obj c ⟶ F.obj c') (F.map 0) 0
X : DifferentialObject.{v, u, u_1} S C
⊢ { f := F.map (DifferentialObject.Hom.f (𝟙 X)), comm := ⋯ } =
    𝟙 { obj := F.obj X.obj, d := F.map X.d ≫ η.app X.obj, d_squared := ⋯ : DifferentialObject.{v', u', u_1} S D }
have w : autoParam
  (DifferentialObject.Hom.f { f := F.map (DifferentialObject.Hom.f (𝟙 X)), comm := sorry } =
    DifferentialObject.Hom.f
      (𝟙 { obj := F.obj X.obj, d := F.map X.d ≫ η.app X.obj, d_squared := sorry : DifferentialObject.{v', u', u_1} S D }))
  DifferentialObject.ext._auto_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddMonoidWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
D : Type u'
inst_4 : Category.{v', u'} D
inst_5 : HasZeroMorphisms.{v', u'} D
inst_6 : HasShift.{v', u', u_1} D S
F : Functor.{v, v', u, u'} C D
η : shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F ⟶ F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1
hF : ∀ (c c' : C), Eq (α := F.obj c ⟶ F.obj c') (F.map 0) 0
X Y Z : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v' + 1} (α :=
    { obj := F.obj X.obj, d := F.map X.d ≫ η.app X.obj, d_squared := ⋯ : DifferentialObject.{v', u', u_1} S D } ⟶
      { obj := F.obj Z.obj, d := F.map Z.d ≫ η.app Z.obj, d_squared := ⋯ })
    { f := F.map (f ≫ g).f, comm := ⋯ }
    (CategoryStruct.comp (Y := { obj := F.obj Y.obj, d := F.map Y.d ≫ η.app Y.obj, d_squared := ⋯ })
      { f := F.map f.f, comm := ⋯ } { f := F.map g.f, comm := ⋯ })
have w : autoParam
  (Eq.{v' + 1} (α :=
    { obj := F.obj X.obj, d := F.map X.d ≫ η.app X.obj, d_squared := sorry : DifferentialObject.{v', u', u_1} S D }.obj ⟶
      { obj := F.obj Z.obj, d := F.map Z.d ≫ η.app Z.obj, d_squared := sorry : DifferentialObject.{v', u', u_1} S D }.obj)
    (DifferentialObject.Hom.f { f := F.map (f ≫ g).f, comm := sorry })
    (DifferentialObject.Hom.f
      (CategoryStruct.comp (Y := { obj := F.obj Y.obj, d := F.map Y.d ≫ η.app Y.obj, d_squared := sorry })
        { f := F.map f.f, comm := sorry } { f := F.map g.f, comm := sorry })))
  DifferentialObject.ext._auto_1
Tactic: ext