[GOAL]
V : Type u_1
inst✝¹ : Category.{?u.28, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ g.op ≫ f.op = 0
[PROOFSTEP]
rw [← op_comp, w, op_zero]
[GOAL]
V : Type u_1
inst✝¹ : Category.{?u.28, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ f ≫ factorThruImage g = 0
[PROOFSTEP]
rw [← cancel_mono (image.ι g), Category.assoc, image.fac, w, zero_comp]
[GOAL]
V : Type u_1
inst✝¹ : Category.{u_2, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.op f.op (_ : g.op ≫ f.op = 0) =
    (imageSubobjectIso g.op ≪≫ (imageOpOp g).symm).hom ≫
      (cokernel.desc f (factorThruImage g) (_ : f ≫ factorThruImage g = 0)).op ≫
        (kernelSubobjectIso f.op ≪≫ kernelOpOp f).inv
[PROOFSTEP]
ext
[GOAL]
case h
V : Type u_1
inst✝¹ : Category.{u_2, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.op f.op (_ : g.op ≫ f.op = 0) ≫ Subobject.arrow (kernelSubobject f.op) =
    ((imageSubobjectIso g.op ≪≫ (imageOpOp g).symm).hom ≫
        (cokernel.desc f (factorThruImage g) (_ : f ≫ factorThruImage g = 0)).op ≫
          (kernelSubobjectIso f.op ≪≫ kernelOpOp f).inv) ≫
      Subobject.arrow (kernelSubobject f.op)
[PROOFSTEP]
simp only [Iso.trans_hom, Iso.symm_hom, Iso.trans_inv, kernelOpOp_inv, Category.assoc, imageToKernel_arrow,
  kernelSubobject_arrow', kernel.lift_ι, ← op_comp, cokernel.π_desc, ← imageSubobject_arrow, ←
  imageUnopOp_inv_comp_op_factorThruImage g.op]
[GOAL]
case h
V : Type u_1
inst✝¹ : Category.{u_2, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ (imageSubobjectIso g.op).hom ≫ (imageUnopOp g.op).inv ≫ (factorThruImage g.op.unop).op =
    (imageSubobjectIso g.op).hom ≫ (imageOpOp g).inv ≫ (factorThruImage g).op
[PROOFSTEP]
rfl
[GOAL]
V : Type u_1
inst✝¹ : Category.{?u.7815, u_1} V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ g.unop ≫ f.unop = 0
[PROOFSTEP]
rw [← unop_comp, w, unop_zero]
[GOAL]
V : Type u_1
inst✝¹ : Category.{?u.7815, u_1} V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ f ≫ factorThruImage g = 0
[PROOFSTEP]
rw [← cancel_mono (image.ι g), Category.assoc, image.fac, w, zero_comp]
[GOAL]
V : Type u_1
inst✝¹ : Category.{u_2, u_1} V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.unop f.unop (_ : g.unop ≫ f.unop = 0) =
    (imageSubobjectIso g.unop ≪≫ (imageUnopUnop g).symm).hom ≫
      (cokernel.desc f (factorThruImage g) (_ : f ≫ factorThruImage g = 0)).unop ≫
        (kernelSubobjectIso f.unop ≪≫ kernelUnopUnop f).inv
[PROOFSTEP]
ext
[GOAL]
case h
V : Type u_1
inst✝¹ : Category.{u_2, u_1} V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.unop f.unop (_ : g.unop ≫ f.unop = 0) ≫ Subobject.arrow (kernelSubobject f.unop) =
    ((imageSubobjectIso g.unop ≪≫ (imageUnopUnop g).symm).hom ≫
        (cokernel.desc f (factorThruImage g) (_ : f ≫ factorThruImage g = 0)).unop ≫
          (kernelSubobjectIso f.unop ≪≫ kernelUnopUnop f).inv) ≫
      Subobject.arrow (kernelSubobject f.unop)
[PROOFSTEP]
dsimp only [imageUnopUnop]
[GOAL]
case h
V : Type u_1
inst✝¹ : Category.{u_2, u_1} V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.unop f.unop (_ : g.unop ≫ f.unop = 0) ≫ Subobject.arrow (kernelSubobject f.unop) =
    ((imageSubobjectIso g.unop ≪≫ (Iso.unop (imageUnopOp g)).symm).hom ≫
        (cokernel.desc f (factorThruImage g) (_ : f ≫ factorThruImage g = 0)).unop ≫
          (kernelSubobjectIso f.unop ≪≫ kernelUnopUnop f).inv) ≫
      Subobject.arrow (kernelSubobject f.unop)
[PROOFSTEP]
simp only [Iso.trans_hom, Iso.symm_hom, Iso.trans_inv, kernelUnopUnop_inv, Category.assoc, imageToKernel_arrow,
  kernelSubobject_arrow', kernel.lift_ι, cokernel.π_desc, Iso.unop_inv, ← unop_comp,
  factorThruImage_comp_imageUnopOp_inv, Quiver.Hom.unop_op, imageSubobject_arrow]
[GOAL]
V : Type u_1
inst✝¹ : Category.{?u.16638, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ g.op ≫ f.op = 0
[PROOFSTEP]
rw [← op_comp, w, op_zero]
[GOAL]
V : Type u_1
inst✝¹ : Category.{?u.16638, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ cokernel.desc f g w = cokernel.desc f (factorThruImage g) (_ : f ≫ factorThruImage g = 0) ≫ image.ι g
[PROOFSTEP]
ext
[GOAL]
case h
V : Type u_1
inst✝¹ : Category.{?u.16638, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ coequalizer.π f 0 ≫ cokernel.desc f g w =
    coequalizer.π f 0 ≫ cokernel.desc f (factorThruImage g) (_ : f ≫ factorThruImage g = 0) ≫ image.ι g
[PROOFSTEP]
simp only [image.fac, cokernel.π_desc, cokernel.π_desc_assoc]
[GOAL]
V : Type u_1
inst✝¹ : Category.{?u.28807, u_1} V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ g.unop ≫ f.unop = 0
[PROOFSTEP]
rw [← unop_comp, w, unop_zero]
[GOAL]
V : Type u_1
inst✝¹ : Category.{?u.28807, u_1} V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ cokernel.desc f g w = cokernel.desc f (factorThruImage g) (_ : f ≫ factorThruImage g = 0) ≫ image.ι g
[PROOFSTEP]
ext
[GOAL]
case h
V : Type u_1
inst✝¹ : Category.{?u.28807, u_1} V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ coequalizer.π f 0 ≫ cokernel.desc f g w =
    coequalizer.π f 0 ≫ cokernel.desc f (factorThruImage g) (_ : f ≫ factorThruImage g = 0) ≫ image.ι g
[PROOFSTEP]
simp only [image.fac, cokernel.π_desc, cokernel.π_desc_assoc]
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.40782, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X : HomologicalComplex V c
i j : ι
hij : ¬ComplexShape.Rel (ComplexShape.symm c) i j
⊢ (fun i j => (d X j i).op) i j = 0
[PROOFSTEP]
simp only
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.40782, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X : HomologicalComplex V c
i j : ι
hij : ¬ComplexShape.Rel (ComplexShape.symm c) i j
⊢ (d X j i).op = 0
[PROOFSTEP]
rw [X.shape j i hij, op_zero]
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.40782, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X : HomologicalComplex V c
x✝⁴ x✝³ x✝² : ι
x✝¹ : ComplexShape.Rel (ComplexShape.symm c) x✝⁴ x✝³
x✝ : ComplexShape.Rel (ComplexShape.symm c) x✝³ x✝²
⊢ (fun i j => (d X j i).op) x✝⁴ x✝³ ≫ (fun i j => (d X j i).op) x✝³ x✝² = 0
[PROOFSTEP]
rw [← op_comp, X.d_comp_d, op_zero]
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.42509, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X : HomologicalComplex V (ComplexShape.symm c)
i j : ι
hij : ¬ComplexShape.Rel c i j
⊢ (fun i j => (d X j i).op) i j = 0
[PROOFSTEP]
simp only
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.42509, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X : HomologicalComplex V (ComplexShape.symm c)
i j : ι
hij : ¬ComplexShape.Rel c i j
⊢ (d X j i).op = 0
[PROOFSTEP]
rw [X.shape j i hij, op_zero]
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.42509, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X : HomologicalComplex V (ComplexShape.symm c)
x✝⁴ x✝³ x✝² : ι
x✝¹ : ComplexShape.Rel c x✝⁴ x✝³
x✝ : ComplexShape.Rel c x✝³ x✝²
⊢ (fun i j => (d X j i).op) x✝⁴ x✝³ ≫ (fun i j => (d X j i).op) x✝³ x✝² = 0
[PROOFSTEP]
rw [← op_comp, X.d_comp_d, op_zero]
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.44206, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X : HomologicalComplex Vᵒᵖ c
i j : ι
hij : ¬ComplexShape.Rel (ComplexShape.symm c) i j
⊢ (fun i j => (d X j i).unop) i j = 0
[PROOFSTEP]
simp only
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.44206, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X : HomologicalComplex Vᵒᵖ c
i j : ι
hij : ¬ComplexShape.Rel (ComplexShape.symm c) i j
⊢ (d X j i).unop = 0
[PROOFSTEP]
rw [X.shape j i hij, unop_zero]
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.44206, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X : HomologicalComplex Vᵒᵖ c
x✝⁴ x✝³ x✝² : ι
x✝¹ : ComplexShape.Rel (ComplexShape.symm c) x✝⁴ x✝³
x✝ : ComplexShape.Rel (ComplexShape.symm c) x✝³ x✝²
⊢ (fun i j => (d X j i).unop) x✝⁴ x✝³ ≫ (fun i j => (d X j i).unop) x✝³ x✝² = 0
[PROOFSTEP]
rw [← unop_comp, X.d_comp_d, unop_zero]
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.45915, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X : HomologicalComplex Vᵒᵖ (ComplexShape.symm c)
i j : ι
hij : ¬ComplexShape.Rel c i j
⊢ (fun i j => (d X j i).unop) i j = 0
[PROOFSTEP]
simp only
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.45915, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X : HomologicalComplex Vᵒᵖ (ComplexShape.symm c)
i j : ι
hij : ¬ComplexShape.Rel c i j
⊢ (d X j i).unop = 0
[PROOFSTEP]
rw [X.shape j i hij, unop_zero]
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.45915, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X : HomologicalComplex Vᵒᵖ (ComplexShape.symm c)
x✝⁴ x✝³ x✝² : ι
x✝¹ : ComplexShape.Rel c x✝⁴ x✝³
x✝ : ComplexShape.Rel c x✝³ x✝²
⊢ (fun i j => (d X j i).unop) x✝⁴ x✝³ ≫ (fun i j => (d X j i).unop) x✝³ x✝² = 0
[PROOFSTEP]
rw [← unop_comp, X.d_comp_d, unop_zero]
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.47656, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X✝ Y✝ : (HomologicalComplex V c)ᵒᵖ
f : X✝ ⟶ Y✝
i j : ι
x✝ : ComplexShape.Rel (ComplexShape.symm c) i j
⊢ (fun i => (Hom.f f.unop i).op) i ≫ d ((fun X => HomologicalComplex.op X.unop) Y✝) i j =
    d ((fun X => HomologicalComplex.op X.unop) X✝) i j ≫ (fun i => (Hom.f f.unop i).op) j
[PROOFSTEP]
simp only [op_d, ← op_comp, f.unop.comm]
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.55812, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X✝ Y✝ : HomologicalComplex Vᵒᵖ (ComplexShape.symm c)
f : X✝ ⟶ Y✝
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ (fun i => (Hom.f f i).unop) i ≫ d (HomologicalComplex.unopSymm X✝) i j =
    d (HomologicalComplex.unopSymm Y✝) i j ≫ (fun i => (Hom.f f i).unop) j
[PROOFSTEP]
simp only [unopSymm_d, ← unop_comp, f.comm]
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.63659, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X : (HomologicalComplex V c)ᵒᵖ
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ ((fun i => Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i)) i).hom ≫
      d X.unop i j =
    d (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i j ≫
      ((fun i => Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i)) j).hom
[PROOFSTEP]
simp only [Iso.refl_hom, Category.id_comp, unopSymm_d, op_d, Quiver.Hom.unop_op, Category.comp_id]
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.63659, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
⊢ ∀ {X Y : (HomologicalComplex V c)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (HomologicalComplex V c)ᵒᵖ).map f ≫
        ((fun X =>
              Iso.op
                (Hom.isoOfComponents fun i =>
                  Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i)))
            Y).hom =
      ((fun X =>
              Iso.op
                (Hom.isoOfComponents fun i =>
                  Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i)))
            X).hom ≫
        (opFunctor V c ⋙ opInverse V c).map f
[PROOFSTEP]
intro X Y f
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.63659, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X Y : (HomologicalComplex V c)ᵒᵖ
f : X ⟶ Y
⊢ (𝟭 (HomologicalComplex V c)ᵒᵖ).map f ≫
      ((fun X =>
            Iso.op
              (Hom.isoOfComponents fun i =>
                Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i)))
          Y).hom =
    ((fun X =>
            Iso.op
              (Hom.isoOfComponents fun i =>
                Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i)))
          X).hom ≫
      (opFunctor V c ⋙ opInverse V c).map f
[PROOFSTEP]
refine' Quiver.Hom.unop_inj _
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.63659, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X Y : (HomologicalComplex V c)ᵒᵖ
f : X ⟶ Y
⊢ ((𝟭 (HomologicalComplex V c)ᵒᵖ).map f ≫
        ((fun X =>
              Iso.op
                (Hom.isoOfComponents fun i =>
                  Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i)))
            Y).hom).unop =
    (((fun X =>
              Iso.op
                (Hom.isoOfComponents fun i =>
                  Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i)))
            X).hom ≫
        (opFunctor V c ⋙ opInverse V c).map f).unop
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.63659, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X Y : (HomologicalComplex V c)ᵒᵖ
f : X ⟶ Y
x : ι
⊢ Hom.f
      ((𝟭 (HomologicalComplex V c)ᵒᵖ).map f ≫
          ((fun X =>
                Iso.op
                  (Hom.isoOfComponents fun i =>
                    Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i)))
              Y).hom).unop
      x =
    Hom.f
      (((fun X =>
                Iso.op
                  (Hom.isoOfComponents fun i =>
                    Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i)))
              X).hom ≫
          (opFunctor V c ⋙ opInverse V c).map f).unop
      x
[PROOFSTEP]
simp only [Quiver.Hom.unop_op, Functor.id_map, Iso.op_hom, Functor.comp_map, unop_comp, comp_f,
  Hom.isoOfComponents_hom_f]
[GOAL]
case h
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.63659, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X Y : (HomologicalComplex V c)ᵒᵖ
f : X ⟶ Y
x : ι
⊢ (Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op Y.unop)) x)).hom ≫
      Hom.f f.unop x =
    Hom.f ((opInverse V c).map ((opFunctor V c).map f)).unop x ≫
      (Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) x)).hom
[PROOFSTEP]
erw [Category.id_comp, Category.comp_id (f.unop.f x)]
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.82165, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X : (HomologicalComplex V c)ᵒᵖ
⊢ (opFunctor V c).map (NatTrans.app (opUnitIso V c).hom X) ≫
      NatTrans.app (opCounitIso V c).hom ((opFunctor V c).obj X) =
    𝟙 ((opFunctor V c).obj X)
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.82165, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X : (HomologicalComplex V c)ᵒᵖ
i✝ : ι
⊢ Hom.f
      ((opFunctor V c).map (NatTrans.app (opUnitIso V c).hom X) ≫
        NatTrans.app (opCounitIso V c).hom ((opFunctor V c).obj X))
      i✝ =
    Hom.f (𝟙 ((opFunctor V c).obj X)) i✝
[PROOFSTEP]
simp only [opUnitIso, opCounitIso, NatIso.ofComponents_hom_app, Iso.op_hom, comp_f, opFunctor_map_f, Quiver.Hom.unop_op,
  Hom.isoOfComponents_hom_f]
[GOAL]
case h
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.82165, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X : (HomologicalComplex V c)ᵒᵖ
i✝ : ι
⊢ (Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i✝)).hom.op ≫
      (Iso.refl (HomologicalComplex.X ((opInverse V c ⋙ opFunctor V c).obj ((opFunctor V c).obj X)) i✝)).hom =
    Hom.f (𝟙 ((opFunctor V c).obj X)) i✝
[PROOFSTEP]
exact Category.comp_id _
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.83999, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X✝ Y✝ : (HomologicalComplex Vᵒᵖ c)ᵒᵖ
f : X✝ ⟶ Y✝
i j : ι
x✝ : ComplexShape.Rel (ComplexShape.symm c) i j
⊢ (fun i => (Hom.f f.unop i).unop) i ≫ d ((fun X => HomologicalComplex.unop X.unop) Y✝) i j =
    d ((fun X => HomologicalComplex.unop X.unop) X✝) i j ≫ (fun i => (Hom.f f.unop i).unop) j
[PROOFSTEP]
simp only [unop_d, ← unop_comp, f.unop.comm]
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.92175, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X✝ Y✝ : HomologicalComplex V (ComplexShape.symm c)
f : X✝ ⟶ Y✝
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ (fun i => (Hom.f f i).op) i ≫ d (HomologicalComplex.opSymm X✝) i j =
    d (HomologicalComplex.opSymm Y✝) i j ≫ (fun i => (Hom.f f i).op) j
[PROOFSTEP]
simp only [opSymm_d, ← op_comp, f.comm]
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.100003, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X : (HomologicalComplex Vᵒᵖ c)ᵒᵖ
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ ((fun i => Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i)) i).hom ≫
      d X.unop i j =
    d (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i j ≫
      ((fun i => Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i)) j).hom
[PROOFSTEP]
simp only [Iso.refl_hom, Category.id_comp, unopSymm_d, op_d, Quiver.Hom.unop_op, Category.comp_id]
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.100003, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
⊢ ∀ {X Y : (HomologicalComplex Vᵒᵖ c)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (HomologicalComplex Vᵒᵖ c)ᵒᵖ).map f ≫
        ((fun X =>
              Iso.op
                (Hom.isoOfComponents fun i =>
                  Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i)))
            Y).hom =
      ((fun X =>
              Iso.op
                (Hom.isoOfComponents fun i =>
                  Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i)))
            X).hom ≫
        (unopFunctor V c ⋙ unopInverse V c).map f
[PROOFSTEP]
intro X Y f
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.100003, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X Y : (HomologicalComplex Vᵒᵖ c)ᵒᵖ
f : X ⟶ Y
⊢ (𝟭 (HomologicalComplex Vᵒᵖ c)ᵒᵖ).map f ≫
      ((fun X =>
            Iso.op
              (Hom.isoOfComponents fun i =>
                Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i)))
          Y).hom =
    ((fun X =>
            Iso.op
              (Hom.isoOfComponents fun i =>
                Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i)))
          X).hom ≫
      (unopFunctor V c ⋙ unopInverse V c).map f
[PROOFSTEP]
refine' Quiver.Hom.unop_inj _
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.100003, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X Y : (HomologicalComplex Vᵒᵖ c)ᵒᵖ
f : X ⟶ Y
⊢ ((𝟭 (HomologicalComplex Vᵒᵖ c)ᵒᵖ).map f ≫
        ((fun X =>
              Iso.op
                (Hom.isoOfComponents fun i =>
                  Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i)))
            Y).hom).unop =
    (((fun X =>
              Iso.op
                (Hom.isoOfComponents fun i =>
                  Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i)))
            X).hom ≫
        (unopFunctor V c ⋙ unopInverse V c).map f).unop
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.100003, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X Y : (HomologicalComplex Vᵒᵖ c)ᵒᵖ
f : X ⟶ Y
x : ι
⊢ Hom.f
      ((𝟭 (HomologicalComplex Vᵒᵖ c)ᵒᵖ).map f ≫
          ((fun X =>
                Iso.op
                  (Hom.isoOfComponents fun i =>
                    Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i)))
              Y).hom).unop
      x =
    Hom.f
      (((fun X =>
                Iso.op
                  (Hom.isoOfComponents fun i =>
                    Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) i)))
              X).hom ≫
          (unopFunctor V c ⋙ unopInverse V c).map f).unop
      x
[PROOFSTEP]
simp only [Quiver.Hom.unop_op, Functor.id_map, Iso.op_hom, Functor.comp_map, unop_comp, comp_f,
  Hom.isoOfComponents_hom_f]
[GOAL]
case h
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.100003, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X Y : (HomologicalComplex Vᵒᵖ c)ᵒᵖ
f : X ⟶ Y
x : ι
⊢ (Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op Y.unop)) x)).hom ≫
      Hom.f f.unop x =
    Hom.f ((unopInverse V c).map ((unopFunctor V c).map f)).unop x ≫
      (Iso.refl (HomologicalComplex.X (HomologicalComplex.unopSymm (HomologicalComplex.op X.unop)) x)).hom
[PROOFSTEP]
erw [Category.id_comp, Category.comp_id (f.unop.f x)]
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.118561, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X : (HomologicalComplex Vᵒᵖ c)ᵒᵖ
⊢ (unopFunctor V c).map (NatTrans.app (unopUnitIso V c).hom X) ≫
      NatTrans.app (unopCounitIso V c).hom ((unopFunctor V c).obj X) =
    𝟙 ((unopFunctor V c).obj X)
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.118561, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X : (HomologicalComplex Vᵒᵖ c)ᵒᵖ
i✝ : ι
⊢ Hom.f
      ((unopFunctor V c).map (NatTrans.app (unopUnitIso V c).hom X) ≫
        NatTrans.app (unopCounitIso V c).hom ((unopFunctor V c).obj X))
      i✝ =
    Hom.f (𝟙 ((unopFunctor V c).obj X)) i✝
[PROOFSTEP]
simp only [opUnitIso, opCounitIso, NatIso.ofComponents_hom_app, Iso.op_hom, comp_f, opFunctor_map_f, Quiver.Hom.unop_op,
  Hom.isoOfComponents_hom_f]
[GOAL]
case h
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.118561, u_2} V
c : ComplexShape ι
inst✝ : Preadditive V
X : (HomologicalComplex Vᵒᵖ c)ᵒᵖ
i✝ : ι
⊢ Hom.f ((unopFunctor V c).map (NatTrans.app (unopUnitIso V c).hom X)) i✝ ≫
      Hom.f (NatTrans.app (unopCounitIso V c).hom ((unopFunctor V c).obj X)) i✝ =
    Hom.f (𝟙 ((unopFunctor V c).obj X)) i✝
[PROOFSTEP]
exact Category.comp_id _
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.125717, u_2} V
c : ComplexShape ι
inst✝ : Abelian V
C : HomologicalComplex V c
i : ι
⊢ (dFrom C i).op ≫ (dTo C i).op = 0
[PROOFSTEP]
rw [← op_comp, C.dTo_comp_dFrom i, op_zero]
[GOAL]
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{?u.129295, u_2} V
c : ComplexShape ι
inst✝ : Abelian V
C✝ : HomologicalComplex V c
i : ι
C : HomologicalComplex Vᵒᵖ c
⊢ (dFrom C i).unop ≫ (dTo C i).unop = 0
[PROOFSTEP]
rw [← unop_comp, C.dTo_comp_dFrom i, unop_zero]
