[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
