case left
C : Type u
inst✝¹ : Category C
I : MulticospanIndex C
inst✝ : HasMultiequalizer I
W : C
i j : W ⟶ multiequalizer I
h : ∀ (a : I.L), i ≫ ι I a = j ≫ ι I a
a : I.L
⊢ i ≫ limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.left a) =
    j ≫ limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.left a)

case right
C : Type u
inst✝¹ : Category C
I : MulticospanIndex C
inst✝ : HasMultiequalizer I
W : C
i j : W ⟶ multiequalizer I
h : ∀ (a : I.L), i ≫ ι I a = j ≫ ι I a
b : I.R
⊢ i ≫ limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.right b) =
    j ≫ limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.right b)
C : Type u
inst✝¹ : Category C
I : MulticospanIndex C
inst✝ : HasMultiequalizer I
W : C
i j : W ⟶ multiequalizer I
h : ∀ (a : I.L), i ≫ ι I a = j ≫ ι I a
⊢ ∀ (j_1 : WalkingMulticospan I.fstTo I.sndTo),
    i ≫ limit.π (MulticospanIndex.multicospan I) j_1 = j ≫ limit.π (MulticospanIndex.multicospan I) j_1
rintro (a | b)
no goals
case right
C : Type u
inst✝¹ : Category C
I : MulticospanIndex C
inst✝ : HasMultiequalizer I
W : C
i j : W ⟶ multiequalizer I
h : ∀ (a : I.L), i ≫ ι I a = j ≫ ι I a
b : I.R
⊢ i ≫ limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.right b) =
    j ≫ limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.right b)
simp_rw [← limit.w I.multicospan (WalkingMulticospan.Hom.fst b), ← Category.assoc, h]
no goals
case left
C : Type u
inst✝¹ : Category C
I : MulticospanIndex C
inst✝ : HasMultiequalizer I
W : C
i j : W ⟶ multiequalizer I
h : ∀ (a : I.L), i ≫ ι I a = j ≫ ι I a
a : I.L
⊢ i ≫ limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.left a) =
    j ≫ limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.left a)
apply h