case mk
C : Type u
inst✝² : Category C
inst✝¹ : Preadditive C
J : Type
inst✝ : Fintype J
f : J → C
b : Bicone f
i : Bicone.IsBilimit b
as✝ : J
⊢ (∑ j : J, Bicone.π b j ≫ Bicone.ι b j) ≫ (Bicone.toCone b).π.app { as := as✝ } =
    𝟙 b.pt ≫ (Bicone.toCone b).π.app { as := as✝ }
C : Type u
inst✝² : Category C
inst✝¹ : Preadditive C
J : Type
inst✝ : Fintype J
f : J → C
b : Bicone f
i : Bicone.IsBilimit b
j : Discrete J
⊢ (∑ j : J, Bicone.π b j ≫ Bicone.ι b j) ≫ (Bicone.toCone b).π.app j = 𝟙 b.pt ≫ (Bicone.toCone b).π.app j
cases j
no goals
case mk
C : Type u
inst✝² : Category C
inst✝¹ : Preadditive C
J : Type
inst✝ : Fintype J
f : J → C
b : Bicone f
i : Bicone.IsBilimit b
as✝ : J
⊢ (∑ j : J, Bicone.π b j ≫ Bicone.ι b j) ≫ (Bicone.toCone b).π.app { as := as✝ } =
    𝟙 b.pt ≫ (Bicone.toCone b).π.app { as := as✝ }
simp [sum_comp, b.ι_π, comp_dite]