no goals
C : Type u
inst✝² : Category C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : I.L
⊢ Sigma.ι I.left b ≫ fstSigmaMap I = fst I b ≫ Sigma.ι I.right (fstFrom I b)
simp [fstSigmaMap]