[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{?u.33371, u_2} D
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
⊢ π₁Toπ₂ ≫ π₂Toπ₃ = 0
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.36094, u_1} C
inst✝³ : Category.{?u.36098, u_2} D
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms F
⊢ F.map S.f ≫ F.map S.g = 0
[PROOFSTEP]
rw [← F.map_comp, S.zero, F.map_zero]
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.44556, u_1} C
inst✝³ : Category.{?u.44560, u_2} D
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms F
X✝ Y✝ : ShortComplex C
φ : X✝ ⟶ Y✝
⊢ F.map φ.τ₁ ≫ ((fun S => map S F) Y✝).f = ((fun S => map S F) X✝).f ≫ F.map φ.τ₂
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.44556, u_1} C
inst✝³ : Category.{?u.44560, u_2} D
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms F
X✝ Y✝ : ShortComplex C
φ : X✝ ⟶ Y✝
⊢ F.map φ.τ₁ ≫ F.map Y✝.f = F.map X✝.f ≫ F.map φ.τ₂
[PROOFSTEP]
simp only [← F.map_comp, φ.comm₁₂]
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.44556, u_1} C
inst✝³ : Category.{?u.44560, u_2} D
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms F
X✝ Y✝ : ShortComplex C
φ : X✝ ⟶ Y✝
⊢ F.map φ.τ₂ ≫ ((fun S => map S F) Y✝).g = ((fun S => map S F) X✝).g ≫ F.map φ.τ₃
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.44556, u_1} C
inst✝³ : Category.{?u.44560, u_2} D
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms F
X✝ Y✝ : ShortComplex C
φ : X✝ ⟶ Y✝
⊢ F.map φ.τ₂ ≫ F.map Y✝.g = F.map X✝.g ≫ F.map φ.τ₃
[PROOFSTEP]
simp only [← F.map_comp, φ.comm₂₃]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.52069, u_1} C
inst✝² : Category.{?u.52073, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
e₁ : S₁.X₁ ≅ S₂.X₁
e₂ : S₁.X₂ ≅ S₂.X₂
e₃ : S₁.X₃ ≅ S₂.X₃
comm₁₂ : autoParam (e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom) _auto✝
comm₂₃ : autoParam (e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom) _auto✝
⊢ e₁.inv ≫ S₁.f = S₂.f ≫ e₂.inv
[PROOFSTEP]
rw [← cancel_mono e₂.hom, assoc, assoc, e₂.inv_hom_id, comp_id, ← comm₁₂, e₁.inv_hom_id_assoc]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.52069, u_1} C
inst✝² : Category.{?u.52073, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
e₁ : S₁.X₁ ≅ S₂.X₁
e₂ : S₁.X₂ ≅ S₂.X₂
e₃ : S₁.X₃ ≅ S₂.X₃
comm₁₂ : autoParam (e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom) _auto✝
comm₂₃ : autoParam (e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom) _auto✝
⊢ e₂.inv ≫ S₁.g = S₂.g ≫ e₃.inv
[PROOFSTEP]
rw [← cancel_mono e₃.hom, assoc, assoc, e₃.inv_hom_id, comp_id, ← comm₂₃, e₂.inv_hom_id_assoc]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.62853, u_1} C
inst✝² : Category.{?u.62857, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
⊢ S.g.op ≫ S.f.op = 0
[PROOFSTEP]
simp only [← op_comp, S.zero]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.62853, u_1} C
inst✝² : Category.{?u.62857, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
⊢ 0.op = 0
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.63553, u_1} C
inst✝² : Category.{?u.63557, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
φ : S₁ ⟶ S₂
⊢ φ.τ₃.op ≫ (op S₁).f = (op S₂).f ≫ φ.τ₂.op
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.63553, u_1} C
inst✝² : Category.{?u.63557, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
φ : S₁ ⟶ S₂
⊢ φ.τ₃.op ≫ S₁.g.op = S₂.g.op ≫ φ.τ₂.op
[PROOFSTEP]
simp only [← op_comp, φ.comm₂₃]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.63553, u_1} C
inst✝² : Category.{?u.63557, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
φ : S₁ ⟶ S₂
⊢ φ.τ₂.op ≫ (op S₁).g = (op S₂).g ≫ φ.τ₁.op
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.63553, u_1} C
inst✝² : Category.{?u.63557, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
φ : S₁ ⟶ S₂
⊢ φ.τ₂.op ≫ S₁.f.op = S₂.f.op ≫ φ.τ₁.op
[PROOFSTEP]
simp only [← op_comp, φ.comm₁₂]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.64969, u_1} C
inst✝² : Category.{?u.64973, u_2} D
inst✝¹ : HasZeroMorphisms C
S✝ S₁ S₂ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
S : ShortComplex Cᵒᵖ
⊢ S.g.unop ≫ S.f.unop = 0
[PROOFSTEP]
simp only [← unop_comp, S.zero]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.64969, u_1} C
inst✝² : Category.{?u.64973, u_2} D
inst✝¹ : HasZeroMorphisms C
S✝ S₁ S₂ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
S : ShortComplex Cᵒᵖ
⊢ 0.unop = 0
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.65733, u_1} C
inst✝² : Category.{?u.65737, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
⊢ φ.τ₃.unop ≫ (unop S₁).f = (unop S₂).f ≫ φ.τ₂.unop
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.65733, u_1} C
inst✝² : Category.{?u.65737, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
⊢ φ.τ₃.unop ≫ S₁.g.unop = S₂.g.unop ≫ φ.τ₂.unop
[PROOFSTEP]
simp only [← unop_comp, φ.comm₂₃]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.65733, u_1} C
inst✝² : Category.{?u.65737, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
⊢ φ.τ₂.unop ≫ (unop S₁).g = (unop S₂).g ≫ φ.τ₁.unop
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.65733, u_1} C
inst✝² : Category.{?u.65737, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
⊢ φ.τ₂.unop ≫ S₁.f.unop = S₂.f.unop ≫ φ.τ₁.unop
[PROOFSTEP]
simp only [← unop_comp, φ.comm₁₂]
