J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : Bicone.IsBilimit b
j : J
j' : Discrete J
⊢ (ι f j ≫ (IsLimit.conePointUniqueUpToIso hb.isLimit (isLimit f)).inv) ≫ (Bicone.toCone b).π.app j' =
    (ι f j ≫ desc b.ι) ≫ (Bicone.toCone b).π.app j'
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : Bicone.IsBilimit b
⊢ (IsLimit.conePointUniqueUpToIso hb.isLimit (isLimit f)).inv = desc b.ι
refine' biproduct.hom_ext' _ _ fun j => hb.isLimit.hom_ext fun j' => _
no goals
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : Bicone.IsBilimit b
j : J
j' : Discrete J
⊢ (ι f j ≫ (IsLimit.conePointUniqueUpToIso hb.isLimit (isLimit f)).inv) ≫ (Bicone.toCone b).π.app j' =
    (ι f j ≫ desc b.ι) ≫ (Bicone.toCone b).π.app j'
rw [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp, Bicone.toCone_π_app,
  biproduct.bicone_π, biproduct.ι_desc, biproduct.ι_π, b.toCone_π_app, b.ι_π]