J : Type w
C : Type u
inst✝¹ : Category C
inst✝ : HasZeroMorphisms C
F f : J → C
t : Bicone f
ht : IsColimit (toCocone t)
j : J
j' : Discrete J
⊢ (toCocone t).ι.app j' ≫ π t j = (Cofan.mk (f j) fun j' => if h : j' = j then eqToHom (_ : f j' = f j) else 0).ι.app j'
J : Type w
C : Type u
inst✝¹ : Category C
inst✝ : HasZeroMorphisms C
F f : J → C
t : Bicone f
ht : IsColimit (toCocone t)
j : J
j' : Discrete J
⊢ (toCocone t).ι.app j' ≫ π t j =
    (toCocone t).ι.app j' ≫
      IsColimit.desc ht (Cofan.mk (f j) fun j' => if h : j' = j then eqToHom (_ : f j' = f j) else 0)
rw [ht.fac]
no goals
J : Type w
C : Type u
inst✝¹ : Category C
inst✝ : HasZeroMorphisms C
F f : J → C
t : Bicone f
ht : IsColimit (toCocone t)
j : J
j' : Discrete J
⊢ (toCocone t).ι.app j' ≫ π t j = (Cofan.mk (f j) fun j' => if h : j' = j then eqToHom (_ : f j' = f j) else 0).ι.app j'
simp [t.ι_π]