awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
W X Y Z : Dial.{v, u} C
⊢ Hom.f
      ((Iso.hom (α_ W X Y) ⊗ₘ 𝟙 Z) ≫
        Iso.hom (α_ W (tensorObj (𝒞 := instCategory) X Y) Z) ≫ (𝟙 W ⊗ₘ Iso.hom (α_ X Y Z))) =
    (Iso.hom (α_ (tensorObj (𝒞 := instCategory) W X) Y Z) ≫ Iso.hom (α_ W X (tensorObj (𝒞 := instCategory) Y Z))).f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
W X Y Z : Dial.{v, u} C
⊢ Hom.F
      ((Iso.hom (α_ W X Y) ⊗ₘ 𝟙 Z) ≫
        Iso.hom (α_ W (tensorObj (𝒞 := instCategory) X Y) Z) ≫ (𝟙 W ⊗ₘ Iso.hom (α_ X Y Z))) =
    (Iso.hom (α_ (tensorObj (𝒞 := instCategory) W X) Y Z) ≫ Iso.hom (α_ W X (tensorObj (𝒞 := instCategory) Y Z))).F

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Dialectica.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y : Dial.{v, u} C
⊢ (tensorObj (𝒞 := instCategory) X Y).rel =
    Functor.obj
      (Subobject.pullback (prod.map (Iso.hom (prod.braiding X.src Y.src)) (Iso.hom (prod.braiding X.tgt Y.tgt))))
      (tensorObj (𝒞 := instCategory) Y X).rel

Tactic:
simp [Subobject.inf_pullback, ← Subobject.pullback_comp, inf_comm]

Premises used: inf_comm, CategoryTheory.Subobject.pullback_comp, CategoryTheory.Subobject.inf_pullback
-- Module: Mathlib.CategoryTheory.DifferentialObject
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
A B : DifferentialObject.{v, u, u_1} S C
f g : A ⟶ B
w : f.f = g.f
⊢ f = g

Tactic:
Hom.ext w

Premises used: CategoryTheory.DifferentialObject.Hom.ext
-- Module: Mathlib.CategoryTheory.DifferentialObject
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 : DifferentialObject.{v, u, u_1} S C
⊢ Hom.f (𝟙 X) = 𝟙 X.obj

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.DifferentialObject
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 Z : DifferentialObject.{v, u, u_1} S C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).f = f.f ≫ g.f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.DifferentialObject
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
h : X = Y
subst : Hom.f (eqToHom ⋯) = eqToHom ⋯
⊢ Hom.f (eqToHom h) = eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.DifferentialObject
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 : DifferentialObject.{v, u, u_1} S C
rw : Hom.f (𝟙 X) = 𝟙 X.obj
⊢ Hom.f (eqToHom ⋯) = eqToHom ⋯

Tactic:
rw [eqToHom_refl, eqToHom_refl]

Premises used: CategoryTheory.eqToHom_refl
-- Module: Mathlib.CategoryTheory.DifferentialObject
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 : DifferentialObject.{v, u, u_1} S C
⊢ Hom.f (𝟙 X) = 𝟙 X.obj

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.DifferentialObject
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
inst_4 : Functor.PreservesZeroMorphisms.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := S) 1)
P Q : DifferentialObject.{v, u, u_1} S C
⊢ Eq.{v + 1} (α := P.obj ⟶ Q.obj) (Hom.f 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.DifferentialObject
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 ≅ Y
rw : (f.hom ≫ f.inv).f = 𝟙 X.obj
rw₁ : Hom.f (𝟙 X) = 𝟙 X.obj
rw₂ rw₃ : Eq.{v + 1} (α := X.obj ⟶ X.obj) (𝟙 X.obj) (𝟙 X.obj)
⊢ f.hom.f ≫ f.inv.f = 𝟙 X.obj

Tactic:
rw [← comp_f, Iso.hom_inv_id, id_f]

Premises used: CategoryTheory.DifferentialObject.comp_f, CategoryTheory.Iso.hom_inv_id, CategoryTheory.DifferentialObject.id_f
-- Module: Mathlib.CategoryTheory.DifferentialObject
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 ≅ Y
rw : (f.inv ≫ f.hom).f = 𝟙 Y.obj
rw₁ : Hom.f (𝟙 Y) = 𝟙 Y.obj
rw₂ rw₃ : Eq.{v + 1} (α := Y.obj ⟶ Y.obj) (𝟙 Y.obj) (𝟙 Y.obj)
⊢ f.inv.f ≫ f.hom.f = 𝟙 Y.obj

Tactic:
rw [← comp_f, Iso.inv_hom_id, id_f]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.DifferentialObject.comp_f, CategoryTheory.DifferentialObject.id_f
-- Module: Mathlib.CategoryTheory.DifferentialObject
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 : DifferentialObject.{v, u, u_1} S C
⊢ isoApp (Iso.refl X) = Iso.refl X.obj

Tactic:
rfl

Premises used: CategoryTheory.Iso.refl, CategoryTheory.DifferentialObject.isoApp, rfl
-- Module: Mathlib.CategoryTheory.DifferentialObject
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 ≅ Y
⊢ isoApp f.symm = (isoApp f).symm

Tactic:
rfl

Premises used: CategoryTheory.DifferentialObject.isoApp, CategoryTheory.Iso.symm, rfl
-- Module: Mathlib.CategoryTheory.DifferentialObject
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 Z : DifferentialObject.{v, u, u_1} S C
f : X ≅ Y
g : Y ≅ Z
⊢ isoApp (f ≪≫ g) = isoApp f ≪≫ isoApp g

Tactic:
rfl

Premises used: CategoryTheory.DifferentialObject.isoApp, CategoryTheory.Iso.trans, rfl
-- Module: Mathlib.CategoryTheory.DifferentialObject
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
rw₅ rw₆ : f.hom ≫ Y.d = f.hom ≫ Y.d
⊢ Y.d ≫ Functor.map (shiftFunctor.{v, u, u_1} C (A := S) 1) f.inv = f.inv ≫ X.d

Tactic:
rw [← Functor.mapIso_inv, Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp, Functor.mapIso_hom,
      hf]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Functor.mapIso_inv, CategoryTheory.Iso.eq_inv_comp, CategoryTheory.Functor.mapIso_hom
-- Module: Mathlib.CategoryTheory.DifferentialObject
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
w : autoParam (Hom.f ({ f := f.hom, comm := hf : X.Hom Y } ≫ { f := f.inv, comm := ⋯ }) = Hom.f (𝟙 X)) ext._auto_1
⊢ { f := f.hom, comm := hf : X.Hom Y } ≫ { f := f.inv, comm := ⋯ } = 𝟙 X

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.DifferentialObject
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
w : autoParam (f.hom ≫ f.inv = 𝟙 X.obj) ext._auto_1
⊢ autoParam (Hom.f ({ f := f.hom, comm := hf : X.Hom Y } ≫ { f := f.inv, comm := ⋯ }) = Hom.f (𝟙 X)) ext._auto_1

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.DifferentialObject
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 (f.hom ≫ f.inv = 𝟙 X.obj) ext._auto_1

Tactic:
f.hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.CategoryTheory.DifferentialObject
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 (f.hom ≫ f.inv = 𝟙 X.obj) ext._auto_1

Tactic:
exact f.hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.CategoryTheory.DifferentialObject
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
w : autoParam (Hom.f ({ f := f.inv, comm := ⋯ : Y.Hom X } ≫ { f := f.hom, comm := hf }) = Hom.f (𝟙 Y)) ext._auto_1
⊢ { f := f.inv, comm := ⋯ : Y.Hom X } ≫ { f := f.hom, comm := hf } = 𝟙 Y

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.DifferentialObject
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
w : autoParam (f.inv ≫ f.hom = 𝟙 Y.obj) ext._auto_1
⊢ autoParam (Hom.f ({ f := f.inv, comm := ⋯ : Y.Hom X } ≫ { f := f.hom, comm := hf }) = Hom.f (𝟙 Y)) ext._auto_1

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.DifferentialObject
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 (f.inv ≫ f.hom = 𝟙 Y.obj) ext._auto_1

Tactic:
f.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id
-- Module: Mathlib.CategoryTheory.DifferentialObject
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 (f.inv ≫ f.hom = 𝟙 Y.obj) ext._auto_1

Tactic:
exact f.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id
-- Module: Mathlib.CategoryTheory.DifferentialObject
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 :
  (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
⊢ (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

Tactic:
rw [Functor.map_comp, ← Functor.comp_map F (shiftFunctor D (1 : S))]

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.Functor.map_comp, OfNat.ofNat, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.DifferentialObject
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
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)
| η.app X.obj ≫ (F ⋙ shiftFunctor.{v', u', u_1} D (A := S) 1).map X.d

Tactic:
rw [← η.naturality X.d]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.DifferentialObject.d
-- Module: Mathlib.CategoryTheory.DifferentialObject
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
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
⊢ (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:
slice_lhs 2 3 => rw [← η.naturality X.d]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.DifferentialObject.d
-- Module: Mathlib.CategoryTheory.DifferentialObject
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 :
  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
⊢ 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:
rw [Functor.comp_map]

Premises used: CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.DifferentialObject
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
a : 0
| F.map X.d ≫ F.map (map (shiftFunctor.{v, u, u_1} C (A := S) 1) X.d)

Tactic:
rw [← F.map_comp, X.d_squared, hF]

Premises used: CategoryTheory.DifferentialObject.d_squared, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.DifferentialObject
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
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
⊢ 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:
slice_lhs 1 2 => rw [← F.map_comp, X.d_squared, hF]

Premises used: CategoryTheory.DifferentialObject.d_squared, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.DifferentialObject
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
rw₁ 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
⊢ 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:
rw [zero_comp, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.DifferentialObject
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
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
⊢ { 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

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.DifferentialObject
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
a : (shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F).map f.f ≫ η.app Y.obj
| η.app X.obj ≫ map (shiftFunctor.{v', u', u_1} D (A := S) 1) (F.map f.f)

Tactic:
rw [← Functor.comp_map F (shiftFunctor D (1 : S)), ← η.naturality f.f]

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.DifferentialObject.Hom.f, CategoryTheory.NatTrans.naturality, OfNat.ofNat, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.DifferentialObject
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
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
⊢ (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:
slice_lhs 2 3 => rw [← Functor.comp_map F (shiftFunctor D (1 : S)), ← η.naturality f.f]

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.DifferentialObject.Hom.f, CategoryTheory.NatTrans.naturality, OfNat.ofNat, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.DifferentialObject
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
a : F.map f.f ≫ F.map Y.d
| F.map X.d ≫ (shiftFunctor.{v, u, u_1} C (A := S) 1 ⋙ F).map f.f

Tactic:
rw [Functor.comp_map, ← F.map_comp, f.comm, F.map_comp]

Premises used: CategoryTheory.DifferentialObject.Hom.comm, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.DifferentialObject
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
slice_lhs : (F.map f.f ≫ F.map Y.d) ≫ η.app Y.obj = F.map f.f ≫ F.map Y.d ≫ η.app Y.obj
⊢ 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 1 2 => rw [Functor.comp_map, ← F.map_comp, f.comm, F.map_comp]

Premises used: CategoryTheory.DifferentialObject.Hom.comm, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map