[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


[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
H : T ∈ distinguishedTriangles
⊢ T.mor₁ ≫ T.mor₂ = 0
[PROOFSTEP]
obtain ⟨c, hc⟩ :=
  complete_distinguished_triangle_morphism _ _ (contractible_distinguished T.obj₁) H (𝟙 T.obj₁) T.mor₁ rfl
[GOAL]
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
H : T ∈ distinguishedTriangles
c : (contractibleTriangle T.obj₁).obj₃ ⟶ T.obj₃
hc :
  (contractibleTriangle T.obj₁).mor₂ ≫ c = T.mor₁ ≫ T.mor₂ ∧
    (contractibleTriangle T.obj₁).mor₃ ≫ (shiftFunctor C 1).map (𝟙 T.obj₁) = c ≫ T.mor₃
⊢ T.mor₁ ≫ T.mor₂ = 0
[PROOFSTEP]
simpa only [contractibleTriangle_mor₂, zero_comp] using hc.left.symm
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
H : T ∈ distinguishedTriangles
⊢ T.mor₃ ≫ (shiftEquiv C 1).functor.map T.mor₁ = 0
[PROOFSTEP]
have H₂ := rot_of_dist_triangle T.rotate (rot_of_dist_triangle T H)
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
H : T ∈ distinguishedTriangles
H₂ : Triangle.rotate (Triangle.rotate T) ∈ distinguishedTriangles
⊢ T.mor₃ ≫ (shiftEquiv C 1).functor.map T.mor₁ = 0
[PROOFSTEP]
simpa using comp_dist_triangle_mor_zero₁₂ T.rotate.rotate H₂
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
Y Z : C
g : Y ⟶ Z
⊢ ∃ X f h, Triangle.mk f g h ∈ distinguishedTriangles
[PROOFSTEP]
obtain ⟨X', f', g', mem⟩ := distinguished_cocone_triangle g
[GOAL]
case intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
Y Z : C
g : Y ⟶ Z
X' : C
f' : Z ⟶ X'
g' : X' ⟶ (shiftFunctor C 1).obj Y
mem : Triangle.mk g f' g' ∈ distinguishedTriangles
⊢ ∃ X f h, Triangle.mk f g h ∈ distinguishedTriangles
[PROOFSTEP]
exact ⟨_, _, _, inv_rot_of_dist_triangle _ mem⟩
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
⊢ ∃ Y f g, Triangle.mk f g h ∈ distinguishedTriangles
[PROOFSTEP]
obtain ⟨Y', f', g', mem⟩ := distinguished_cocone_triangle h
[GOAL]
case intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
Y' : C
f' : (shiftFunctor C 1).obj X ⟶ Y'
g' : Y' ⟶ (shiftFunctor C 1).obj Z
mem : Triangle.mk h f' g' ∈ distinguishedTriangles
⊢ ∃ Y f g, Triangle.mk f g h ∈ distinguishedTriangles
[PROOFSTEP]
let T' := (Triangle.mk h f' g').invRotate.invRotate
[GOAL]
case intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
Y' : C
f' : (shiftFunctor C 1).obj X ⟶ Y'
g' : Y' ⟶ (shiftFunctor C 1).obj Z
mem : Triangle.mk h f' g' ∈ distinguishedTriangles
T' : Triangle C := Triangle.invRotate (Triangle.invRotate (Triangle.mk h f' g'))
⊢ ∃ Y f g, Triangle.mk f g h ∈ distinguishedTriangles
[PROOFSTEP]
refine'
  ⟨T'.obj₂, ((shiftEquiv C (1 : ℤ)).unitIso.app X).hom ≫ T'.mor₁, T'.mor₂,
    isomorphic_distinguished _ (inv_rot_of_dist_triangle _ (inv_rot_of_dist_triangle _ mem)) _ _⟩
[GOAL]
case intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
Y' : C
f' : (shiftFunctor C 1).obj X ⟶ Y'
g' : Y' ⟶ (shiftFunctor C 1).obj Z
mem : Triangle.mk h f' g' ∈ distinguishedTriangles
T' : Triangle C := Triangle.invRotate (Triangle.invRotate (Triangle.mk h f' g'))
⊢ Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h ≅
    Triangle.invRotate (Triangle.invRotate (Triangle.mk h f' g'))
[PROOFSTEP]
exact
  Triangle.isoMk _ _ ((shiftEquiv C (1 : ℤ)).unitIso.app X) (Iso.refl _) (Iso.refl _) (by aesop_cat) (by aesop_cat)
    (by dsimp; simp only [shift_shiftFunctorCompIsoId_inv_app, id_comp])
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
Y' : C
f' : (shiftFunctor C 1).obj X ⟶ Y'
g' : Y' ⟶ (shiftFunctor C 1).obj Z
mem : Triangle.mk h f' g' ∈ distinguishedTriangles
T' : Triangle C := Triangle.invRotate (Triangle.invRotate (Triangle.mk h f' g'))
⊢ (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).mor₁ ≫
      (Iso.refl (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).obj₂).hom =
    ((shiftEquiv C 1).unitIso.app X).hom ≫ (Triangle.invRotate (Triangle.invRotate (Triangle.mk h f' g'))).mor₁
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
Y' : C
f' : (shiftFunctor C 1).obj X ⟶ Y'
g' : Y' ⟶ (shiftFunctor C 1).obj Z
mem : Triangle.mk h f' g' ∈ distinguishedTriangles
T' : Triangle C := Triangle.invRotate (Triangle.invRotate (Triangle.mk h f' g'))
⊢ (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).mor₂ ≫
      (Iso.refl (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).obj₃).hom =
    (Iso.refl (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).obj₂).hom ≫
      (Triangle.invRotate (Triangle.invRotate (Triangle.mk h f' g'))).mor₂
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
Y' : C
f' : (shiftFunctor C 1).obj X ⟶ Y'
g' : Y' ⟶ (shiftFunctor C 1).obj Z
mem : Triangle.mk h f' g' ∈ distinguishedTriangles
T' : Triangle C := Triangle.invRotate (Triangle.invRotate (Triangle.mk h f' g'))
⊢ (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).mor₃ ≫
      (shiftFunctor C 1).map ((shiftEquiv C 1).unitIso.app X).hom =
    (Iso.refl (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).obj₃).hom ≫
      (Triangle.invRotate (Triangle.invRotate (Triangle.mk h f' g'))).mor₃
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
Y' : C
f' : (shiftFunctor C 1).obj X ⟶ Y'
g' : Y' ⟶ (shiftFunctor C 1).obj Z
mem : Triangle.mk h f' g' ∈ distinguishedTriangles
T' : Triangle C := Triangle.invRotate (Triangle.invRotate (Triangle.mk h f' g'))
⊢ h ≫ (shiftFunctor C 1).map (NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).inv X) =
    𝟙 Z ≫ h ≫ NatTrans.app (shiftFunctorCompIsoId C (-1) 1 (_ : -1 + 1 = 0)).inv ((shiftFunctor C 1).obj X)
[PROOFSTEP]
simp only [shift_shiftFunctorCompIsoId_inv_app, id_comp]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
⊢ ∃ a, T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃
[PROOFSTEP]
obtain ⟨a, ⟨ha₁, ha₂⟩⟩ :=
  complete_distinguished_triangle_morphism _ _ (rot_of_dist_triangle _ hT₁) (rot_of_dist_triangle _ hT₂) b c comm
[GOAL]
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : (Triangle.rotate T₁).obj₃ ⟶ (Triangle.rotate T₂).obj₃
ha₁ : (Triangle.rotate T₁).mor₂ ≫ a = c ≫ (Triangle.rotate T₂).mor₂
ha₂ : (Triangle.rotate T₁).mor₃ ≫ (shiftFunctor C 1).map b = a ≫ (Triangle.rotate T₂).mor₃
⊢ ∃ a, T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃
[PROOFSTEP]
refine' ⟨(shiftFunctor C (1 : ℤ)).preimage a, ⟨_, _⟩⟩
[GOAL]
case intro.intro.refine'_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : (Triangle.rotate T₁).obj₃ ⟶ (Triangle.rotate T₂).obj₃
ha₁ : (Triangle.rotate T₁).mor₂ ≫ a = c ≫ (Triangle.rotate T₂).mor₂
ha₂ : (Triangle.rotate T₁).mor₃ ≫ (shiftFunctor C 1).map b = a ≫ (Triangle.rotate T₂).mor₃
⊢ T₁.mor₁ ≫ b = (shiftFunctor C 1).preimage a ≫ T₂.mor₁
[PROOFSTEP]
apply (shiftFunctor C (1 : ℤ)).map_injective
[GOAL]
case intro.intro.refine'_1.a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : (Triangle.rotate T₁).obj₃ ⟶ (Triangle.rotate T₂).obj₃
ha₁ : (Triangle.rotate T₁).mor₂ ≫ a = c ≫ (Triangle.rotate T₂).mor₂
ha₂ : (Triangle.rotate T₁).mor₃ ≫ (shiftFunctor C 1).map b = a ≫ (Triangle.rotate T₂).mor₃
⊢ (shiftFunctor C 1).map (T₁.mor₁ ≫ b) = (shiftFunctor C 1).map ((shiftFunctor C 1).preimage a ≫ T₂.mor₁)
[PROOFSTEP]
dsimp at ha₂
[GOAL]
case intro.intro.refine'_1.a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : (Triangle.rotate T₁).obj₃ ⟶ (Triangle.rotate T₂).obj₃
ha₁ : (Triangle.rotate T₁).mor₂ ≫ a = c ≫ (Triangle.rotate T₂).mor₂
ha₂ : (-(shiftFunctor C 1).map T₁.mor₁) ≫ (shiftFunctor C 1).map b = a ≫ (-(shiftFunctor C 1).map T₂.mor₁)
⊢ (shiftFunctor C 1).map (T₁.mor₁ ≫ b) = (shiftFunctor C 1).map ((shiftFunctor C 1).preimage a ≫ T₂.mor₁)
[PROOFSTEP]
rw [neg_comp, comp_neg, neg_inj] at ha₂
[GOAL]
case intro.intro.refine'_1.a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : (Triangle.rotate T₁).obj₃ ⟶ (Triangle.rotate T₂).obj₃
ha₁ : (Triangle.rotate T₁).mor₂ ≫ a = c ≫ (Triangle.rotate T₂).mor₂
ha₂ : (shiftFunctor C 1).map T₁.mor₁ ≫ (shiftFunctor C 1).map b = a ≫ (shiftFunctor C 1).map T₂.mor₁
⊢ (shiftFunctor C 1).map (T₁.mor₁ ≫ b) = (shiftFunctor C 1).map ((shiftFunctor C 1).preimage a ≫ T₂.mor₁)
[PROOFSTEP]
simpa only [Functor.map_comp, Functor.image_preimage] using ha₂
[GOAL]
case intro.intro.refine'_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : (Triangle.rotate T₁).obj₃ ⟶ (Triangle.rotate T₂).obj₃
ha₁ : (Triangle.rotate T₁).mor₂ ≫ a = c ≫ (Triangle.rotate T₂).mor₂
ha₂ : (Triangle.rotate T₁).mor₃ ≫ (shiftFunctor C 1).map b = a ≫ (Triangle.rotate T₂).mor₃
⊢ T₁.mor₃ ≫ (shiftFunctor C 1).map ((shiftFunctor C 1).preimage a) = c ≫ T₂.mor₃
[PROOFSTEP]
simpa only [Functor.image_preimage] using ha₁
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃
⊢ ∃ b, T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₂ ≫ c = b ≫ T₂.mor₂
[PROOFSTEP]
obtain ⟨a, ⟨ha₁, ha₂⟩⟩ :=
  complete_distinguished_triangle_morphism _ _ (inv_rot_of_dist_triangle _ hT₁) (inv_rot_of_dist_triangle _ hT₂)
    (c⟦(-1 : ℤ)⟧') a
    (by
      dsimp
      simp only [neg_comp, comp_neg, ← Functor.map_comp_assoc, ← comm, Functor.map_comp, shift_shift_neg',
        Functor.id_obj, assoc, Iso.inv_hom_id_app, comp_id])
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃
⊢ (Triangle.invRotate T₁).mor₁ ≫ a = (shiftFunctor C (-1)).map c ≫ (Triangle.invRotate T₂).mor₁
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃
⊢ (-(shiftFunctor C (-1)).map T₁.mor₃ ≫ NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom T₁.obj₁) ≫
      a =
    (shiftFunctor C (-1)).map c ≫
      (-(shiftFunctor C (-1)).map T₂.mor₃ ≫ NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).hom T₂.obj₁)
[PROOFSTEP]
simp only [neg_comp, comp_neg, ← Functor.map_comp_assoc, ← comm, Functor.map_comp, shift_shift_neg', Functor.id_obj,
  assoc, Iso.inv_hom_id_app, comp_id]
[GOAL]
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a✝ : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃
a : (Triangle.invRotate T₁).obj₃ ⟶ (Triangle.invRotate T₂).obj₃
ha₁ : (Triangle.invRotate T₁).mor₂ ≫ a = a✝ ≫ (Triangle.invRotate T₂).mor₂
ha₂ :
  (Triangle.invRotate T₁).mor₃ ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) = a ≫ (Triangle.invRotate T₂).mor₃
⊢ ∃ b, T₁.mor₁ ≫ b = a✝ ≫ T₂.mor₁ ∧ T₁.mor₂ ≫ c = b ≫ T₂.mor₂
[PROOFSTEP]
refine' ⟨a, ⟨ha₁, _⟩⟩
[GOAL]
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a✝ : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃
a : (Triangle.invRotate T₁).obj₃ ⟶ (Triangle.invRotate T₂).obj₃
ha₁ : (Triangle.invRotate T₁).mor₂ ≫ a = a✝ ≫ (Triangle.invRotate T₂).mor₂
ha₂ :
  (Triangle.invRotate T₁).mor₃ ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) = a ≫ (Triangle.invRotate T₂).mor₃
⊢ T₁.mor₂ ≫ c = a ≫ T₂.mor₂
[PROOFSTEP]
dsimp only [Triangle.invRotate, Triangle.mk] at ha₂
[GOAL]
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a✝ : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃
a : (Triangle.invRotate T₁).obj₃ ⟶ (Triangle.invRotate T₂).obj₃
ha₁ : (Triangle.invRotate T₁).mor₂ ≫ a = a✝ ≫ (Triangle.invRotate T₂).mor₂
ha₂ :
  (T₁.mor₂ ≫ NatTrans.app (shiftEquiv C 1).counitIso.inv T₁.3) ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) =
    a ≫ T₂.mor₂ ≫ NatTrans.app (shiftEquiv C 1).counitIso.inv T₂.3
⊢ T₁.mor₂ ≫ c = a ≫ T₂.mor₂
[PROOFSTEP]
rw [← cancel_mono ((shiftEquiv C (1 : ℤ)).counitIso.inv.app T₂.obj₃), assoc, assoc, ← ha₂]
[GOAL]
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a✝ : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃
a : (Triangle.invRotate T₁).obj₃ ⟶ (Triangle.invRotate T₂).obj₃
ha₁ : (Triangle.invRotate T₁).mor₂ ≫ a = a✝ ≫ (Triangle.invRotate T₂).mor₂
ha₂ :
  (T₁.mor₂ ≫ NatTrans.app (shiftEquiv C 1).counitIso.inv T₁.3) ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) =
    a ≫ T₂.mor₂ ≫ NatTrans.app (shiftEquiv C 1).counitIso.inv T₂.3
⊢ T₁.mor₂ ≫ c ≫ NatTrans.app (shiftEquiv C 1).counitIso.inv T₂.obj₃ =
    (T₁.mor₂ ≫ NatTrans.app (shiftEquiv C 1).counitIso.inv T₁.3) ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c)
[PROOFSTEP]
simp only [shiftEquiv'_counitIso, shift_neg_shift', assoc, Iso.inv_hom_id_app_assoc]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
X : C
⊢ Triangle.mk 0 (𝟙 X) 0 ∈ distinguishedTriangles
[PROOFSTEP]
refine' isomorphic_distinguished _ (inv_rot_of_dist_triangle _ (contractible_distinguished X)) _ _
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
X : C
⊢ Triangle.mk 0 (𝟙 X) 0 ≅ Triangle.invRotate (contractibleTriangle X)
[PROOFSTEP]
exact
  Triangle.isoMk _ _ (Functor.mapZeroObject _).symm (Iso.refl _) (Iso.refl _) (by aesop_cat) (by aesop_cat)
    (by aesop_cat)
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 (𝟙 X) 0).mor₁ ≫ (Iso.refl (Triangle.mk 0 (𝟙 X) 0).obj₂).hom =
    (Functor.mapZeroObject (shiftFunctor C (-1))).symm.hom ≫ (Triangle.invRotate (contractibleTriangle X)).mor₁
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 (𝟙 X) 0).mor₂ ≫ (Iso.refl (Triangle.mk 0 (𝟙 X) 0).obj₃).hom =
    (Iso.refl (Triangle.mk 0 (𝟙 X) 0).obj₂).hom ≫ (Triangle.invRotate (contractibleTriangle X)).mor₂
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 (𝟙 X) 0).mor₃ ≫ (shiftFunctor C 1).map (Functor.mapZeroObject (shiftFunctor C (-1))).symm.hom =
    (Iso.refl (Triangle.mk 0 (𝟙 X) 0).obj₃).hom ≫ (Triangle.invRotate (contractibleTriangle X)).mor₃
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
X : C
⊢ Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X)) ∈ distinguishedTriangles
[PROOFSTEP]
refine' isomorphic_distinguished _ (inv_rot_of_dist_triangle _ (contractible_distinguished₁ (X⟦(1 : ℤ)⟧))) _ _
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
X : C
⊢ Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X)) ≅ Triangle.invRotate (Triangle.mk 0 (𝟙 ((shiftFunctor C 1).obj X)) 0)
[PROOFSTEP]
exact
  Triangle.isoMk _ _ ((shiftEquiv C (1 : ℤ)).unitIso.app X) (Iso.refl _) (Iso.refl _) (by aesop_cat) (by aesop_cat)
    (by dsimp; simp only [shift_shiftFunctorCompIsoId_inv_app, id_comp])
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).mor₁ ≫
      (Iso.refl (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).obj₂).hom =
    ((shiftEquiv C 1).unitIso.app X).hom ≫ (Triangle.invRotate (Triangle.mk 0 (𝟙 ((shiftFunctor C 1).obj X)) 0)).mor₁
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).mor₂ ≫
      (Iso.refl (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).obj₃).hom =
    (Iso.refl (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).obj₂).hom ≫
      (Triangle.invRotate (Triangle.mk 0 (𝟙 ((shiftFunctor C 1).obj X)) 0)).mor₂
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).mor₃ ≫ (shiftFunctor C 1).map ((shiftEquiv C 1).unitIso.app X).hom =
    (Iso.refl (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).obj₃).hom ≫
      (Triangle.invRotate (Triangle.mk 0 (𝟙 ((shiftFunctor C 1).obj X)) 0)).mor₃
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
X : C
⊢ 𝟙 ((shiftFunctor C 1).obj X) ≫
      (shiftFunctor C 1).map (NatTrans.app (shiftFunctorCompIsoId C 1 (-1) (_ : 1 + -1 = 0)).inv X) =
    𝟙 ((shiftFunctor C 1).obj X) ≫
      𝟙 ((shiftFunctor C 1).obj X) ≫
        NatTrans.app (shiftFunctorCompIsoId C (-1) 1 (_ : -1 + 1 = 0)).inv ((shiftFunctor C 1).obj X)
[PROOFSTEP]
simp only [shift_shiftFunctorCompIsoId_inv_app, id_comp]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
⊢ ∃ g, f = T.mor₂ ≫ g
[PROOFSTEP]
obtain ⟨g, ⟨hg₁, _⟩⟩ :=
  complete_distinguished_triangle_morphism T _ hT (contractible_distinguished₁ X) 0 f (by aesop_cat)
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
⊢ T.mor₁ ≫ f = 0 ≫ (Triangle.mk 0 (𝟙 X) 0).mor₁
[PROOFSTEP]
aesop_cat
[GOAL]
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
g : T.obj₃ ⟶ (Triangle.mk 0 (𝟙 X) 0).obj₃
hg₁ : T.mor₂ ≫ g = f ≫ (Triangle.mk 0 (𝟙 X) 0).mor₂
right✝ : T.mor₃ ≫ (shiftFunctor C 1).map 0 = g ≫ (Triangle.mk 0 (𝟙 X) 0).mor₃
⊢ ∃ g, f = T.mor₂ ≫ g
[PROOFSTEP]
exact ⟨g, by simpa using hg₁.symm⟩
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
g : T.obj₃ ⟶ (Triangle.mk 0 (𝟙 X) 0).obj₃
hg₁ : T.mor₂ ≫ g = f ≫ (Triangle.mk 0 (𝟙 X) 0).mor₂
right✝ : T.mor₃ ≫ (shiftFunctor C 1).map 0 = g ≫ (Triangle.mk 0 (𝟙 X) 0).mor₃
⊢ f = T.mor₂ ≫ g
[PROOFSTEP]
simpa using hg₁.symm
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
⊢ ∃ g, f = g ≫ T.mor₁
[PROOFSTEP]
obtain ⟨a, ⟨ha₁, _⟩⟩ :=
  complete_distinguished_triangle_morphism₁ _ T (contractible_distinguished X) hT f 0 (by aesop_cat)
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
⊢ (contractibleTriangle X).mor₂ ≫ 0 = f ≫ T.mor₂
[PROOFSTEP]
aesop_cat
[GOAL]
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
a : (contractibleTriangle X).obj₁ ⟶ T.obj₁
ha₁ : (contractibleTriangle X).mor₁ ≫ f = a ≫ T.mor₁
right✝ : (contractibleTriangle X).mor₃ ≫ (shiftFunctor C 1).map a = 0 ≫ T.mor₃
⊢ ∃ g, f = g ≫ T.mor₁
[PROOFSTEP]
exact ⟨a, by simpa using ha₁⟩
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
a : (contractibleTriangle X).obj₁ ⟶ T.obj₁
ha₁ : (contractibleTriangle X).mor₁ ≫ f = a ≫ T.mor₁
right✝ : (contractibleTriangle X).mor₃ ≫ (shiftFunctor C 1).map a = 0 ≫ T.mor₃
⊢ f = a ≫ T.mor₁
[PROOFSTEP]
simpa using ha₁
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ (shiftFunctor C 1).obj T.obj₁
hf : f ≫ (shiftFunctor C 1).map T.mor₁ = 0
⊢ f ≫ (Triangle.rotate (Triangle.rotate T)).mor₂ = 0
[PROOFSTEP]
aesop_cat