C : Type u
inst✝ : Category C
I : MulticospanIndex C
K : Multifork I
b : I.R
⊢ K.π.app (WalkingMulticospan.left (MulticospanIndex.sndTo I b)) ≫
      (MulticospanIndex.multicospan I).map (WalkingMulticospan.Hom.snd b) =
    ι K (MulticospanIndex.sndTo I b) ≫ MulticospanIndex.snd I b
C : Type u
inst✝ : Category C
I : MulticospanIndex C
K : Multifork I
b : I.R
⊢ K.π.app (WalkingMulticospan.right b) = ι K (MulticospanIndex.sndTo I b) ≫ MulticospanIndex.snd I b
rw [← K.w (WalkingMulticospan.Hom.snd b)]
no goals
C : Type u
inst✝ : Category C
I : MulticospanIndex C
K : Multifork I
b : I.R
⊢ K.π.app (WalkingMulticospan.left (MulticospanIndex.sndTo I b)) ≫
      (MulticospanIndex.multicospan I).map (WalkingMulticospan.Hom.snd b) =
    ι K (MulticospanIndex.sndTo I b) ≫ MulticospanIndex.snd I b
rfl