[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c) c'
i : ι
j j' : ι'
w : ¬ComplexShape.Rel c' j j'
⊢ (fun j j' => Hom.f (d C j j') i) j j' = 0
[PROOFSTEP]
simp_all only [shape, zero_f]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c) c'
i i' : ι
w : ¬ComplexShape.Rel c i i'
⊢ (fun i i' => Hom.mk fun j => d (X C j) i i') i i' = 0
[PROOFSTEP]
ext j
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c) c'
i i' : ι
w : ¬ComplexShape.Rel c i i'
j : ι'
⊢ Hom.f ((fun i i' => Hom.mk fun j => d (X C j) i i') i i') j = Hom.f 0 j
[PROOFSTEP]
exact (C.X j).shape i i' w
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c) c'
i j : ι'
x✝ : ComplexShape.Rel c' i j
⊢ (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) i ≫ d ((flip V c c' ⋙ flip V c' c).obj C) i j =
    d ((𝟭 (HomologicalComplex (HomologicalComplex V c) c')).obj C) i j ≫ (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) j
[PROOFSTEP]
ext
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c) c'
i j : ι'
x✝ : ComplexShape.Rel c' i j
i✝ : ι
⊢ Hom.f ((fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) i ≫ d ((flip V c c' ⋙ flip V c' c).obj C) i j) i✝ =
    Hom.f
      (d ((𝟭 (HomologicalComplex (HomologicalComplex V c) c')).obj C) i j ≫
        (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) j)
      i✝
[PROOFSTEP]
dsimp
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c) c'
i j : ι'
x✝ : ComplexShape.Rel c' i j
i✝ : ι
⊢ 𝟙 (X (X C i) i✝) ≫ Hom.f (d C i j) i✝ = Hom.f (d C i j) i✝ ≫ 𝟙 (X (X C j) i✝)
[PROOFSTEP]
simp only [Category.id_comp, Category.comp_id]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c) c'
i j : ι'
x✝ : ComplexShape.Rel c' i j
⊢ (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) i ≫ d ((𝟭 (HomologicalComplex (HomologicalComplex V c) c')).obj C) i j =
    d ((flip V c c' ⋙ flip V c' c).obj C) i j ≫ (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) j
[PROOFSTEP]
ext
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c) c'
i j : ι'
x✝ : ComplexShape.Rel c' i j
i✝ : ι
⊢ Hom.f
      ((fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) i ≫
        d ((𝟭 (HomologicalComplex (HomologicalComplex V c) c')).obj C) i j)
      i✝ =
    Hom.f (d ((flip V c c' ⋙ flip V c' c).obj C) i j ≫ (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) j) i✝
[PROOFSTEP]
dsimp
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c) c'
i j : ι'
x✝ : ComplexShape.Rel c' i j
i✝ : ι
⊢ 𝟙 (X (X C i) i✝) ≫ Hom.f (d C i j) i✝ = Hom.f (d C i j) i✝ ≫ 𝟙 (X (X C j) i✝)
[PROOFSTEP]
simp only [Category.id_comp, Category.comp_id]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
X Y : HomologicalComplex (HomologicalComplex V c) c'
f : X ⟶ Y
⊢ (𝟭 (HomologicalComplex (HomologicalComplex V c) c')).map f ≫
      ((fun C =>
            Iso.mk (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j))
              (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j)))
          Y).hom =
    ((fun C =>
            Iso.mk (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j))
              (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j)))
          X).hom ≫
      (flip V c c' ⋙ flip V c' c).map f
[PROOFSTEP]
ext
[GOAL]
case h.h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
X Y : HomologicalComplex (HomologicalComplex V c) c'
f : X ⟶ Y
i✝¹ : ι'
i✝ : ι
⊢ Hom.f
      (Hom.f
        ((𝟭 (HomologicalComplex (HomologicalComplex V c) c')).map f ≫
          ((fun C =>
                Iso.mk (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j))
                  (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j)))
              Y).hom)
        i✝¹)
      i✝ =
    Hom.f
      (Hom.f
        (((fun C =>
                Iso.mk (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j))
                  (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j)))
              X).hom ≫
          (flip V c c' ⋙ flip V c' c).map f)
        i✝¹)
      i✝
[PROOFSTEP]
dsimp
[GOAL]
case h.h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
X Y : HomologicalComplex (HomologicalComplex V c) c'
f : X ⟶ Y
i✝¹ : ι'
i✝ : ι
⊢ Hom.f (Hom.f f i✝¹) i✝ ≫ 𝟙 (HomologicalComplex.X (HomologicalComplex.X Y i✝¹) i✝) =
    𝟙 (HomologicalComplex.X (HomologicalComplex.X X i✝¹) i✝) ≫ Hom.f (Hom.f f i✝¹) i✝
[PROOFSTEP]
simp only [Category.id_comp, Category.comp_id]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c') c
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) i ≫ d ((𝟭 (HomologicalComplex (HomologicalComplex V c') c)).obj C) i j =
    d ((flip V c' c ⋙ flip V c c').obj C) i j ≫ (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) j
[PROOFSTEP]
ext
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c') c
i j : ι
x✝ : ComplexShape.Rel c i j
i✝ : ι'
⊢ Hom.f
      ((fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) i ≫
        d ((𝟭 (HomologicalComplex (HomologicalComplex V c') c)).obj C) i j)
      i✝ =
    Hom.f (d ((flip V c' c ⋙ flip V c c').obj C) i j ≫ (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) j) i✝
[PROOFSTEP]
dsimp
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c') c
i j : ι
x✝ : ComplexShape.Rel c i j
i✝ : ι'
⊢ 𝟙 (X (X C i) i✝) ≫ Hom.f (d C i j) i✝ = Hom.f (d C i j) i✝ ≫ 𝟙 (X (X C j) i✝)
[PROOFSTEP]
simp only [Category.id_comp, Category.comp_id]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c') c
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) i ≫ d ((flip V c' c ⋙ flip V c c').obj C) i j =
    d ((𝟭 (HomologicalComplex (HomologicalComplex V c') c)).obj C) i j ≫ (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) j
[PROOFSTEP]
ext
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c') c
i j : ι
x✝ : ComplexShape.Rel c i j
i✝ : ι'
⊢ Hom.f ((fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) i ≫ d ((flip V c' c ⋙ flip V c c').obj C) i j) i✝ =
    Hom.f
      (d ((𝟭 (HomologicalComplex (HomologicalComplex V c') c)).obj C) i j ≫
        (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) j)
      i✝
[PROOFSTEP]
dsimp
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c') c
i j : ι
x✝ : ComplexShape.Rel c i j
i✝ : ι'
⊢ 𝟙 (X (X C i) i✝) ≫ Hom.f (d C i j) i✝ = Hom.f (d C i j) i✝ ≫ 𝟙 (X (X C j) i✝)
[PROOFSTEP]
simp only [Category.id_comp, Category.comp_id]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
X Y : HomologicalComplex (HomologicalComplex V c') c
f : X ⟶ Y
⊢ (flip V c' c ⋙ flip V c c').map f ≫
      ((fun C =>
            Iso.mk (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j))
              (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j)))
          Y).hom =
    ((fun C =>
            Iso.mk (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j))
              (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j)))
          X).hom ≫
      (𝟭 (HomologicalComplex (HomologicalComplex V c') c)).map f
[PROOFSTEP]
ext
[GOAL]
case h.h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
X Y : HomologicalComplex (HomologicalComplex V c') c
f : X ⟶ Y
i✝¹ : ι
i✝ : ι'
⊢ Hom.f
      (Hom.f
        ((flip V c' c ⋙ flip V c c').map f ≫
          ((fun C =>
                Iso.mk (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j))
                  (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j)))
              Y).hom)
        i✝¹)
      i✝ =
    Hom.f
      (Hom.f
        (((fun C =>
                Iso.mk (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j))
                  (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j)))
              X).hom ≫
          (𝟭 (HomologicalComplex (HomologicalComplex V c') c)).map f)
        i✝¹)
      i✝
[PROOFSTEP]
dsimp
[GOAL]
case h.h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
X Y : HomologicalComplex (HomologicalComplex V c') c
f : X ⟶ Y
i✝¹ : ι
i✝ : ι'
⊢ Hom.f (Hom.f f i✝¹) i✝ ≫ 𝟙 (HomologicalComplex.X (HomologicalComplex.X Y i✝¹) i✝) =
    𝟙 (HomologicalComplex.X (HomologicalComplex.X X i✝¹) i✝) ≫ Hom.f (Hom.f f i✝¹) i✝
[PROOFSTEP]
simp only [Category.id_comp, Category.comp_id]
