case h
C : Type u
inst✝² : Category C
I : MultispanIndex C
K : Multicofork I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b✝ : I.L
⊢ Sigma.ι I.left b✝ ≫ MultispanIndex.fstSigmaMap I ≫ Sigma.desc (π K) =
    Sigma.ι I.left b✝ ≫ MultispanIndex.sndSigmaMap I ≫ Sigma.desc (π K)
C : Type u
inst✝² : Category C
I : MultispanIndex C
K : Multicofork I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
⊢ MultispanIndex.fstSigmaMap I ≫ Sigma.desc (π K) = MultispanIndex.sndSigmaMap I ≫ Sigma.desc (π K)
ext
no goals
case h
C : Type u
inst✝² : Category C
I : MultispanIndex C
K : Multicofork I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b✝ : I.L
⊢ Sigma.ι I.left b✝ ≫ MultispanIndex.fstSigmaMap I ≫ Sigma.desc (π K) =
    Sigma.ι I.left b✝ ≫ MultispanIndex.sndSigmaMap I ≫ Sigma.desc (π K)
simp