no goals
C : Type u
inst✝² : Category C
I : MulticospanIndex C
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
b : I.R
⊢ sndPiMap I ≫ Pi.π I.right b = Pi.π I.left (sndTo I b) ≫ snd I b
simp [sndPiMap]