C : Type u
inst✝³ : Category C
I : MulticospanIndex C
inst✝² : HasMultiequalizer I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
a : I.L
⊢ equalizer.ι (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I) ≫ Pi.π I.left a =
    (limit.isoLimitCone
          {
            cone :=
              (MulticospanIndex.multiforkEquivPiFork I).inverse.obj
                (limit.cone (parallelPair (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I))),
            isLimit :=
              IsLimit.ofPreservesConeTerminal (MulticospanIndex.multiforkEquivPiFork I).inverse
                (limit.isLimit (parallelPair (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I))) }).inv ≫
      ι I a
C : Type u
inst✝³ : Category C
I : MulticospanIndex C
inst✝² : HasMultiequalizer I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
a : I.L
⊢ ιPi I ≫ Pi.π I.left a = ι I a
rw [ιPi, Category.assoc, ← Iso.eq_inv_comp, isoEqualizer]
no goals
C : Type u
inst✝³ : Category C
I : MulticospanIndex C
inst✝² : HasMultiequalizer I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
a : I.L
⊢ equalizer.ι (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I) ≫ Pi.π I.left a =
    (limit.isoLimitCone
          {
            cone :=
              (MulticospanIndex.multiforkEquivPiFork I).inverse.obj
                (limit.cone (parallelPair (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I))),
            isLimit :=
              IsLimit.ofPreservesConeTerminal (MulticospanIndex.multiforkEquivPiFork I).inverse
                (limit.isLimit (parallelPair (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I))) }).inv ≫
      ι I a
simp