C : Type u
inst✝ : Category C
I : MultispanIndex C
K : Multicofork I
a : I.L
⊢ (MultispanIndex.multispan I).map (WalkingMultispan.Hom.snd a) ≫
      K.ι.app (WalkingMultispan.right (MultispanIndex.sndFrom I a)) =
    MultispanIndex.snd I a ≫ π K (MultispanIndex.sndFrom I a)
C : Type u
inst✝ : Category C
I : MultispanIndex C
K : Multicofork I
a : I.L
⊢ K.ι.app (WalkingMultispan.left a) = MultispanIndex.snd I a ≫ π K (MultispanIndex.sndFrom I a)
rw [← K.w (WalkingMultispan.Hom.snd a)]
no goals
C : Type u
inst✝ : Category C
I : MultispanIndex C
K : Multicofork I
a : I.L
⊢ (MultispanIndex.multispan I).map (WalkingMultispan.Hom.snd a) ≫
      K.ι.app (WalkingMultispan.right (MultispanIndex.sndFrom I a)) =
    MultispanIndex.snd I a ≫ π K (MultispanIndex.sndFrom I a)
rfl