case w
C✝ : Type u₁
inst✝³ : Category C✝
J : Type u_1
inst✝² : Category J
C : Type u_3
inst✝¹ : Category C
inst✝ : HasInitial C
j : J
⊢ ∀ (j_1 : Discrete PEmpty),
    colimit.ι (Functor.empty C) j_1 ≫ colimit.ι ((Functor.const J).obj (⊥_ C)) j ≫ colimitConstInitial.hom =
      colimit.ι (Functor.empty C) j_1 ≫ initial.to (⊥_ C)
C✝ : Type u₁
inst✝³ : Category C✝
J : Type u_1
inst✝² : Category J
C : Type u_3
inst✝¹ : Category C
inst✝ : HasInitial C
j : J
⊢ colimit.ι ((Functor.const J).obj (⊥_ C)) j ≫ colimitConstInitial.hom = initial.to (⊥_ C)
apply Limits.colimit.hom_ext
no goals
case w
C✝ : Type u₁
inst✝³ : Category C✝
J : Type u_1
inst✝² : Category J
C : Type u_3
inst✝¹ : Category C
inst✝ : HasInitial C
j : J
⊢ ∀ (j_1 : Discrete PEmpty),
    colimit.ι (Functor.empty C) j_1 ≫ colimit.ι ((Functor.const J).obj (⊥_ C)) j ≫ colimitConstInitial.hom =
      colimit.ι (Functor.empty C) j_1 ≫ initial.to (⊥_ C)
aesop_cat