[GOAL]
S : Type u_1
inst✝³ : AddMonoidWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X Y : DifferentialObject S C
h : X = Y
⊢ (eqToHom h).f = eqToHom (_ : X.obj = Y.obj)
[PROOFSTEP]
subst h
[GOAL]
S : Type u_1
inst✝³ : AddMonoidWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X : DifferentialObject S C
⊢ (eqToHom (_ : X = X)).f = eqToHom (_ : X.obj = X.obj)
[PROOFSTEP]
rw [eqToHom_refl, eqToHom_refl]
[GOAL]
S : Type u_1
inst✝³ : AddMonoidWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X : DifferentialObject S C
⊢ (𝟙 X).f = 𝟙 X.obj
[PROOFSTEP]
rfl
[GOAL]
S : Type u_1
inst✝⁴ : AddMonoidWithOne S
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasShift C S
inst✝ : Functor.PreservesZeroMorphisms (shiftFunctor C 1)
X Y : DifferentialObject S C
f : X ≅ Y
⊢ f.hom.f ≫ f.inv.f = 𝟙 X.obj
[PROOFSTEP]
rw [← comp_f, Iso.hom_inv_id, id_f]
[GOAL]
S : Type u_1
inst✝⁴ : AddMonoidWithOne S
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasShift C S
inst✝ : Functor.PreservesZeroMorphisms (shiftFunctor C 1)
X Y : DifferentialObject S C
f : X ≅ Y
⊢ f.inv.f ≫ f.hom.f = 𝟙 Y.obj
[PROOFSTEP]
rw [← comp_f, Iso.inv_hom_id, id_f]
[GOAL]
S : Type u_1
inst✝⁴ : AddMonoidWithOne S
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasShift C S
inst✝ : Functor.PreservesZeroMorphisms (shiftFunctor C 1)
X Y : DifferentialObject S C
f : X.obj ≅ Y.obj
hf : X.d ≫ (shiftFunctor C 1).map f.hom = f.hom ≫ Y.d
⊢ Y.d ≫ (shiftFunctor C 1).map f.inv = f.inv ≫ X.d
[PROOFSTEP]
rw [← Functor.mapIso_inv, Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp, Functor.mapIso_hom, hf]
[GOAL]
S : Type u_1
inst✝⁴ : AddMonoidWithOne S
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasShift C S
inst✝ : Functor.PreservesZeroMorphisms (shiftFunctor C 1)
X Y : DifferentialObject S C
f : X.obj ≅ Y.obj
hf : X.d ≫ (shiftFunctor C 1).map f.hom = f.hom ≫ Y.d
⊢ Hom.mk f.hom ≫ Hom.mk f.inv = 𝟙 X
[PROOFSTEP]
ext1
[GOAL]
case w
S : Type u_1
inst✝⁴ : AddMonoidWithOne S
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasShift C S
inst✝ : Functor.PreservesZeroMorphisms (shiftFunctor C 1)
X Y : DifferentialObject S C
f : X.obj ≅ Y.obj
hf : X.d ≫ (shiftFunctor C 1).map f.hom = f.hom ≫ Y.d
⊢ autoParam ((Hom.mk f.hom ≫ Hom.mk f.inv).f = (𝟙 X).f) _auto✝
[PROOFSTEP]
dsimp
[GOAL]
case w
S : Type u_1
inst✝⁴ : AddMonoidWithOne S
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasShift C S
inst✝ : Functor.PreservesZeroMorphisms (shiftFunctor C 1)
X Y : DifferentialObject S C
f : X.obj ≅ Y.obj
hf : X.d ≫ (shiftFunctor C 1).map f.hom = f.hom ≫ Y.d
⊢ autoParam (f.hom ≫ f.inv = 𝟙 X.obj) _auto✝
[PROOFSTEP]
exact f.hom_inv_id
[GOAL]
S : Type u_1
inst✝⁴ : AddMonoidWithOne S
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasShift C S
inst✝ : Functor.PreservesZeroMorphisms (shiftFunctor C 1)
X Y : DifferentialObject S C
f : X.obj ≅ Y.obj
hf : X.d ≫ (shiftFunctor C 1).map f.hom = f.hom ≫ Y.d
⊢ Hom.mk f.inv ≫ Hom.mk f.hom = 𝟙 Y
[PROOFSTEP]
ext1
[GOAL]
case w
S : Type u_1
inst✝⁴ : AddMonoidWithOne S
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasShift C S
inst✝ : Functor.PreservesZeroMorphisms (shiftFunctor C 1)
X Y : DifferentialObject S C
f : X.obj ≅ Y.obj
hf : X.d ≫ (shiftFunctor C 1).map f.hom = f.hom ≫ Y.d
⊢ autoParam ((Hom.mk f.inv ≫ Hom.mk f.hom).f = (𝟙 Y).f) _auto✝
[PROOFSTEP]
dsimp
[GOAL]
case w
S : Type u_1
inst✝⁴ : AddMonoidWithOne S
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasShift C S
inst✝ : Functor.PreservesZeroMorphisms (shiftFunctor C 1)
X Y : DifferentialObject S C
f : X.obj ≅ Y.obj
hf : X.d ≫ (shiftFunctor C 1).map f.hom = f.hom ≫ Y.d
⊢ autoParam (f.inv ≫ f.hom = 𝟙 Y.obj) _auto✝
[PROOFSTEP]
exact f.inv_hom_id
[GOAL]
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
⊢ (F.map X.d ≫ NatTrans.app η X.obj) ≫ (shiftFunctor D 1).map (F.map X.d ≫ NatTrans.app η X.obj) = 0
[PROOFSTEP]
rw [Functor.map_comp, ← Functor.comp_map F (shiftFunctor D (1 : S))]
[GOAL]
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
⊢ (F.map X.d ≫ NatTrans.app η X.obj) ≫ (F ⋙ shiftFunctor D 1).map X.d ≫ (shiftFunctor D 1).map (NatTrans.app η X.obj) =
    0
[PROOFSTEP]
slice_lhs 2 3 => rw [← η.naturality X.d]
[GOAL]
case a.a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
| NatTrans.app η X.obj ≫ (F ⋙ shiftFunctor D 1).map X.d
case a.a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
| (shiftFunctor D 1).map (NatTrans.app η X.obj)
case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
| F.map X.d
[PROOFSTEP]
rw [← η.naturality X.d]
[GOAL]
case a.a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
| NatTrans.app η X.obj ≫ (F ⋙ shiftFunctor D 1).map X.d
case a.a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
| (shiftFunctor D 1).map (NatTrans.app η X.obj)
case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
| F.map X.d
[PROOFSTEP]
rw [← η.naturality X.d]
[GOAL]
case a.a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
| NatTrans.app η X.obj ≫ (F ⋙ shiftFunctor D 1).map X.d
case a.a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
| (shiftFunctor D 1).map (NatTrans.app η X.obj)
case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
| F.map X.d
[PROOFSTEP]
rw [← η.naturality X.d]
[GOAL]
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
⊢ F.map X.d ≫
      ((shiftFunctor C 1 ⋙ F).map X.d ≫ NatTrans.app η ((shiftFunctor C 1).obj X.obj)) ≫
        (shiftFunctor D 1).map (NatTrans.app η X.obj) =
    0
[PROOFSTEP]
rw [Functor.comp_map]
[GOAL]
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
⊢ F.map X.d ≫
      (F.map ((shiftFunctor C 1).map X.d) ≫ NatTrans.app η ((shiftFunctor C 1).obj X.obj)) ≫
        (shiftFunctor D 1).map (NatTrans.app η X.obj) =
    0
[PROOFSTEP]
slice_lhs 1 2 => rw [← F.map_comp, X.d_squared, hF]
[GOAL]
case a.a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
| F.map X.d ≫ F.map ((shiftFunctor C 1).map X.d)
case a.a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
| NatTrans.app η ((shiftFunctor C 1).obj X.obj)
case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
| (shiftFunctor D 1).map (NatTrans.app η X.obj)
[PROOFSTEP]
rw [← F.map_comp, X.d_squared, hF]
[GOAL]
case a.a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
| F.map X.d ≫ F.map ((shiftFunctor C 1).map X.d)
case a.a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
| NatTrans.app η ((shiftFunctor C 1).obj X.obj)
case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
| (shiftFunctor D 1).map (NatTrans.app η X.obj)
[PROOFSTEP]
rw [← F.map_comp, X.d_squared, hF]
[GOAL]
case a.a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
| F.map X.d ≫ F.map ((shiftFunctor C 1).map X.d)
case a.a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
| NatTrans.app η ((shiftFunctor C 1).obj X.obj)
case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
| (shiftFunctor D 1).map (NatTrans.app η X.obj)
[PROOFSTEP]
rw [← F.map_comp, X.d_squared, hF]
[GOAL]
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
⊢ (0 ≫ NatTrans.app η ((shiftFunctor C 1).obj X.obj)) ≫ (shiftFunctor D 1).map (NatTrans.app η X.obj) = 0
[PROOFSTEP]
rw [zero_comp, zero_comp]
[GOAL]
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ ((fun X => DifferentialObject.mk (F.obj X.obj) (F.map X.d ≫ NatTrans.app η X.obj)) X✝).d ≫
      (shiftFunctor D 1).map (F.map f.f) =
    F.map f.f ≫ ((fun X => DifferentialObject.mk (F.obj X.obj) (F.map X.d ≫ NatTrans.app η X.obj)) Y✝).d
[PROOFSTEP]
dsimp
[GOAL]
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ (F.map X✝.d ≫ NatTrans.app η X✝.obj) ≫ (shiftFunctor D 1).map (F.map f.f) =
    F.map f.f ≫ F.map Y✝.d ≫ NatTrans.app η Y✝.obj
[PROOFSTEP]
slice_lhs 2 3 => rw [← Functor.comp_map F (shiftFunctor D (1 : S)), ← η.naturality f.f]
[GOAL]
case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
| NatTrans.app η X✝.obj ≫ (shiftFunctor D 1).map (F.map f.f)
case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
| F.map X✝.d
[PROOFSTEP]
rw [← Functor.comp_map F (shiftFunctor D (1 : S)), ← η.naturality f.f]
[GOAL]
case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
| NatTrans.app η X✝.obj ≫ (shiftFunctor D 1).map (F.map f.f)
case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
| F.map X✝.d
[PROOFSTEP]
rw [← Functor.comp_map F (shiftFunctor D (1 : S)), ← η.naturality f.f]
[GOAL]
case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
| NatTrans.app η X✝.obj ≫ (shiftFunctor D 1).map (F.map f.f)
case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
| F.map X✝.d
[PROOFSTEP]
rw [← Functor.comp_map F (shiftFunctor D (1 : S)), ← η.naturality f.f]
[GOAL]
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ F.map X✝.d ≫ (shiftFunctor C 1 ⋙ F).map f.f ≫ NatTrans.app η Y✝.obj = F.map f.f ≫ F.map Y✝.d ≫ NatTrans.app η Y✝.obj
[PROOFSTEP]
slice_lhs 1 2 => rw [Functor.comp_map, ← F.map_comp, f.comm, F.map_comp]
[GOAL]
case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
| F.map X✝.d ≫ (shiftFunctor C 1 ⋙ F).map f.f
case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
| NatTrans.app η Y✝.obj
[PROOFSTEP]
rw [Functor.comp_map, ← F.map_comp, f.comm, F.map_comp]
[GOAL]
case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
| F.map X✝.d ≫ (shiftFunctor C 1 ⋙ F).map f.f
case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
| NatTrans.app η Y✝.obj
[PROOFSTEP]
rw [Functor.comp_map, ← F.map_comp, f.comm, F.map_comp]
[GOAL]
case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
| F.map X✝.d ≫ (shiftFunctor C 1 ⋙ F).map f.f
case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
| NatTrans.app η Y✝.obj
[PROOFSTEP]
rw [Functor.comp_map, ← F.map_comp, f.comm, F.map_comp]
[GOAL]
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ (F.map f.f ≫ F.map Y✝.d) ≫ NatTrans.app η Y✝.obj = F.map f.f ≫ F.map Y✝.d ≫ NatTrans.app η Y✝.obj
[PROOFSTEP]
rw [Category.assoc]
[GOAL]
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
⊢ ∀ (X : DifferentialObject S C),
    { obj := fun X => DifferentialObject.mk (F.obj X.obj) (F.map X.d ≫ NatTrans.app η X.obj),
            map := fun {X Y} f => DifferentialObject.Hom.mk (F.map f.f) }.map
        (𝟙 X) =
      𝟙
        ({ obj := fun X => DifferentialObject.mk (F.obj X.obj) (F.map X.d ≫ NatTrans.app η X.obj),
              map := fun {X Y} f => DifferentialObject.Hom.mk (F.map f.f) }.obj
          X)
[PROOFSTEP]
intros
[GOAL]
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ : DifferentialObject S C
⊢ { obj := fun X => DifferentialObject.mk (F.obj X.obj) (F.map X.d ≫ NatTrans.app η X.obj),
          map := fun {X Y} f => DifferentialObject.Hom.mk (F.map f.f) }.map
      (𝟙 X✝) =
    𝟙
      ({ obj := fun X => DifferentialObject.mk (F.obj X.obj) (F.map X.d ≫ NatTrans.app η X.obj),
            map := fun {X Y} f => DifferentialObject.Hom.mk (F.map f.f) }.obj
        X✝)
[PROOFSTEP]
ext
[GOAL]
case w
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ : DifferentialObject S C
⊢ autoParam
    (({ obj := fun X => DifferentialObject.mk (F.obj X.obj) (F.map X.d ≫ NatTrans.app η X.obj),
              map := fun {X Y} f => DifferentialObject.Hom.mk (F.map f.f) }.map
          (𝟙 X✝)).f =
      (𝟙
          ({ obj := fun X => DifferentialObject.mk (F.obj X.obj) (F.map X.d ≫ NatTrans.app η X.obj),
                map := fun {X Y} f => DifferentialObject.Hom.mk (F.map f.f) }.obj
            X✝)).f)
    _auto✝
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
⊢ ∀ {X Y Z : DifferentialObject S C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := fun X => DifferentialObject.mk (F.obj X.obj) (F.map X.d ≫ NatTrans.app η X.obj),
            map := fun {X Y} f => DifferentialObject.Hom.mk (F.map f.f) }.map
        (f ≫ g) =
      { obj := fun X => DifferentialObject.mk (F.obj X.obj) (F.map X.d ≫ NatTrans.app η X.obj),
              map := fun {X Y} f => DifferentialObject.Hom.mk (F.map f.f) }.map
          f ≫
        { obj := fun X => DifferentialObject.mk (F.obj X.obj) (F.map X.d ≫ NatTrans.app η X.obj),
              map := fun {X Y} f => DifferentialObject.Hom.mk (F.map f.f) }.map
          g
[PROOFSTEP]
intros
[GOAL]
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ Z✝ : DifferentialObject S C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { obj := fun X => DifferentialObject.mk (F.obj X.obj) (F.map X.d ≫ NatTrans.app η X.obj),
          map := fun {X Y} f => DifferentialObject.Hom.mk (F.map f.f) }.map
      (f✝ ≫ g✝) =
    { obj := fun X => DifferentialObject.mk (F.obj X.obj) (F.map X.d ≫ NatTrans.app η X.obj),
            map := fun {X Y} f => DifferentialObject.Hom.mk (F.map f.f) }.map
        f✝ ≫
      { obj := fun X => DifferentialObject.mk (F.obj X.obj) (F.map X.d ≫ NatTrans.app η X.obj),
            map := fun {X Y} f => DifferentialObject.Hom.mk (F.map f.f) }.map
        g✝
[PROOFSTEP]
ext
[GOAL]
case w
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ Z✝ : DifferentialObject S C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ autoParam
    (({ obj := fun X => DifferentialObject.mk (F.obj X.obj) (F.map X.d ≫ NatTrans.app η X.obj),
              map := fun {X Y} f => DifferentialObject.Hom.mk (F.map f.f) }.map
          (f✝ ≫ g✝)).f =
      ({ obj := fun X => DifferentialObject.mk (F.obj X.obj) (F.map X.d ≫ NatTrans.app η X.obj),
                map := fun {X Y} f => DifferentialObject.Hom.mk (F.map f.f) }.map
            f✝ ≫
          { obj := fun X => DifferentialObject.mk (F.obj X.obj) (F.map X.d ≫ NatTrans.app η X.obj),
                map := fun {X Y} f => DifferentialObject.Hom.mk (F.map f.f) }.map
            g✝).f)
    _auto✝
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
inst✝⁵ : AddMonoidWithOne S
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasShift C S
inst✝ : Functor.PreservesZeroMorphisms (shiftFunctor C 1)
⊢ HasZeroObject (DifferentialObject S C)
[PROOFSTEP]
refine'
  ⟨⟨⟨0, 0, by aesop_cat⟩, fun X => ⟨⟨⟨⟨0, by aesop_cat⟩⟩, fun f => _⟩⟩, fun X => ⟨⟨⟨⟨0, by aesop_cat⟩⟩, fun f => _⟩⟩⟩⟩
[GOAL]
S : Type u_1
inst✝⁵ : AddMonoidWithOne S
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasShift C S
inst✝ : Functor.PreservesZeroMorphisms (shiftFunctor C 1)
⊢ 0 ≫ (shiftFunctor C 1).map 0 = 0
[PROOFSTEP]
aesop_cat
[GOAL]
S : Type u_1
inst✝⁵ : AddMonoidWithOne S
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasShift C S
inst✝ : Functor.PreservesZeroMorphisms (shiftFunctor C 1)
X : DifferentialObject S C
⊢ (mk 0 0).d ≫ (shiftFunctor C 1).map 0 = 0 ≫ X.d
[PROOFSTEP]
aesop_cat
[GOAL]
S : Type u_1
inst✝⁵ : AddMonoidWithOne S
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasShift C S
inst✝ : Functor.PreservesZeroMorphisms (shiftFunctor C 1)
X : DifferentialObject S C
⊢ X.d ≫ (shiftFunctor C 1).map 0 = 0 ≫ (mk 0 0).d
[PROOFSTEP]
aesop_cat
[GOAL]
case refine'_1
S : Type u_1
inst✝⁵ : AddMonoidWithOne S
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasShift C S
inst✝ : Functor.PreservesZeroMorphisms (shiftFunctor C 1)
X : DifferentialObject S C
f : mk 0 0 ⟶ X
⊢ f = default
[PROOFSTEP]
ext
[GOAL]
case refine'_2
S : Type u_1
inst✝⁵ : AddMonoidWithOne S
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasShift C S
inst✝ : Functor.PreservesZeroMorphisms (shiftFunctor C 1)
X : DifferentialObject S C
f : X ⟶ mk 0 0
⊢ f = default
[PROOFSTEP]
ext
[GOAL]
case refine'_1.w
S : Type u_1
inst✝⁵ : AddMonoidWithOne S
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasShift C S
inst✝ : Functor.PreservesZeroMorphisms (shiftFunctor C 1)
X : DifferentialObject S C
f : mk 0 0 ⟶ X
⊢ autoParam (f.f = default.f) _auto✝
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
case refine'_2.w
S : Type u_1
inst✝⁵ : AddMonoidWithOne S
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasShift C S
inst✝ : Functor.PreservesZeroMorphisms (shiftFunctor C 1)
X : DifferentialObject S C
f : X ⟶ mk 0 0
⊢ autoParam (f.f = default.f) _auto✝
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
⊢ ((CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom) ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom) =
    0
[PROOFSTEP]
rw [Functor.map_comp, Category.assoc, shiftComm_hom_comp_assoc, ← Functor.map_comp_assoc, X.d_squared, Functor.map_zero,
  zero_comp]
[GOAL]
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ ((fun X =>
            mk ((CategoryTheory.shiftFunctor C n).obj X.obj)
              ((CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom))
          X✝).d ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map f.f) =
    (CategoryTheory.shiftFunctor C n).map f.f ≫
      ((fun X =>
            mk ((CategoryTheory.shiftFunctor C n).obj X.obj)
              ((CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom))
          Y✝).d
[PROOFSTEP]
dsimp
[GOAL]
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ ((CategoryTheory.shiftFunctor C n).map X✝.d ≫ NatTrans.app (shiftFunctorComm C 1 n).hom X✝.obj) ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map f.f) =
    (CategoryTheory.shiftFunctor C n).map f.f ≫
      (CategoryTheory.shiftFunctor C n).map Y✝.d ≫ NatTrans.app (shiftFunctorComm C 1 n).hom Y✝.obj
[PROOFSTEP]
erw [Category.assoc, shiftComm_hom_comp, ← Functor.map_comp_assoc, f.comm, Functor.map_comp_assoc]
[GOAL]
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ (CategoryTheory.shiftFunctor C n).map f.f ≫ (CategoryTheory.shiftFunctor C n).map Y✝.d ≫ (shiftComm Y✝.obj 1 n).hom =
    (CategoryTheory.shiftFunctor C n).map f.f ≫
      (CategoryTheory.shiftFunctor C n).map Y✝.d ≫ NatTrans.app (shiftFunctorComm C 1 n).hom Y✝.obj
[PROOFSTEP]
rfl
[GOAL]
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
⊢ {
          obj := fun X =>
            mk ((CategoryTheory.shiftFunctor C n).obj X.obj)
              ((CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom),
          map := fun {X Y} f => Hom.mk ((CategoryTheory.shiftFunctor C n).map f.f) }.map
      (𝟙 X) =
    𝟙
      ({
            obj := fun X =>
              mk ((CategoryTheory.shiftFunctor C n).obj X.obj)
                ((CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom),
            map := fun {X Y} f => Hom.mk ((CategoryTheory.shiftFunctor C n).map f.f) }.obj
        X)
[PROOFSTEP]
ext1
[GOAL]
case w
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
⊢ autoParam
    (({
              obj := fun X =>
                mk ((CategoryTheory.shiftFunctor C n).obj X.obj)
                  ((CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom),
              map := fun {X Y} f => Hom.mk ((CategoryTheory.shiftFunctor C n).map f.f) }.map
          (𝟙 X)).f =
      (𝟙
          ({
                obj := fun X =>
                  mk ((CategoryTheory.shiftFunctor C n).obj X.obj)
                    ((CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom),
                map := fun {X Y} f => Hom.mk ((CategoryTheory.shiftFunctor C n).map f.f) }.obj
            X)).f)
    _auto✝
[PROOFSTEP]
dsimp
[GOAL]
case w
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
⊢ autoParam ((CategoryTheory.shiftFunctor C n).map (𝟙 X.obj) = 𝟙 ((CategoryTheory.shiftFunctor C n).obj X.obj)) _auto✝
[PROOFSTEP]
rw [Functor.map_id]
[GOAL]
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X✝ Y✝ Z✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ {
          obj := fun X =>
            mk ((CategoryTheory.shiftFunctor C n).obj X.obj)
              ((CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom),
          map := fun {X Y} f => Hom.mk ((CategoryTheory.shiftFunctor C n).map f.f) }.map
      (f ≫ g) =
    {
            obj := fun X =>
              mk ((CategoryTheory.shiftFunctor C n).obj X.obj)
                ((CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom),
            map := fun {X Y} f => Hom.mk ((CategoryTheory.shiftFunctor C n).map f.f) }.map
        f ≫
      {
            obj := fun X =>
              mk ((CategoryTheory.shiftFunctor C n).obj X.obj)
                ((CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom),
            map := fun {X Y} f => Hom.mk ((CategoryTheory.shiftFunctor C n).map f.f) }.map
        g
[PROOFSTEP]
ext1
[GOAL]
case w
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X✝ Y✝ Z✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ autoParam
    (({
              obj := fun X =>
                mk ((CategoryTheory.shiftFunctor C n).obj X.obj)
                  ((CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom),
              map := fun {X Y} f => Hom.mk ((CategoryTheory.shiftFunctor C n).map f.f) }.map
          (f ≫ g)).f =
      ({
                obj := fun X =>
                  mk ((CategoryTheory.shiftFunctor C n).obj X.obj)
                    ((CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom),
                map := fun {X Y} f => Hom.mk ((CategoryTheory.shiftFunctor C n).map f.f) }.map
            f ≫
          {
                obj := fun X =>
                  mk ((CategoryTheory.shiftFunctor C n).obj X.obj)
                    ((CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom),
                map := fun {X Y} f => Hom.mk ((CategoryTheory.shiftFunctor C n).map f.f) }.map
            g).f)
    _auto✝
[PROOFSTEP]
dsimp
[GOAL]
case w
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X✝ Y✝ Z✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ autoParam
    ((CategoryTheory.shiftFunctor C n).map (f.f ≫ g.f) =
      (CategoryTheory.shiftFunctor C n).map f.f ≫ (CategoryTheory.shiftFunctor C n).map g.f)
    _auto✝
[PROOFSTEP]
rw [Functor.map_comp]
[GOAL]
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
⊢ shiftFunctor C (m + n) ≅ shiftFunctor C m ⋙ shiftFunctor C n
[PROOFSTEP]
refine' NatIso.ofComponents (fun X => mkIso (shiftAdd X.obj _ _) _) (fun f => _)
[GOAL]
case refine'_1
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X : DifferentialObject S C
⊢ ((shiftFunctor C (m + n)).obj X).d ≫ (CategoryTheory.shiftFunctor C 1).map (shiftAdd X.obj m n).hom =
    (shiftAdd X.obj m n).hom ≫ ((shiftFunctor C m ⋙ shiftFunctor C n).obj X).d
[PROOFSTEP]
dsimp
[GOAL]
case refine'_1
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X : DifferentialObject S C
⊢ ((CategoryTheory.shiftFunctor C (m + n)).map X.d ≫ NatTrans.app (shiftFunctorComm C 1 (m + n)).hom X.obj) ≫
      (CategoryTheory.shiftFunctor C 1).map (NatTrans.app (CategoryTheory.shiftFunctorAdd C m n).hom X.obj) =
    NatTrans.app (CategoryTheory.shiftFunctorAdd C m n).hom X.obj ≫
      (CategoryTheory.shiftFunctor C n).map
          ((CategoryTheory.shiftFunctor C m).map X.d ≫ NatTrans.app (shiftFunctorComm C 1 m).hom X.obj) ≫
        NatTrans.app (shiftFunctorComm C 1 n).hom ((CategoryTheory.shiftFunctor C m).obj X.obj)
[PROOFSTEP]
rw [← cancel_epi ((shiftFunctorAdd C m n).inv.app X.obj)]
[GOAL]
case refine'_1
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X : DifferentialObject S C
⊢ NatTrans.app (CategoryTheory.shiftFunctorAdd C m n).inv X.obj ≫
      ((CategoryTheory.shiftFunctor C (m + n)).map X.d ≫ NatTrans.app (shiftFunctorComm C 1 (m + n)).hom X.obj) ≫
        (CategoryTheory.shiftFunctor C 1).map (NatTrans.app (CategoryTheory.shiftFunctorAdd C m n).hom X.obj) =
    NatTrans.app (CategoryTheory.shiftFunctorAdd C m n).inv X.obj ≫
      NatTrans.app (CategoryTheory.shiftFunctorAdd C m n).hom X.obj ≫
        (CategoryTheory.shiftFunctor C n).map
            ((CategoryTheory.shiftFunctor C m).map X.d ≫ NatTrans.app (shiftFunctorComm C 1 m).hom X.obj) ≫
          NatTrans.app (shiftFunctorComm C 1 n).hom ((CategoryTheory.shiftFunctor C m).obj X.obj)
[PROOFSTEP]
simp only [Category.assoc, Iso.inv_hom_id_app_assoc]
[GOAL]
case refine'_1
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X : DifferentialObject S C
⊢ NatTrans.app (CategoryTheory.shiftFunctorAdd C m n).inv X.obj ≫
      (CategoryTheory.shiftFunctor C (m + n)).map X.d ≫
        NatTrans.app (shiftFunctorComm C 1 (m + n)).hom X.obj ≫
          (CategoryTheory.shiftFunctor C 1).map (NatTrans.app (CategoryTheory.shiftFunctorAdd C m n).hom X.obj) =
    (CategoryTheory.shiftFunctor C n).map
        ((CategoryTheory.shiftFunctor C m).map X.d ≫ NatTrans.app (shiftFunctorComm C 1 m).hom X.obj) ≫
      NatTrans.app (shiftFunctorComm C 1 n).hom ((CategoryTheory.shiftFunctor C m).obj X.obj)
[PROOFSTEP]
erw [← NatTrans.naturality_assoc]
[GOAL]
case refine'_1
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X : DifferentialObject S C
⊢ (CategoryTheory.shiftFunctor C m ⋙ CategoryTheory.shiftFunctor C n).map X.d ≫
      NatTrans.app (CategoryTheory.shiftFunctorAdd C m n).inv ((CategoryTheory.shiftFunctor C 1).obj X.obj) ≫
        NatTrans.app (shiftFunctorComm C 1 (m + n)).hom X.obj ≫
          (CategoryTheory.shiftFunctor C 1).map (NatTrans.app (CategoryTheory.shiftFunctorAdd C m n).hom X.obj) =
    (CategoryTheory.shiftFunctor C n).map
        ((CategoryTheory.shiftFunctor C m).map X.d ≫ NatTrans.app (shiftFunctorComm C 1 m).hom X.obj) ≫
      NatTrans.app (shiftFunctorComm C 1 n).hom ((CategoryTheory.shiftFunctor C m).obj X.obj)
[PROOFSTEP]
dsimp
[GOAL]
case refine'_1
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X : DifferentialObject S C
⊢ (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor C m).map X.d) ≫
      NatTrans.app (CategoryTheory.shiftFunctorAdd C m n).inv ((CategoryTheory.shiftFunctor C 1).obj X.obj) ≫
        NatTrans.app (shiftFunctorComm C 1 (m + n)).hom X.obj ≫
          (CategoryTheory.shiftFunctor C 1).map (NatTrans.app (CategoryTheory.shiftFunctorAdd C m n).hom X.obj) =
    (CategoryTheory.shiftFunctor C n).map
        ((CategoryTheory.shiftFunctor C m).map X.d ≫ NatTrans.app (shiftFunctorComm C 1 m).hom X.obj) ≫
      NatTrans.app (shiftFunctorComm C 1 n).hom ((CategoryTheory.shiftFunctor C m).obj X.obj)
[PROOFSTEP]
simp only [Functor.map_comp, Category.assoc, shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app 1 m n X.obj,
  Iso.inv_hom_id_app_assoc]
[GOAL]
case refine'_2
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ (shiftFunctor C (m + n)).map f ≫
      ((fun X =>
            mkIso (shiftAdd X.obj m n)
              (_ :
                ((shiftFunctor C (m + n)).obj X).d ≫ (CategoryTheory.shiftFunctor C 1).map (shiftAdd X.obj m n).hom =
                  (shiftAdd X.obj m n).hom ≫ ((shiftFunctor C m ⋙ shiftFunctor C n).obj X).d))
          Y✝).hom =
    ((fun X =>
            mkIso (shiftAdd X.obj m n)
              (_ :
                ((shiftFunctor C (m + n)).obj X).d ≫ (CategoryTheory.shiftFunctor C 1).map (shiftAdd X.obj m n).hom =
                  (shiftAdd X.obj m n).hom ≫ ((shiftFunctor C m ⋙ shiftFunctor C n).obj X).d))
          X✝).hom ≫
      (shiftFunctor C m ⋙ shiftFunctor C n).map f
[PROOFSTEP]
ext
[GOAL]
case refine'_2.w
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ autoParam
    (((shiftFunctor C (m + n)).map f ≫
          ((fun X =>
                mkIso (shiftAdd X.obj m n)
                  (_ :
                    ((shiftFunctor C (m + n)).obj X).d ≫
                        (CategoryTheory.shiftFunctor C 1).map (shiftAdd X.obj m n).hom =
                      (shiftAdd X.obj m n).hom ≫ ((shiftFunctor C m ⋙ shiftFunctor C n).obj X).d))
              Y✝).hom).f =
      (((fun X =>
                mkIso (shiftAdd X.obj m n)
                  (_ :
                    ((shiftFunctor C (m + n)).obj X).d ≫
                        (CategoryTheory.shiftFunctor C 1).map (shiftAdd X.obj m n).hom =
                      (shiftAdd X.obj m n).hom ≫ ((shiftFunctor C m ⋙ shiftFunctor C n).obj X).d))
              X✝).hom ≫
          (shiftFunctor C m ⋙ shiftFunctor C n).map f).f)
    _auto✝
[PROOFSTEP]
dsimp
[GOAL]
case refine'_2.w
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ autoParam
    ((CategoryTheory.shiftFunctor C (m + n)).map f.f ≫ NatTrans.app (CategoryTheory.shiftFunctorAdd C m n).hom Y✝.obj =
      NatTrans.app (CategoryTheory.shiftFunctorAdd C m n).hom X✝.obj ≫
        (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor C m).map f.f))
    _auto✝
[PROOFSTEP]
exact NatTrans.naturality _ _
[GOAL]
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
⊢ shiftFunctor C 0 ≅ 𝟭 (DifferentialObject S C)
[PROOFSTEP]
refine' NatIso.ofComponents (fun X => mkIso ((shiftFunctorZero C S).app X.obj) _) (fun f => _)
[GOAL]
case refine'_1
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X : DifferentialObject S C
⊢ ((shiftFunctor C 0).obj X).d ≫ (CategoryTheory.shiftFunctor C 1).map ((shiftFunctorZero C S).app X.obj).hom =
    ((shiftFunctorZero C S).app X.obj).hom ≫ ((𝟭 (DifferentialObject S C)).obj X).d
[PROOFSTEP]
erw [← NatTrans.naturality]
[GOAL]
case refine'_1
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X : DifferentialObject S C
⊢ ((shiftFunctor C 0).obj X).d ≫ (CategoryTheory.shiftFunctor C 1).map ((shiftFunctorZero C S).app X.obj).hom =
    (CategoryTheory.shiftFunctor C 0).map ((𝟭 (DifferentialObject S C)).obj X).2 ≫
      NatTrans.app (shiftFunctorZero C S).hom
        ((CategoryTheory.shiftFunctor C 1).obj ((𝟭 (DifferentialObject S C)).obj X).1)
[PROOFSTEP]
dsimp
[GOAL]
case refine'_1
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X : DifferentialObject S C
⊢ ((CategoryTheory.shiftFunctor C 0).map X.d ≫ NatTrans.app (shiftFunctorComm C 1 0).hom X.obj) ≫
      (CategoryTheory.shiftFunctor C 1).map (NatTrans.app (shiftFunctorZero C S).hom X.obj) =
    (CategoryTheory.shiftFunctor C 0).map X.2 ≫
      NatTrans.app (shiftFunctorZero C S).hom ((CategoryTheory.shiftFunctor C 1).obj X.1)
[PROOFSTEP]
simp only [shiftFunctorZero_hom_app_shift, Category.assoc]
[GOAL]
case refine'_2
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ (shiftFunctor C 0).map f ≫
      ((fun X =>
            mkIso ((shiftFunctorZero C S).app X.obj)
              (_ :
                ((shiftFunctor C 0).obj X).d ≫
                    (CategoryTheory.shiftFunctor C 1).map ((shiftFunctorZero C S).app X.obj).hom =
                  ((shiftFunctorZero C S).app X.obj).hom ≫ ((𝟭 (DifferentialObject S C)).obj X).d))
          Y✝).hom =
    ((fun X =>
            mkIso ((shiftFunctorZero C S).app X.obj)
              (_ :
                ((shiftFunctor C 0).obj X).d ≫
                    (CategoryTheory.shiftFunctor C 1).map ((shiftFunctorZero C S).app X.obj).hom =
                  ((shiftFunctorZero C S).app X.obj).hom ≫ ((𝟭 (DifferentialObject S C)).obj X).d))
          X✝).hom ≫
      (𝟭 (DifferentialObject S C)).map f
[PROOFSTEP]
aesop_cat
[GOAL]
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m₁ m₂ m₃ : S
X : DifferentialObject S C
⊢ NatTrans.app (shiftFunctorAdd C (m₁ + m₂) m₃).hom X ≫
      (shiftFunctor C m₃).map (NatTrans.app (shiftFunctorAdd C m₁ m₂).hom X) =
    eqToHom (_ : (shiftFunctor C (m₁ + m₂ + m₃)).obj X = (shiftFunctor C (m₁ + (m₂ + m₃))).obj X) ≫
      NatTrans.app (shiftFunctorAdd C m₁ (m₂ + m₃)).hom X ≫
        NatTrans.app (shiftFunctorAdd C m₂ m₃).hom ((shiftFunctor C m₁).obj X)
[PROOFSTEP]
ext1
[GOAL]
case w
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m₁ m₂ m₃ : S
X : DifferentialObject S C
⊢ autoParam
    ((NatTrans.app (shiftFunctorAdd C (m₁ + m₂) m₃).hom X ≫
          (shiftFunctor C m₃).map (NatTrans.app (shiftFunctorAdd C m₁ m₂).hom X)).f =
      (eqToHom (_ : (shiftFunctor C (m₁ + m₂ + m₃)).obj X = (shiftFunctor C (m₁ + (m₂ + m₃))).obj X) ≫
          NatTrans.app (shiftFunctorAdd C m₁ (m₂ + m₃)).hom X ≫
            NatTrans.app (shiftFunctorAdd C m₂ m₃).hom ((shiftFunctor C m₁).obj X)).f)
    _auto✝
[PROOFSTEP]
convert shiftFunctorAdd_assoc_hom_app m₁ m₂ m₃ X.obj
[GOAL]
case h.e'_3.h
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m₁ m₂ m₃ : S
X : DifferentialObject S C
e_1✝ :
  (((shiftFunctor C (m₁ + m₂ + m₃)).obj X).obj ⟶
      ((shiftFunctor C m₃).obj ((shiftFunctor C m₁ ⋙ shiftFunctor C m₂).obj X)).obj) =
    ((CategoryTheory.shiftFunctor C (m₁ + m₂ + m₃)).obj X.obj ⟶
      (CategoryTheory.shiftFunctor C m₃).obj
        ((CategoryTheory.shiftFunctor C m₁ ⋙ CategoryTheory.shiftFunctor C m₂).obj X.obj))
⊢ (eqToHom (_ : (shiftFunctor C (m₁ + m₂ + m₃)).obj X = (shiftFunctor C (m₁ + (m₂ + m₃))).obj X) ≫
        NatTrans.app (shiftFunctorAdd C m₁ (m₂ + m₃)).hom X ≫
          NatTrans.app (shiftFunctorAdd C m₂ m₃).hom ((shiftFunctor C m₁).obj X)).f =
    NatTrans.app (shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + m₂ + m₃) (_ : m₁ + (m₂ + m₃) = m₁ + m₂ + m₃)).hom X.obj ≫
      NatTrans.app (CategoryTheory.shiftFunctorAdd C m₂ m₃).hom ((CategoryTheory.shiftFunctor C m₁).obj X.obj)
[PROOFSTEP]
dsimp [shiftFunctorAdd']
[GOAL]
case h.e'_3.h
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m₁ m₂ m₃ : S
X : DifferentialObject S C
e_1✝ :
  (((shiftFunctor C (m₁ + m₂ + m₃)).obj X).obj ⟶
      ((shiftFunctor C m₃).obj ((shiftFunctor C m₁ ⋙ shiftFunctor C m₂).obj X)).obj) =
    ((CategoryTheory.shiftFunctor C (m₁ + m₂ + m₃)).obj X.obj ⟶
      (CategoryTheory.shiftFunctor C m₃).obj
        ((CategoryTheory.shiftFunctor C m₁ ⋙ CategoryTheory.shiftFunctor C m₂).obj X.obj))
⊢ (eqToHom (_ : (shiftFunctor C (m₁ + m₂ + m₃)).obj X = (shiftFunctor C (m₁ + (m₂ + m₃))).obj X)).f ≫
      NatTrans.app (CategoryTheory.shiftFunctorAdd C m₁ (m₂ + m₃)).hom X.obj ≫
        NatTrans.app (CategoryTheory.shiftFunctorAdd C m₂ m₃).hom ((CategoryTheory.shiftFunctor C m₁).obj X.obj) =
    (NatTrans.app
          (eqToHom (_ : CategoryTheory.shiftFunctor C (m₁ + m₂ + m₃) = CategoryTheory.shiftFunctor C (m₁ + (m₂ + m₃))))
          X.obj ≫
        NatTrans.app (CategoryTheory.shiftFunctorAdd C m₁ (m₂ + m₃)).hom X.obj) ≫
      NatTrans.app (CategoryTheory.shiftFunctorAdd C m₂ m₃).hom ((CategoryTheory.shiftFunctor C m₁).obj X.obj)
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
⊢ NatTrans.app (shiftFunctorAdd C 0 n).hom X =
    eqToHom (_ : (shiftFunctor C (0 + n)).obj X = (shiftFunctor C n).obj ((𝟭 (DifferentialObject S C)).obj X)) ≫
      (shiftFunctor C n).map (NatTrans.app (shiftZero C).inv X)
[PROOFSTEP]
ext1
[GOAL]
case w
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
⊢ autoParam
    ((NatTrans.app (shiftFunctorAdd C 0 n).hom X).f =
      (eqToHom (_ : (shiftFunctor C (0 + n)).obj X = (shiftFunctor C n).obj ((𝟭 (DifferentialObject S C)).obj X)) ≫
          (shiftFunctor C n).map (NatTrans.app (shiftZero C).inv X)).f)
    _auto✝
[PROOFSTEP]
convert shiftFunctorAdd_zero_add_hom_app n X.obj
[GOAL]
case h.e'_3.h
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
e_1✝ :
  (((shiftFunctor C (0 + n)).obj X).obj ⟶ ((shiftFunctor C 0 ⋙ shiftFunctor C n).obj X).obj) =
    ((CategoryTheory.shiftFunctor C (0 + n)).obj X.obj ⟶
      (CategoryTheory.shiftFunctor C 0 ⋙ CategoryTheory.shiftFunctor C n).obj X.obj)
⊢ (eqToHom (_ : (shiftFunctor C (0 + n)).obj X = (shiftFunctor C n).obj ((𝟭 (DifferentialObject S C)).obj X)) ≫
        (shiftFunctor C n).map (NatTrans.app (shiftZero C).inv X)).f =
    eqToHom
        (_ :
          (CategoryTheory.shiftFunctor C (0 + n)).obj X.obj = (CategoryTheory.shiftFunctor C n).obj ((𝟭 C).obj X.obj)) ≫
      (CategoryTheory.shiftFunctor C n).map (NatTrans.app (shiftFunctorZero C S).inv X.obj)
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
⊢ NatTrans.app (shiftFunctorAdd C n 0).hom X =
    eqToHom (_ : (shiftFunctor C (n + 0)).obj X = (𝟭 (DifferentialObject S C)).obj ((shiftFunctor C n).obj X)) ≫
      NatTrans.app (shiftZero C).inv ((shiftFunctor C n).obj X)
[PROOFSTEP]
ext1
[GOAL]
case w
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
⊢ autoParam
    ((NatTrans.app (shiftFunctorAdd C n 0).hom X).f =
      (eqToHom (_ : (shiftFunctor C (n + 0)).obj X = (𝟭 (DifferentialObject S C)).obj ((shiftFunctor C n).obj X)) ≫
          NatTrans.app (shiftZero C).inv ((shiftFunctor C n).obj X)).f)
    _auto✝
[PROOFSTEP]
convert shiftFunctorAdd_add_zero_hom_app n X.obj
[GOAL]
case h.e'_3.h
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
e_1✝ :
  (((shiftFunctor C (n + 0)).obj X).obj ⟶ ((shiftFunctor C n ⋙ shiftFunctor C 0).obj X).obj) =
    ((CategoryTheory.shiftFunctor C (n + 0)).obj X.obj ⟶
      (CategoryTheory.shiftFunctor C n ⋙ CategoryTheory.shiftFunctor C 0).obj X.obj)
⊢ (eqToHom (_ : (shiftFunctor C (n + 0)).obj X = (𝟭 (DifferentialObject S C)).obj ((shiftFunctor C n).obj X)) ≫
        NatTrans.app (shiftZero C).inv ((shiftFunctor C n).obj X)).f =
    eqToHom
        (_ :
          (CategoryTheory.shiftFunctor C (n + 0)).obj X.obj = (𝟭 C).obj ((CategoryTheory.shiftFunctor C n).obj X.obj)) ≫
      NatTrans.app (shiftFunctorZero C S).inv ((CategoryTheory.shiftFunctor C n).obj X.obj)
[PROOFSTEP]
simp
