C : Type u
inst✝³ : Category C
I : MultispanIndex C
inst✝² : HasMulticoequalizer I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : I.R
⊢ Sigma.ι I.right b ≫ coequalizer.π (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I) =
    π I b ≫
      (colimit.isoColimitCocone
          {
            cocone :=
              (MultispanIndex.multicoforkEquivSigmaCofork I).inverse.obj
                (colimit.cocone (parallelPair (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I))),
            isColimit :=
              IsColimit.ofPreservesCoconeInitial (MultispanIndex.multicoforkEquivSigmaCofork I).inverse
                (colimit.isColimit (parallelPair (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I))) }).hom
C : Type u
inst✝³ : Category C
I : MultispanIndex C
inst✝² : HasMulticoequalizer I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : I.R
⊢ Sigma.ι I.right b ≫ sigmaπ I = π I b
rw [sigmaπ, ← Category.assoc, Iso.comp_inv_eq, isoCoequalizer]
C : Type u
inst✝³ : Category C
I : MultispanIndex C
inst✝² : HasMulticoequalizer I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : I.R
⊢ Sigma.ι I.right b ≫ coequalizer.π (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I) =
    Multicofork.π
      (Multicofork.ofSigmaCofork I
        (colimit.cocone (parallelPair (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I))))
      b
C : Type u
inst✝³ : Category C
I : MultispanIndex C
inst✝² : HasMulticoequalizer I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : I.R
⊢ Sigma.ι I.right b ≫ coequalizer.π (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I) =
    π I b ≫
      (colimit.isoColimitCocone
          {
            cocone :=
              (MultispanIndex.multicoforkEquivSigmaCofork I).inverse.obj
                (colimit.cocone (parallelPair (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I))),
            isColimit :=
              IsColimit.ofPreservesCoconeInitial (MultispanIndex.multicoforkEquivSigmaCofork I).inverse
                (colimit.isColimit (parallelPair (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I))) }).hom
simp only [MultispanIndex.multicoforkEquivSigmaCofork_inverse,
  MultispanIndex.ofSigmaCoforkFunctor_obj, colimit.isoColimitCocone_ι_hom,
  Multicofork.ofSigmaCofork_pt, colimit.cocone_x, Multicofork.π_eq_app_right]
no goals
C : Type u
inst✝³ : Category C
I : MultispanIndex C
inst✝² : HasMulticoequalizer I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : I.R
⊢ Sigma.ι I.right b ≫ coequalizer.π (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I) =
    Multicofork.π
      (Multicofork.ofSigmaCofork I
        (colimit.cocone (parallelPair (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I))))
      b
rfl