[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.96, u_1} J
inst✝¹ : Category.{?u.100, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
⊢ (IsLimit.lift h₁ (π₁.mapCone s) ≫ c.pt.f) ≫ NatTrans.app (π₂.mapCone c).π j =
    (s.pt.f ≫ IsLimit.lift h₂ (π₂.mapCone s)) ≫ NatTrans.app (π₂.mapCone c).π j
[PROOFSTEP]
have eq₁ := h₁.fac (π₁.mapCone s)
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.96, u_1} J
inst✝¹ : Category.{?u.100, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
eq₁ : ∀ (j : J), IsLimit.lift h₁ (π₁.mapCone s) ≫ NatTrans.app (π₁.mapCone c).π j = NatTrans.app (π₁.mapCone s).π j
⊢ (IsLimit.lift h₁ (π₁.mapCone s) ≫ c.pt.f) ≫ NatTrans.app (π₂.mapCone c).π j =
    (s.pt.f ≫ IsLimit.lift h₂ (π₂.mapCone s)) ≫ NatTrans.app (π₂.mapCone c).π j
[PROOFSTEP]
have eq₂ := h₂.fac (π₂.mapCone s)
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.96, u_1} J
inst✝¹ : Category.{?u.100, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
eq₁ : ∀ (j : J), IsLimit.lift h₁ (π₁.mapCone s) ≫ NatTrans.app (π₁.mapCone c).π j = NatTrans.app (π₁.mapCone s).π j
eq₂ : ∀ (j : J), IsLimit.lift h₂ (π₂.mapCone s) ≫ NatTrans.app (π₂.mapCone c).π j = NatTrans.app (π₂.mapCone s).π j
⊢ (IsLimit.lift h₁ (π₁.mapCone s) ≫ c.pt.f) ≫ NatTrans.app (π₂.mapCone c).π j =
    (s.pt.f ≫ IsLimit.lift h₂ (π₂.mapCone s)) ≫ NatTrans.app (π₂.mapCone c).π j
[PROOFSTEP]
have eq₁₂ := fun j => (c.π.app j).comm₁₂
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.96, u_1} J
inst✝¹ : Category.{?u.100, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
eq₁ : ∀ (j : J), IsLimit.lift h₁ (π₁.mapCone s) ≫ NatTrans.app (π₁.mapCone c).π j = NatTrans.app (π₁.mapCone s).π j
eq₂ : ∀ (j : J), IsLimit.lift h₂ (π₂.mapCone s) ≫ NatTrans.app (π₂.mapCone c).π j = NatTrans.app (π₂.mapCone s).π j
eq₁₂ :
  ∀ (j : J), (NatTrans.app c.π j).τ₁ ≫ (F.obj j).f = (((Functor.const J).obj c.pt).obj j).f ≫ (NatTrans.app c.π j).τ₂
⊢ (IsLimit.lift h₁ (π₁.mapCone s) ≫ c.pt.f) ≫ NatTrans.app (π₂.mapCone c).π j =
    (s.pt.f ≫ IsLimit.lift h₂ (π₂.mapCone s)) ≫ NatTrans.app (π₂.mapCone c).π j
[PROOFSTEP]
have eq₁₂' := fun j => (s.π.app j).comm₁₂
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.96, u_1} J
inst✝¹ : Category.{?u.100, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
eq₁ : ∀ (j : J), IsLimit.lift h₁ (π₁.mapCone s) ≫ NatTrans.app (π₁.mapCone c).π j = NatTrans.app (π₁.mapCone s).π j
eq₂ : ∀ (j : J), IsLimit.lift h₂ (π₂.mapCone s) ≫ NatTrans.app (π₂.mapCone c).π j = NatTrans.app (π₂.mapCone s).π j
eq₁₂ :
  ∀ (j : J), (NatTrans.app c.π j).τ₁ ≫ (F.obj j).f = (((Functor.const J).obj c.pt).obj j).f ≫ (NatTrans.app c.π j).τ₂
eq₁₂' :
  ∀ (j : J), (NatTrans.app s.π j).τ₁ ≫ (F.obj j).f = (((Functor.const J).obj s.pt).obj j).f ≫ (NatTrans.app s.π j).τ₂
⊢ (IsLimit.lift h₁ (π₁.mapCone s) ≫ c.pt.f) ≫ NatTrans.app (π₂.mapCone c).π j =
    (s.pt.f ≫ IsLimit.lift h₂ (π₂.mapCone s)) ≫ NatTrans.app (π₂.mapCone c).π j
[PROOFSTEP]
dsimp at eq₁ eq₂ eq₁₂ eq₁₂' ⊢
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.96, u_1} J
inst✝¹ : Category.{?u.100, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
eq₁ : ∀ (j : J), IsLimit.lift h₁ (π₁.mapCone s) ≫ (NatTrans.app c.π j).τ₁ = (NatTrans.app s.π j).τ₁
eq₂ : ∀ (j : J), IsLimit.lift h₂ (π₂.mapCone s) ≫ (NatTrans.app c.π j).τ₂ = (NatTrans.app s.π j).τ₂
eq₁₂ : ∀ (j : J), (NatTrans.app c.π j).τ₁ ≫ (F.obj j).f = c.pt.f ≫ (NatTrans.app c.π j).τ₂
eq₁₂' : ∀ (j : J), (NatTrans.app s.π j).τ₁ ≫ (F.obj j).f = s.pt.f ≫ (NatTrans.app s.π j).τ₂
⊢ (IsLimit.lift h₁ (π₁.mapCone s) ≫ c.pt.f) ≫ (NatTrans.app c.π j).τ₂ =
    (s.pt.f ≫ IsLimit.lift h₂ (π₂.mapCone s)) ≫ (NatTrans.app c.π j).τ₂
[PROOFSTEP]
rw [assoc, assoc, ← eq₁₂, reassoc_of% eq₁, eq₂, eq₁₂']
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.96, u_1} J
inst✝¹ : Category.{?u.100, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
⊢ (IsLimit.lift h₂ (π₂.mapCone s) ≫ c.pt.g) ≫ NatTrans.app (π₃.mapCone c).π j =
    (s.pt.g ≫ IsLimit.lift h₃ (π₃.mapCone s)) ≫ NatTrans.app (π₃.mapCone c).π j
[PROOFSTEP]
have eq₂ := h₂.fac (π₂.mapCone s)
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.96, u_1} J
inst✝¹ : Category.{?u.100, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
eq₂ : ∀ (j : J), IsLimit.lift h₂ (π₂.mapCone s) ≫ NatTrans.app (π₂.mapCone c).π j = NatTrans.app (π₂.mapCone s).π j
⊢ (IsLimit.lift h₂ (π₂.mapCone s) ≫ c.pt.g) ≫ NatTrans.app (π₃.mapCone c).π j =
    (s.pt.g ≫ IsLimit.lift h₃ (π₃.mapCone s)) ≫ NatTrans.app (π₃.mapCone c).π j
[PROOFSTEP]
have eq₃ := h₃.fac (π₃.mapCone s)
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.96, u_1} J
inst✝¹ : Category.{?u.100, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
eq₂ : ∀ (j : J), IsLimit.lift h₂ (π₂.mapCone s) ≫ NatTrans.app (π₂.mapCone c).π j = NatTrans.app (π₂.mapCone s).π j
eq₃ : ∀ (j : J), IsLimit.lift h₃ (π₃.mapCone s) ≫ NatTrans.app (π₃.mapCone c).π j = NatTrans.app (π₃.mapCone s).π j
⊢ (IsLimit.lift h₂ (π₂.mapCone s) ≫ c.pt.g) ≫ NatTrans.app (π₃.mapCone c).π j =
    (s.pt.g ≫ IsLimit.lift h₃ (π₃.mapCone s)) ≫ NatTrans.app (π₃.mapCone c).π j
[PROOFSTEP]
have eq₂₃ := fun j => (c.π.app j).comm₂₃
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.96, u_1} J
inst✝¹ : Category.{?u.100, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
eq₂ : ∀ (j : J), IsLimit.lift h₂ (π₂.mapCone s) ≫ NatTrans.app (π₂.mapCone c).π j = NatTrans.app (π₂.mapCone s).π j
eq₃ : ∀ (j : J), IsLimit.lift h₃ (π₃.mapCone s) ≫ NatTrans.app (π₃.mapCone c).π j = NatTrans.app (π₃.mapCone s).π j
eq₂₃ :
  ∀ (j : J), (NatTrans.app c.π j).τ₂ ≫ (F.obj j).g = (((Functor.const J).obj c.pt).obj j).g ≫ (NatTrans.app c.π j).τ₃
⊢ (IsLimit.lift h₂ (π₂.mapCone s) ≫ c.pt.g) ≫ NatTrans.app (π₃.mapCone c).π j =
    (s.pt.g ≫ IsLimit.lift h₃ (π₃.mapCone s)) ≫ NatTrans.app (π₃.mapCone c).π j
[PROOFSTEP]
have eq₂₃' := fun j => (s.π.app j).comm₂₃
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.96, u_1} J
inst✝¹ : Category.{?u.100, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
eq₂ : ∀ (j : J), IsLimit.lift h₂ (π₂.mapCone s) ≫ NatTrans.app (π₂.mapCone c).π j = NatTrans.app (π₂.mapCone s).π j
eq₃ : ∀ (j : J), IsLimit.lift h₃ (π₃.mapCone s) ≫ NatTrans.app (π₃.mapCone c).π j = NatTrans.app (π₃.mapCone s).π j
eq₂₃ :
  ∀ (j : J), (NatTrans.app c.π j).τ₂ ≫ (F.obj j).g = (((Functor.const J).obj c.pt).obj j).g ≫ (NatTrans.app c.π j).τ₃
eq₂₃' :
  ∀ (j : J), (NatTrans.app s.π j).τ₂ ≫ (F.obj j).g = (((Functor.const J).obj s.pt).obj j).g ≫ (NatTrans.app s.π j).τ₃
⊢ (IsLimit.lift h₂ (π₂.mapCone s) ≫ c.pt.g) ≫ NatTrans.app (π₃.mapCone c).π j =
    (s.pt.g ≫ IsLimit.lift h₃ (π₃.mapCone s)) ≫ NatTrans.app (π₃.mapCone c).π j
[PROOFSTEP]
dsimp at eq₂ eq₃ eq₂₃ eq₂₃' ⊢
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.96, u_1} J
inst✝¹ : Category.{?u.100, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
eq₂ : ∀ (j : J), IsLimit.lift h₂ (π₂.mapCone s) ≫ (NatTrans.app c.π j).τ₂ = (NatTrans.app s.π j).τ₂
eq₃ : ∀ (j : J), IsLimit.lift h₃ (π₃.mapCone s) ≫ (NatTrans.app c.π j).τ₃ = (NatTrans.app s.π j).τ₃
eq₂₃ : ∀ (j : J), (NatTrans.app c.π j).τ₂ ≫ (F.obj j).g = c.pt.g ≫ (NatTrans.app c.π j).τ₃
eq₂₃' : ∀ (j : J), (NatTrans.app s.π j).τ₂ ≫ (F.obj j).g = s.pt.g ≫ (NatTrans.app s.π j).τ₃
⊢ (IsLimit.lift h₂ (π₂.mapCone s) ≫ c.pt.g) ≫ (NatTrans.app c.π j).τ₃ =
    (s.pt.g ≫ IsLimit.lift h₃ (π₃.mapCone s)) ≫ (NatTrans.app c.π j).τ₃
[PROOFSTEP]
rw [assoc, assoc, ← eq₂₃, reassoc_of% eq₂, eq₃, eq₂₃']
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.96, u_1} J
inst✝¹ : Category.{?u.100, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
⊢ (fun s => Hom.mk (IsLimit.lift h₁ (π₁.mapCone s)) (IsLimit.lift h₂ (π₂.mapCone s)) (IsLimit.lift h₃ (π₃.mapCone s)))
        s ≫
      NatTrans.app c.π j =
    NatTrans.app s.π j
[PROOFSTEP]
ext
[GOAL]
case h₁
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.96, u_1} J
inst✝¹ : Category.{?u.100, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
⊢ ((fun s => Hom.mk (IsLimit.lift h₁ (π₁.mapCone s)) (IsLimit.lift h₂ (π₂.mapCone s)) (IsLimit.lift h₃ (π₃.mapCone s)))
          s ≫
        NatTrans.app c.π j).τ₁ =
    (NatTrans.app s.π j).τ₁
[PROOFSTEP]
apply IsLimit.fac
[GOAL]
case h₂
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.96, u_1} J
inst✝¹ : Category.{?u.100, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
⊢ ((fun s => Hom.mk (IsLimit.lift h₁ (π₁.mapCone s)) (IsLimit.lift h₂ (π₂.mapCone s)) (IsLimit.lift h₃ (π₃.mapCone s)))
          s ≫
        NatTrans.app c.π j).τ₂ =
    (NatTrans.app s.π j).τ₂
[PROOFSTEP]
apply IsLimit.fac
[GOAL]
case h₃
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.96, u_1} J
inst✝¹ : Category.{?u.100, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
⊢ ((fun s => Hom.mk (IsLimit.lift h₁ (π₁.mapCone s)) (IsLimit.lift h₂ (π₂.mapCone s)) (IsLimit.lift h₃ (π₃.mapCone s)))
          s ≫
        NatTrans.app c.π j).τ₃ =
    (NatTrans.app s.π j).τ₃
[PROOFSTEP]
apply IsLimit.fac
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.96, u_1} J
inst✝¹ : Category.{?u.100, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
⊢ m =
    (fun s => Hom.mk (IsLimit.lift h₁ (π₁.mapCone s)) (IsLimit.lift h₂ (π₂.mapCone s)) (IsLimit.lift h₃ (π₃.mapCone s)))
      s
[PROOFSTEP]
ext
[GOAL]
case h₁
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.96, u_1} J
inst✝¹ : Category.{?u.100, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
⊢ m.τ₁ =
    ((fun s =>
          Hom.mk (IsLimit.lift h₁ (π₁.mapCone s)) (IsLimit.lift h₂ (π₂.mapCone s)) (IsLimit.lift h₃ (π₃.mapCone s)))
        s).τ₁
[PROOFSTEP]
exact h₁.uniq (π₁.mapCone s) _ (fun j => π₁.congr_map (hm j))
[GOAL]
case h₂
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.96, u_1} J
inst✝¹ : Category.{?u.100, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
⊢ m.τ₂ =
    ((fun s =>
          Hom.mk (IsLimit.lift h₁ (π₁.mapCone s)) (IsLimit.lift h₂ (π₂.mapCone s)) (IsLimit.lift h₃ (π₃.mapCone s)))
        s).τ₂
[PROOFSTEP]
exact h₂.uniq (π₂.mapCone s) _ (fun j => π₂.congr_map (hm j))
[GOAL]
case h₃
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.96, u_1} J
inst✝¹ : Category.{?u.100, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
⊢ m.τ₃ =
    ((fun s =>
          Hom.mk (IsLimit.lift h₁ (π₁.mapCone s)) (IsLimit.lift h₂ (π₂.mapCone s)) (IsLimit.lift h₃ (π₃.mapCone s)))
        s).τ₃
[PROOFSTEP]
exact h₃.uniq (π₃.mapCone s) _ (fun j => π₃.congr_map (hm j))
[GOAL]
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.21982, u_1} J
inst✝⁴ : Category.{?u.21986, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
⊢ limMap (whiskerLeft F π₁Toπ₂) ≫ limMap (whiskerLeft F π₂Toπ₃) = 0
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.21982, u_1} J
inst✝⁴ : Category.{?u.21986, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
j : J
⊢ limit.π (F ⋙ π₁) j ≫ (F.obj j).f =
    (((Functor.const J).obj
              (mk (limMap (whiskerLeft F π₁Toπ₂)) (limMap (whiskerLeft F π₂Toπ₃))
                (_ : limMap (whiskerLeft F π₁Toπ₂) ≫ limMap (whiskerLeft F π₂Toπ₃) = 0))).obj
          j).f ≫
      limit.π (F ⋙ π₂) j
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.21982, u_1} J
inst✝⁴ : Category.{?u.21986, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
j : J
⊢ limit.π (F ⋙ π₂) j ≫ (F.obj j).g =
    (((Functor.const J).obj
              (mk (limMap (whiskerLeft F π₁Toπ₂)) (limMap (whiskerLeft F π₂Toπ₃))
                (_ : limMap (whiskerLeft F π₁Toπ₂) ≫ limMap (whiskerLeft F π₂Toπ₃) = 0))).obj
          j).g ≫
      limit.π (F ⋙ π₃) j
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.21982, u_1} J
inst✝⁴ : Category.{?u.21986, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ ((Functor.const J).obj
            (mk (limMap (whiskerLeft F π₁Toπ₂)) (limMap (whiskerLeft F π₂Toπ₃))
              (_ : limMap (whiskerLeft F π₁Toπ₂) ≫ limMap (whiskerLeft F π₂Toπ₃) = 0))).map
        f ≫
      (fun j => Hom.mk (limit.π (F ⋙ π₁) j) (limit.π (F ⋙ π₂) j) (limit.π (F ⋙ π₃) j)) x✝ =
    (fun j => Hom.mk (limit.π (F ⋙ π₁) j) (limit.π (F ⋙ π₂) j) (limit.π (F ⋙ π₃) j)) x✝¹ ≫ F.map f
[PROOFSTEP]
ext
[GOAL]
case h₁
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.21982, u_1} J
inst✝⁴ : Category.{?u.21986, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (((Functor.const J).obj
              (mk (limMap (whiskerLeft F π₁Toπ₂)) (limMap (whiskerLeft F π₂Toπ₃))
                (_ : limMap (whiskerLeft F π₁Toπ₂) ≫ limMap (whiskerLeft F π₂Toπ₃) = 0))).map
          f ≫
        (fun j => Hom.mk (limit.π (F ⋙ π₁) j) (limit.π (F ⋙ π₂) j) (limit.π (F ⋙ π₃) j)) x✝).τ₁ =
    ((fun j => Hom.mk (limit.π (F ⋙ π₁) j) (limit.π (F ⋙ π₂) j) (limit.π (F ⋙ π₃) j)) x✝¹ ≫ F.map f).τ₁
case h₂
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.21982, u_1} J
inst✝⁴ : Category.{?u.21986, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (((Functor.const J).obj
              (mk (limMap (whiskerLeft F π₁Toπ₂)) (limMap (whiskerLeft F π₂Toπ₃))
                (_ : limMap (whiskerLeft F π₁Toπ₂) ≫ limMap (whiskerLeft F π₂Toπ₃) = 0))).map
          f ≫
        (fun j => Hom.mk (limit.π (F ⋙ π₁) j) (limit.π (F ⋙ π₂) j) (limit.π (F ⋙ π₃) j)) x✝).τ₂ =
    ((fun j => Hom.mk (limit.π (F ⋙ π₁) j) (limit.π (F ⋙ π₂) j) (limit.π (F ⋙ π₃) j)) x✝¹ ≫ F.map f).τ₂
case h₃
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.21982, u_1} J
inst✝⁴ : Category.{?u.21986, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (((Functor.const J).obj
              (mk (limMap (whiskerLeft F π₁Toπ₂)) (limMap (whiskerLeft F π₂Toπ₃))
                (_ : limMap (whiskerLeft F π₁Toπ₂) ≫ limMap (whiskerLeft F π₂Toπ₃) = 0))).map
          f ≫
        (fun j => Hom.mk (limit.π (F ⋙ π₁) j) (limit.π (F ⋙ π₂) j) (limit.π (F ⋙ π₃) j)) x✝).τ₃ =
    ((fun j => Hom.mk (limit.π (F ⋙ π₁) j) (limit.π (F ⋙ π₂) j) (limit.π (F ⋙ π₃) j)) x✝¹ ≫ F.map f).τ₃
[PROOFSTEP]
all_goals
  dsimp
  erw [id_comp, limit.w]
[GOAL]
case h₁
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.21982, u_1} J
inst✝⁴ : Category.{?u.21986, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (((Functor.const J).obj
              (mk (limMap (whiskerLeft F π₁Toπ₂)) (limMap (whiskerLeft F π₂Toπ₃))
                (_ : limMap (whiskerLeft F π₁Toπ₂) ≫ limMap (whiskerLeft F π₂Toπ₃) = 0))).map
          f ≫
        (fun j => Hom.mk (limit.π (F ⋙ π₁) j) (limit.π (F ⋙ π₂) j) (limit.π (F ⋙ π₃) j)) x✝).τ₁ =
    ((fun j => Hom.mk (limit.π (F ⋙ π₁) j) (limit.π (F ⋙ π₂) j) (limit.π (F ⋙ π₃) j)) x✝¹ ≫ F.map f).τ₁
[PROOFSTEP]
dsimp
[GOAL]
case h₁
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.21982, u_1} J
inst✝⁴ : Category.{?u.21986, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ 𝟙 (limit (F ⋙ π₁)) ≫ limit.π (F ⋙ π₁) x✝ = limit.π (F ⋙ π₁) x✝¹ ≫ (F.map f).τ₁
[PROOFSTEP]
erw [id_comp, limit.w]
[GOAL]
case h₂
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.21982, u_1} J
inst✝⁴ : Category.{?u.21986, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (((Functor.const J).obj
              (mk (limMap (whiskerLeft F π₁Toπ₂)) (limMap (whiskerLeft F π₂Toπ₃))
                (_ : limMap (whiskerLeft F π₁Toπ₂) ≫ limMap (whiskerLeft F π₂Toπ₃) = 0))).map
          f ≫
        (fun j => Hom.mk (limit.π (F ⋙ π₁) j) (limit.π (F ⋙ π₂) j) (limit.π (F ⋙ π₃) j)) x✝).τ₂ =
    ((fun j => Hom.mk (limit.π (F ⋙ π₁) j) (limit.π (F ⋙ π₂) j) (limit.π (F ⋙ π₃) j)) x✝¹ ≫ F.map f).τ₂
[PROOFSTEP]
dsimp
[GOAL]
case h₂
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.21982, u_1} J
inst✝⁴ : Category.{?u.21986, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ 𝟙 (limit (F ⋙ π₂)) ≫ limit.π (F ⋙ π₂) x✝ = limit.π (F ⋙ π₂) x✝¹ ≫ (F.map f).τ₂
[PROOFSTEP]
erw [id_comp, limit.w]
[GOAL]
case h₃
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.21982, u_1} J
inst✝⁴ : Category.{?u.21986, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (((Functor.const J).obj
              (mk (limMap (whiskerLeft F π₁Toπ₂)) (limMap (whiskerLeft F π₂Toπ₃))
                (_ : limMap (whiskerLeft F π₁Toπ₂) ≫ limMap (whiskerLeft F π₂Toπ₃) = 0))).map
          f ≫
        (fun j => Hom.mk (limit.π (F ⋙ π₁) j) (limit.π (F ⋙ π₂) j) (limit.π (F ⋙ π₃) j)) x✝).τ₃ =
    ((fun j => Hom.mk (limit.π (F ⋙ π₁) j) (limit.π (F ⋙ π₂) j) (limit.π (F ⋙ π₃) j)) x✝¹ ≫ F.map f).τ₃
[PROOFSTEP]
dsimp
[GOAL]
case h₃
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.21982, u_1} J
inst✝⁴ : Category.{?u.21986, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ 𝟙 (limit (F ⋙ π₃)) ≫ limit.π (F ⋙ π₃) x✝ = limit.π (F ⋙ π₃) x✝¹ ≫ (F.map f).τ₃
[PROOFSTEP]
erw [id_comp, limit.w]
[GOAL]
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.38492, u_1} J
inst✝⁴ : Category.{?u.38496, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
⊢ ∀ (j : J),
    NatTrans.app (limit.cone (F ⋙ π₁)).π j =
      (Iso.refl (limit.cone (F ⋙ π₁)).pt).hom ≫ NatTrans.app (π₁.mapCone (limitCone F)).π j
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.44003, u_1} J
inst✝⁴ : Category.{?u.44007, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
⊢ ∀ (j : J),
    NatTrans.app (limit.cone (F ⋙ π₂)).π j =
      (Iso.refl (limit.cone (F ⋙ π₂)).pt).hom ≫ NatTrans.app (π₂.mapCone (limitCone F)).π j
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.49514, u_1} J
inst✝⁴ : Category.{?u.49518, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
⊢ ∀ (j : J),
    NatTrans.app (limit.cone (F ⋙ π₃)).π j =
      (Iso.refl (limit.cone (F ⋙ π₃)).pt).hom ≫ NatTrans.app (π₃.mapCone (limitCone F)).π j
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.84519, u_1} J
inst✝¹ : Category.{?u.84523, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
⊢ NatTrans.app (π₁.mapCocone c).ι j ≫ IsColimit.desc h₁ (π₁.mapCocone s) ≫ s.pt.f =
    NatTrans.app (π₁.mapCocone c).ι j ≫ c.pt.f ≫ IsColimit.desc h₂ (π₂.mapCocone s)
[PROOFSTEP]
have eq₁ := h₁.fac (π₁.mapCocone s)
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.84519, u_1} J
inst✝¹ : Category.{?u.84523, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
eq₁ :
  ∀ (j : J), NatTrans.app (π₁.mapCocone c).ι j ≫ IsColimit.desc h₁ (π₁.mapCocone s) = NatTrans.app (π₁.mapCocone s).ι j
⊢ NatTrans.app (π₁.mapCocone c).ι j ≫ IsColimit.desc h₁ (π₁.mapCocone s) ≫ s.pt.f =
    NatTrans.app (π₁.mapCocone c).ι j ≫ c.pt.f ≫ IsColimit.desc h₂ (π₂.mapCocone s)
[PROOFSTEP]
have eq₂ := h₂.fac (π₂.mapCocone s)
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.84519, u_1} J
inst✝¹ : Category.{?u.84523, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
eq₁ :
  ∀ (j : J), NatTrans.app (π₁.mapCocone c).ι j ≫ IsColimit.desc h₁ (π₁.mapCocone s) = NatTrans.app (π₁.mapCocone s).ι j
eq₂ :
  ∀ (j : J), NatTrans.app (π₂.mapCocone c).ι j ≫ IsColimit.desc h₂ (π₂.mapCocone s) = NatTrans.app (π₂.mapCocone s).ι j
⊢ NatTrans.app (π₁.mapCocone c).ι j ≫ IsColimit.desc h₁ (π₁.mapCocone s) ≫ s.pt.f =
    NatTrans.app (π₁.mapCocone c).ι j ≫ c.pt.f ≫ IsColimit.desc h₂ (π₂.mapCocone s)
[PROOFSTEP]
have eq₁₂ := fun j => (c.ι.app j).comm₁₂
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.84519, u_1} J
inst✝¹ : Category.{?u.84523, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
eq₁ :
  ∀ (j : J), NatTrans.app (π₁.mapCocone c).ι j ≫ IsColimit.desc h₁ (π₁.mapCocone s) = NatTrans.app (π₁.mapCocone s).ι j
eq₂ :
  ∀ (j : J), NatTrans.app (π₂.mapCocone c).ι j ≫ IsColimit.desc h₂ (π₂.mapCocone s) = NatTrans.app (π₂.mapCocone s).ι j
eq₁₂ :
  ∀ (j : J), (NatTrans.app c.ι j).τ₁ ≫ (((Functor.const J).obj c.pt).obj j).f = (F.obj j).f ≫ (NatTrans.app c.ι j).τ₂
⊢ NatTrans.app (π₁.mapCocone c).ι j ≫ IsColimit.desc h₁ (π₁.mapCocone s) ≫ s.pt.f =
    NatTrans.app (π₁.mapCocone c).ι j ≫ c.pt.f ≫ IsColimit.desc h₂ (π₂.mapCocone s)
[PROOFSTEP]
have eq₁₂' := fun j => (s.ι.app j).comm₁₂
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.84519, u_1} J
inst✝¹ : Category.{?u.84523, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
eq₁ :
  ∀ (j : J), NatTrans.app (π₁.mapCocone c).ι j ≫ IsColimit.desc h₁ (π₁.mapCocone s) = NatTrans.app (π₁.mapCocone s).ι j
eq₂ :
  ∀ (j : J), NatTrans.app (π₂.mapCocone c).ι j ≫ IsColimit.desc h₂ (π₂.mapCocone s) = NatTrans.app (π₂.mapCocone s).ι j
eq₁₂ :
  ∀ (j : J), (NatTrans.app c.ι j).τ₁ ≫ (((Functor.const J).obj c.pt).obj j).f = (F.obj j).f ≫ (NatTrans.app c.ι j).τ₂
eq₁₂' :
  ∀ (j : J), (NatTrans.app s.ι j).τ₁ ≫ (((Functor.const J).obj s.pt).obj j).f = (F.obj j).f ≫ (NatTrans.app s.ι j).τ₂
⊢ NatTrans.app (π₁.mapCocone c).ι j ≫ IsColimit.desc h₁ (π₁.mapCocone s) ≫ s.pt.f =
    NatTrans.app (π₁.mapCocone c).ι j ≫ c.pt.f ≫ IsColimit.desc h₂ (π₂.mapCocone s)
[PROOFSTEP]
dsimp at eq₁ eq₂ eq₁₂ eq₁₂' ⊢
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.84519, u_1} J
inst✝¹ : Category.{?u.84523, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
eq₁ : ∀ (j : J), (NatTrans.app c.ι j).τ₁ ≫ IsColimit.desc h₁ (π₁.mapCocone s) = (NatTrans.app s.ι j).τ₁
eq₂ : ∀ (j : J), (NatTrans.app c.ι j).τ₂ ≫ IsColimit.desc h₂ (π₂.mapCocone s) = (NatTrans.app s.ι j).τ₂
eq₁₂ : ∀ (j : J), (NatTrans.app c.ι j).τ₁ ≫ c.pt.f = (F.obj j).f ≫ (NatTrans.app c.ι j).τ₂
eq₁₂' : ∀ (j : J), (NatTrans.app s.ι j).τ₁ ≫ s.pt.f = (F.obj j).f ≫ (NatTrans.app s.ι j).τ₂
⊢ (NatTrans.app c.ι j).τ₁ ≫ IsColimit.desc h₁ (π₁.mapCocone s) ≫ s.pt.f =
    (NatTrans.app c.ι j).τ₁ ≫ c.pt.f ≫ IsColimit.desc h₂ (π₂.mapCocone s)
[PROOFSTEP]
rw [reassoc_of% (eq₁ j), eq₁₂', reassoc_of% eq₁₂, eq₂]
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.84519, u_1} J
inst✝¹ : Category.{?u.84523, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
⊢ NatTrans.app (π₂.mapCocone c).ι j ≫ IsColimit.desc h₂ (π₂.mapCocone s) ≫ s.pt.g =
    NatTrans.app (π₂.mapCocone c).ι j ≫ c.pt.g ≫ IsColimit.desc h₃ (π₃.mapCocone s)
[PROOFSTEP]
have eq₂ := h₂.fac (π₂.mapCocone s)
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.84519, u_1} J
inst✝¹ : Category.{?u.84523, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
eq₂ :
  ∀ (j : J), NatTrans.app (π₂.mapCocone c).ι j ≫ IsColimit.desc h₂ (π₂.mapCocone s) = NatTrans.app (π₂.mapCocone s).ι j
⊢ NatTrans.app (π₂.mapCocone c).ι j ≫ IsColimit.desc h₂ (π₂.mapCocone s) ≫ s.pt.g =
    NatTrans.app (π₂.mapCocone c).ι j ≫ c.pt.g ≫ IsColimit.desc h₃ (π₃.mapCocone s)
[PROOFSTEP]
have eq₃ := h₃.fac (π₃.mapCocone s)
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.84519, u_1} J
inst✝¹ : Category.{?u.84523, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
eq₂ :
  ∀ (j : J), NatTrans.app (π₂.mapCocone c).ι j ≫ IsColimit.desc h₂ (π₂.mapCocone s) = NatTrans.app (π₂.mapCocone s).ι j
eq₃ :
  ∀ (j : J), NatTrans.app (π₃.mapCocone c).ι j ≫ IsColimit.desc h₃ (π₃.mapCocone s) = NatTrans.app (π₃.mapCocone s).ι j
⊢ NatTrans.app (π₂.mapCocone c).ι j ≫ IsColimit.desc h₂ (π₂.mapCocone s) ≫ s.pt.g =
    NatTrans.app (π₂.mapCocone c).ι j ≫ c.pt.g ≫ IsColimit.desc h₃ (π₃.mapCocone s)
[PROOFSTEP]
have eq₂₃ := fun j => (c.ι.app j).comm₂₃
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.84519, u_1} J
inst✝¹ : Category.{?u.84523, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
eq₂ :
  ∀ (j : J), NatTrans.app (π₂.mapCocone c).ι j ≫ IsColimit.desc h₂ (π₂.mapCocone s) = NatTrans.app (π₂.mapCocone s).ι j
eq₃ :
  ∀ (j : J), NatTrans.app (π₃.mapCocone c).ι j ≫ IsColimit.desc h₃ (π₃.mapCocone s) = NatTrans.app (π₃.mapCocone s).ι j
eq₂₃ :
  ∀ (j : J), (NatTrans.app c.ι j).τ₂ ≫ (((Functor.const J).obj c.pt).obj j).g = (F.obj j).g ≫ (NatTrans.app c.ι j).τ₃
⊢ NatTrans.app (π₂.mapCocone c).ι j ≫ IsColimit.desc h₂ (π₂.mapCocone s) ≫ s.pt.g =
    NatTrans.app (π₂.mapCocone c).ι j ≫ c.pt.g ≫ IsColimit.desc h₃ (π₃.mapCocone s)
[PROOFSTEP]
have eq₂₃' := fun j => (s.ι.app j).comm₂₃
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.84519, u_1} J
inst✝¹ : Category.{?u.84523, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
eq₂ :
  ∀ (j : J), NatTrans.app (π₂.mapCocone c).ι j ≫ IsColimit.desc h₂ (π₂.mapCocone s) = NatTrans.app (π₂.mapCocone s).ι j
eq₃ :
  ∀ (j : J), NatTrans.app (π₃.mapCocone c).ι j ≫ IsColimit.desc h₃ (π₃.mapCocone s) = NatTrans.app (π₃.mapCocone s).ι j
eq₂₃ :
  ∀ (j : J), (NatTrans.app c.ι j).τ₂ ≫ (((Functor.const J).obj c.pt).obj j).g = (F.obj j).g ≫ (NatTrans.app c.ι j).τ₃
eq₂₃' :
  ∀ (j : J), (NatTrans.app s.ι j).τ₂ ≫ (((Functor.const J).obj s.pt).obj j).g = (F.obj j).g ≫ (NatTrans.app s.ι j).τ₃
⊢ NatTrans.app (π₂.mapCocone c).ι j ≫ IsColimit.desc h₂ (π₂.mapCocone s) ≫ s.pt.g =
    NatTrans.app (π₂.mapCocone c).ι j ≫ c.pt.g ≫ IsColimit.desc h₃ (π₃.mapCocone s)
[PROOFSTEP]
dsimp at eq₂ eq₃ eq₂₃ eq₂₃' ⊢
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.84519, u_1} J
inst✝¹ : Category.{?u.84523, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
eq₂ : ∀ (j : J), (NatTrans.app c.ι j).τ₂ ≫ IsColimit.desc h₂ (π₂.mapCocone s) = (NatTrans.app s.ι j).τ₂
eq₃ : ∀ (j : J), (NatTrans.app c.ι j).τ₃ ≫ IsColimit.desc h₃ (π₃.mapCocone s) = (NatTrans.app s.ι j).τ₃
eq₂₃ : ∀ (j : J), (NatTrans.app c.ι j).τ₂ ≫ c.pt.g = (F.obj j).g ≫ (NatTrans.app c.ι j).τ₃
eq₂₃' : ∀ (j : J), (NatTrans.app s.ι j).τ₂ ≫ s.pt.g = (F.obj j).g ≫ (NatTrans.app s.ι j).τ₃
⊢ (NatTrans.app c.ι j).τ₂ ≫ IsColimit.desc h₂ (π₂.mapCocone s) ≫ s.pt.g =
    (NatTrans.app c.ι j).τ₂ ≫ c.pt.g ≫ IsColimit.desc h₃ (π₃.mapCocone s)
[PROOFSTEP]
rw [reassoc_of% (eq₂ j), eq₂₃', reassoc_of% eq₂₃, eq₃]
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.84519, u_1} J
inst✝¹ : Category.{?u.84523, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
⊢ NatTrans.app c.ι j ≫
      (fun s =>
          Hom.mk (IsColimit.desc h₁ (π₁.mapCocone s)) (IsColimit.desc h₂ (π₂.mapCocone s))
            (IsColimit.desc h₃ (π₃.mapCocone s)))
        s =
    NatTrans.app s.ι j
[PROOFSTEP]
ext
[GOAL]
case h₁
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.84519, u_1} J
inst✝¹ : Category.{?u.84523, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
⊢ (NatTrans.app c.ι j ≫
        (fun s =>
            Hom.mk (IsColimit.desc h₁ (π₁.mapCocone s)) (IsColimit.desc h₂ (π₂.mapCocone s))
              (IsColimit.desc h₃ (π₃.mapCocone s)))
          s).τ₁ =
    (NatTrans.app s.ι j).τ₁
[PROOFSTEP]
apply IsColimit.fac h₁
[GOAL]
case h₂
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.84519, u_1} J
inst✝¹ : Category.{?u.84523, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
⊢ (NatTrans.app c.ι j ≫
        (fun s =>
            Hom.mk (IsColimit.desc h₁ (π₁.mapCocone s)) (IsColimit.desc h₂ (π₂.mapCocone s))
              (IsColimit.desc h₃ (π₃.mapCocone s)))
          s).τ₂ =
    (NatTrans.app s.ι j).τ₂
[PROOFSTEP]
apply IsColimit.fac h₂
[GOAL]
case h₃
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.84519, u_1} J
inst✝¹ : Category.{?u.84523, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
⊢ (NatTrans.app c.ι j ≫
        (fun s =>
            Hom.mk (IsColimit.desc h₁ (π₁.mapCocone s)) (IsColimit.desc h₂ (π₂.mapCocone s))
              (IsColimit.desc h₃ (π₃.mapCocone s)))
          s).τ₃ =
    (NatTrans.app s.ι j).τ₃
[PROOFSTEP]
apply IsColimit.fac h₃
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.84519, u_1} J
inst✝¹ : Category.{?u.84523, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), NatTrans.app c.ι j ≫ m = NatTrans.app s.ι j
⊢ m =
    (fun s =>
        Hom.mk (IsColimit.desc h₁ (π₁.mapCocone s)) (IsColimit.desc h₂ (π₂.mapCocone s))
          (IsColimit.desc h₃ (π₃.mapCocone s)))
      s
[PROOFSTEP]
ext
[GOAL]
case h₁
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.84519, u_1} J
inst✝¹ : Category.{?u.84523, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), NatTrans.app c.ι j ≫ m = NatTrans.app s.ι j
⊢ m.τ₁ =
    ((fun s =>
          Hom.mk (IsColimit.desc h₁ (π₁.mapCocone s)) (IsColimit.desc h₂ (π₂.mapCocone s))
            (IsColimit.desc h₃ (π₃.mapCocone s)))
        s).τ₁
[PROOFSTEP]
exact h₁.uniq (π₁.mapCocone s) _ (fun j => π₁.congr_map (hm j))
[GOAL]
case h₂
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.84519, u_1} J
inst✝¹ : Category.{?u.84523, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), NatTrans.app c.ι j ≫ m = NatTrans.app s.ι j
⊢ m.τ₂ =
    ((fun s =>
          Hom.mk (IsColimit.desc h₁ (π₁.mapCocone s)) (IsColimit.desc h₂ (π₂.mapCocone s))
            (IsColimit.desc h₃ (π₃.mapCocone s)))
        s).τ₂
[PROOFSTEP]
exact h₂.uniq (π₂.mapCocone s) _ (fun j => π₂.congr_map (hm j))
[GOAL]
case h₃
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.84519, u_1} J
inst✝¹ : Category.{?u.84523, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), NatTrans.app c.ι j ≫ m = NatTrans.app s.ι j
⊢ m.τ₃ =
    ((fun s =>
          Hom.mk (IsColimit.desc h₁ (π₁.mapCocone s)) (IsColimit.desc h₂ (π₂.mapCocone s))
            (IsColimit.desc h₃ (π₃.mapCocone s)))
        s).τ₃
[PROOFSTEP]
exact h₃.uniq (π₃.mapCocone s) _ (fun j => π₃.congr_map (hm j))
[GOAL]
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.105288, u_1} J
inst✝⁴ : Category.{?u.105292, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasColimit (F ⋙ π₁)
inst✝¹ : HasColimit (F ⋙ π₂)
inst✝ : HasColimit (F ⋙ π₃)
⊢ colimMap (whiskerLeft F π₁Toπ₂) ≫ colimMap (whiskerLeft F π₂Toπ₃) = 0
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.105288, u_1} J
inst✝⁴ : Category.{?u.105292, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasColimit (F ⋙ π₁)
inst✝¹ : HasColimit (F ⋙ π₂)
inst✝ : HasColimit (F ⋙ π₃)
j : J
⊢ colimit.ι (F ⋙ π₁) j ≫
      (((Functor.const J).obj
              (mk (colimMap (whiskerLeft F π₁Toπ₂)) (colimMap (whiskerLeft F π₂Toπ₃))
                (_ : colimMap (whiskerLeft F π₁Toπ₂) ≫ colimMap (whiskerLeft F π₂Toπ₃) = 0))).obj
          j).f =
    (F.obj j).f ≫ colimit.ι (F ⋙ π₂) j
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.105288, u_1} J
inst✝⁴ : Category.{?u.105292, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasColimit (F ⋙ π₁)
inst✝¹ : HasColimit (F ⋙ π₂)
inst✝ : HasColimit (F ⋙ π₃)
j : J
⊢ colimit.ι (F ⋙ π₂) j ≫
      (((Functor.const J).obj
              (mk (colimMap (whiskerLeft F π₁Toπ₂)) (colimMap (whiskerLeft F π₂Toπ₃))
                (_ : colimMap (whiskerLeft F π₁Toπ₂) ≫ colimMap (whiskerLeft F π₂Toπ₃) = 0))).obj
          j).g =
    (F.obj j).g ≫ colimit.ι (F ⋙ π₃) j
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.105288, u_1} J
inst✝⁴ : Category.{?u.105292, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasColimit (F ⋙ π₁)
inst✝¹ : HasColimit (F ⋙ π₂)
inst✝ : HasColimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ F.map f ≫ (fun j => Hom.mk (colimit.ι (F ⋙ π₁) j) (colimit.ι (F ⋙ π₂) j) (colimit.ι (F ⋙ π₃) j)) x✝ =
    (fun j => Hom.mk (colimit.ι (F ⋙ π₁) j) (colimit.ι (F ⋙ π₂) j) (colimit.ι (F ⋙ π₃) j)) x✝¹ ≫
      ((Functor.const J).obj
            (mk (colimMap (whiskerLeft F π₁Toπ₂)) (colimMap (whiskerLeft F π₂Toπ₃))
              (_ : colimMap (whiskerLeft F π₁Toπ₂) ≫ colimMap (whiskerLeft F π₂Toπ₃) = 0))).map
        f
[PROOFSTEP]
ext
[GOAL]
case h₁
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.105288, u_1} J
inst✝⁴ : Category.{?u.105292, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasColimit (F ⋙ π₁)
inst✝¹ : HasColimit (F ⋙ π₂)
inst✝ : HasColimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (F.map f ≫ (fun j => Hom.mk (colimit.ι (F ⋙ π₁) j) (colimit.ι (F ⋙ π₂) j) (colimit.ι (F ⋙ π₃) j)) x✝).τ₁ =
    ((fun j => Hom.mk (colimit.ι (F ⋙ π₁) j) (colimit.ι (F ⋙ π₂) j) (colimit.ι (F ⋙ π₃) j)) x✝¹ ≫
        ((Functor.const J).obj
              (mk (colimMap (whiskerLeft F π₁Toπ₂)) (colimMap (whiskerLeft F π₂Toπ₃))
                (_ : colimMap (whiskerLeft F π₁Toπ₂) ≫ colimMap (whiskerLeft F π₂Toπ₃) = 0))).map
          f).τ₁
[PROOFSTEP]
dsimp
[GOAL]
case h₁
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.105288, u_1} J
inst✝⁴ : Category.{?u.105292, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasColimit (F ⋙ π₁)
inst✝¹ : HasColimit (F ⋙ π₂)
inst✝ : HasColimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (F.map f).τ₁ ≫ colimit.ι (F ⋙ π₁) x✝ = colimit.ι (F ⋙ π₁) x✝¹ ≫ 𝟙 (colimit (F ⋙ π₁))
[PROOFSTEP]
erw [comp_id, colimit.w (F ⋙ π₁)]
[GOAL]
case h₂
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.105288, u_1} J
inst✝⁴ : Category.{?u.105292, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasColimit (F ⋙ π₁)
inst✝¹ : HasColimit (F ⋙ π₂)
inst✝ : HasColimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (F.map f ≫ (fun j => Hom.mk (colimit.ι (F ⋙ π₁) j) (colimit.ι (F ⋙ π₂) j) (colimit.ι (F ⋙ π₃) j)) x✝).τ₂ =
    ((fun j => Hom.mk (colimit.ι (F ⋙ π₁) j) (colimit.ι (F ⋙ π₂) j) (colimit.ι (F ⋙ π₃) j)) x✝¹ ≫
        ((Functor.const J).obj
              (mk (colimMap (whiskerLeft F π₁Toπ₂)) (colimMap (whiskerLeft F π₂Toπ₃))
                (_ : colimMap (whiskerLeft F π₁Toπ₂) ≫ colimMap (whiskerLeft F π₂Toπ₃) = 0))).map
          f).τ₂
[PROOFSTEP]
dsimp
[GOAL]
case h₂
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.105288, u_1} J
inst✝⁴ : Category.{?u.105292, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasColimit (F ⋙ π₁)
inst✝¹ : HasColimit (F ⋙ π₂)
inst✝ : HasColimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (F.map f).τ₂ ≫ colimit.ι (F ⋙ π₂) x✝ = colimit.ι (F ⋙ π₂) x✝¹ ≫ 𝟙 (colimit (F ⋙ π₂))
[PROOFSTEP]
erw [comp_id, colimit.w (F ⋙ π₂)]
[GOAL]
case h₃
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.105288, u_1} J
inst✝⁴ : Category.{?u.105292, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasColimit (F ⋙ π₁)
inst✝¹ : HasColimit (F ⋙ π₂)
inst✝ : HasColimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (F.map f ≫ (fun j => Hom.mk (colimit.ι (F ⋙ π₁) j) (colimit.ι (F ⋙ π₂) j) (colimit.ι (F ⋙ π₃) j)) x✝).τ₃ =
    ((fun j => Hom.mk (colimit.ι (F ⋙ π₁) j) (colimit.ι (F ⋙ π₂) j) (colimit.ι (F ⋙ π₃) j)) x✝¹ ≫
        ((Functor.const J).obj
              (mk (colimMap (whiskerLeft F π₁Toπ₂)) (colimMap (whiskerLeft F π₂Toπ₃))
                (_ : colimMap (whiskerLeft F π₁Toπ₂) ≫ colimMap (whiskerLeft F π₂Toπ₃) = 0))).map
          f).τ₃
[PROOFSTEP]
dsimp
[GOAL]
case h₃
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.105288, u_1} J
inst✝⁴ : Category.{?u.105292, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasColimit (F ⋙ π₁)
inst✝¹ : HasColimit (F ⋙ π₂)
inst✝ : HasColimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (F.map f).τ₃ ≫ colimit.ι (F ⋙ π₃) x✝ = colimit.ι (F ⋙ π₃) x✝¹ ≫ 𝟙 (colimit (F ⋙ π₃))
[PROOFSTEP]
erw [comp_id, colimit.w (F ⋙ π₃)]
[GOAL]
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.123211, u_1} J
inst✝⁴ : Category.{?u.123215, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasColimit (F ⋙ π₁)
inst✝¹ : HasColimit (F ⋙ π₂)
inst✝ : HasColimit (F ⋙ π₃)
⊢ ∀ (j : J),
    NatTrans.app (colimit.cocone (F ⋙ π₁)).ι j ≫ (Iso.refl (colimit.cocone (F ⋙ π₁)).pt).hom =
      NatTrans.app (π₁.mapCocone (colimitCocone F)).ι j
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.128766, u_1} J
inst✝⁴ : Category.{?u.128770, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasColimit (F ⋙ π₁)
inst✝¹ : HasColimit (F ⋙ π₂)
inst✝ : HasColimit (F ⋙ π₃)
⊢ ∀ (j : J),
    NatTrans.app (colimit.cocone (F ⋙ π₂)).ι j ≫ (Iso.refl (colimit.cocone (F ⋙ π₂)).pt).hom =
      NatTrans.app (π₂.mapCocone (colimitCocone F)).ι j
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{?u.134321, u_1} J
inst✝⁴ : Category.{?u.134325, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasColimit (F ⋙ π₁)
inst✝¹ : HasColimit (F ⋙ π₂)
inst✝ : HasColimit (F ⋙ π₃)
⊢ ∀ (j : J),
    NatTrans.app (colimit.cocone (F ⋙ π₃)).ι j ≫ (Iso.refl (colimit.cocone (F ⋙ π₃)).pt).hom =
      NatTrans.app (π₃.mapCocone (colimitCocone F)).ι j
[PROOFSTEP]
aesop_cat


[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]