awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
inst_1 : HasMultiequalizer I
a : J.L
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) (multifork I).pt) (WalkingMulticospan.left a) ⟶
      I.multicospan.obj (WalkingMulticospan.left a))
    ((multifork I).π.app (WalkingMulticospan.left a)) (ι I a)

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
inst_1 : HasMultiequalizer I
b : J.R
⊢ Eq (α := multiequalizer I ⟶ I.right b) (ι I (J.fst b) ≫ I.fst b) (ι I (J.snd b) ≫ I.snd b)

Tactic:
Multifork.condition _ _

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.Multifork.condition, CategoryTheory.Limits.limit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
inst_1 : HasMultiequalizer I
W : C
k : (a : J.L) → W ⟶ I.left a
h : ∀ (b : J.R), k (J.fst b) ≫ I.fst b = k (J.snd b) ≫ I.snd b
a : J.L
⊢ CategoryStruct.comp (Y := multiequalizer I) (lift I W k h) (ι I a) = k a

Tactic:
limit.lift_π _ _

Premises used: CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
inst_1 : HasMultiequalizer I
W : C
i j : W ⟶ multiequalizer I
h : ∀ (a : J.L), i ≫ ι I a = j ≫ ι I a
⊢ i = j

Tactic:
Multifork.IsLimit.hom_ext (limit.isLimit _) h

Premises used: CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, CategoryTheory.Limits.Multifork.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
inst_1 : HasMultiequalizer I
inst_2 : HasProduct.{w, v, u} I.left
inst_3 : HasProduct.{w', v, u} I.right
⊢ HasEqualizer (X := piObj.{w, v, u} I.left) (Y := piObj.{w', v, u} I.right) I.fstPiMap I.sndPiMap

Tactic:
⟨⟨⟨_, IsLimit.ofPreservesConeTerminal I.multiforkEquivPiFork.functor (limit.isLimit _)⟩⟩⟩

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork, Nonempty.intro, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.IsLimit.ofPreservesConeTerminal, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
inst_1 : HasMultiequalizer I
inst_2 : HasProduct.{w, v, u} I.left
inst_3 : HasProduct.{w', v, u} I.right
a : J.L
rw :
  equalizer.ι I.fstPiMap I.sndPiMap ≫ Pi.π I.left a =
    CategoryStruct.comp (Y := multiequalizer I)
      (Iso.inv
        (limit.isoLimitCone
          {
            cone :=
              Functor.obj (Equivalence.inverse I.multiforkEquivPiFork)
                (limit.cone
                  (parallelPair (X := piObj.{w, v, u} I.left) (Y := piObj.{w', v, u} I.right) I.fstPiMap I.sndPiMap)),
            isLimit :=
              IsLimit.ofPreservesConeTerminal (Equivalence.inverse I.multiforkEquivPiFork)
                (limit.isLimit
                  (parallelPair (X := piObj.{w, v, u} I.left) (Y := piObj.{w', v, u} I.right) I.fstPiMap I.sndPiMap)) :
            LimitCone I.multicospan }))
      (ι I a)
⊢ Eq (α := multiequalizer I ⟶ I.left a) (CategoryStruct.comp (Y := piObj.{w, v, u} I.left) (ιPi I) (Pi.π I.left a))
    (ι I a)

Tactic:
rw [ιPi, Category.assoc, ← Iso.eq_inv_comp, isoEqualizer]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Multiequalizer.isoEqualizer, CategoryTheory.Limits.Multiequalizer.ιPi, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
inst_1 : HasMultiequalizer I
inst_2 : HasProduct.{w, v, u} I.left
inst_3 : HasProduct.{w', v, u} I.right
a : J.L
simp :
  equalizer.ι I.fstPiMap I.sndPiMap ≫ Pi.π I.left a =
    Fork.ι
        (limit.cone
          (parallelPair (X := piObj.{w, v, u} I.left) (Y := piObj.{w', v, u} I.right) I.fstPiMap I.sndPiMap)) ≫
      Fan.proj (limit.cone (Discrete.functor I.left)) a
⊢ equalizer.ι I.fstPiMap I.sndPiMap ≫ Pi.π I.left a =
    CategoryStruct.comp (Y := multiequalizer I)
      (Iso.inv
        (limit.isoLimitCone
          {
            cone :=
              Functor.obj (Equivalence.inverse I.multiforkEquivPiFork)
                (limit.cone
                  (parallelPair (X := piObj.{w, v, u} I.left) (Y := piObj.{w', v, u} I.right) I.fstPiMap I.sndPiMap)),
            isLimit :=
              IsLimit.ofPreservesConeTerminal (Equivalence.inverse I.multiforkEquivPiFork)
                (limit.isLimit
                  (parallelPair (X := piObj.{w, v, u} I.left) (Y := piObj.{w', v, u} I.right) I.fstPiMap I.sndPiMap)) :
            LimitCone I.multicospan }))
      (ι I a)

Tactic:
simp only [limit.isoLimitCone_inv_π, MulticospanIndex.multiforkEquivPiFork_inverse_obj_pt,
    limit.cone_x, MulticospanIndex.multiforkEquivPiFork_inverse_obj_π_app]

Premises used: CategoryTheory.Limits.limit.cone_x, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_π_app, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_pt, CategoryTheory.Limits.limit.isoLimitCone_inv_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
inst_1 : HasMultiequalizer I
inst_2 : HasProduct.{w, v, u} I.left
inst_3 : HasProduct.{w', v, u} I.right
a : J.L
⊢ equalizer.ι I.fstPiMap I.sndPiMap ≫ Pi.π I.left a =
    Fork.ι
        (limit.cone
          (parallelPair (X := piObj.{w, v, u} I.left) (Y := piObj.{w', v, u} I.right) I.fstPiMap I.sndPiMap)) ≫
      Fan.proj (limit.cone (Discrete.functor I.left)) a

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
inst_1 : HasMultiequalizer I
inst_2 : HasProduct.{w, v, u} I.left
inst_3 : HasProduct.{w', v, u} I.right
⊢ Mono (X := multiequalizer I) (Y := piObj.{w, v, u} I.left) (ιPi I)

Tactic:
mono_comp _ _

Premises used: CategoryTheory.Limits.Multiequalizer.ιPi, CategoryTheory.mono_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
inst_1 : HasMulticoequalizer I
b : J.R
⊢ (multicofork I).π b = π I b

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
inst_1 : HasMulticoequalizer I
b : J.R
⊢ Eq (α :=
    I.multispan.obj (WalkingMultispan.right b) ⟶
      Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) (multicofork I).pt) (WalkingMultispan.right b))
    ((multicofork I).ι.app (WalkingMultispan.right b)) (π I b)

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
inst_1 : HasMulticoequalizer I
b : J.R
⊢ Eq (α := I.multispan.obj (WalkingMultispan.right b) ⟶ colimit I.multispan)
    (colimit.ι I.multispan (WalkingMultispan.right b)) (π I b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
inst_1 : HasMulticoequalizer I
a : J.L
⊢ Eq (α := I.left a ⟶ multicoequalizer I) (I.fst a ≫ π I (J.fst a)) (I.snd a ≫ π I (J.snd a))

Tactic:
Multicofork.condition _ _

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.Limits.Multicofork.condition, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
inst_1 : HasMulticoequalizer I
W : C
k : (b : J.R) → I.right b ⟶ W
h : ∀ (a : J.L), I.fst a ≫ k (J.fst a) = I.snd a ≫ k (J.snd a)
b : J.R
⊢ CategoryStruct.comp (Y := multicoequalizer I) (π I b) (desc I W k h) = k b

Tactic:
colimit.ι_desc _ _

Premises used: CategoryTheory.Limits.colimit.ι_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
inst_1 : HasMulticoequalizer I
W : C
i j : multicoequalizer I ⟶ W
h : ∀ (b : J.R), π I b ≫ i = π I b ≫ j
a : J.L
left :
  (I.multispan.map (WalkingMultispan.Hom.fst a) ≫ colimit.ι I.multispan (WalkingMultispan.right (J.fst a))) ≫ i =
    (I.multispan.map (WalkingMultispan.Hom.fst a) ≫ colimit.ι I.multispan (WalkingMultispan.right (J.fst a))) ≫ j
left₁ :
  I.multispan.map (WalkingMultispan.Hom.fst a) ≫ colimit.ι I.multispan (WalkingMultispan.right (J.fst a)) ≫ i =
    I.multispan.map (WalkingMultispan.Hom.fst a) ≫ colimit.ι I.multispan (WalkingMultispan.right (J.fst a)) ≫ j
⊢ Eq (α := I.multispan.obj (WalkingMultispan.left a) ⟶ W) (colimit.ι I.multispan (WalkingMultispan.left a) ≫ i)
    (colimit.ι I.multispan (WalkingMultispan.left a) ≫ j)

Tactic:
simp_rw [← colimit.w I.multispan (WalkingMultispan.Hom.fst a), Category.assoc, h]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.WalkingMultispan.Hom.fst, CategoryTheory.Limits.MultispanIndex.multispan, CategoryTheory.Limits.colimit.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
inst_1 : HasMulticoequalizer I
W : C
i j : multicoequalizer I ⟶ W
h : ∀ (b : J.R), π I b ≫ i = π I b ≫ j
b : J.R
⊢ Eq (α := I.multispan.obj (WalkingMultispan.right b) ⟶ W) (colimit.ι I.multispan (WalkingMultispan.right b) ≫ i)
    (colimit.ι I.multispan (WalkingMultispan.right b) ≫ j)

Tactic:
apply h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
inst_1 : HasMulticoequalizer I
inst_2 : HasCoproduct.{w, v, u} I.left
inst_3 : HasCoproduct.{w', v, u} I.right
⊢ HasCoequalizer (X := sigmaObj.{w, v, u} I.left) (Y := sigmaObj.{w', v, u} I.right) I.fstSigmaMap I.sndSigmaMap

Tactic:
⟨⟨⟨_,
      IsColimit.ofPreservesCoconeInitial
        I.multicoforkEquivSigmaCofork.functor (colimit.isColimit _)⟩⟩⟩

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork, CategoryTheory.Equivalence.functor, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.IsColimit.ofPreservesCoconeInitial
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
inst_1 : HasMulticoequalizer I
inst_2 : HasCoproduct.{w, v, u} I.left
inst_3 : HasCoproduct.{w', v, u} I.right
b : J.R
rw :
  Sigma.ι I.right b ≫ coequalizer.π I.fstSigmaMap I.sndSigmaMap =
    CategoryStruct.comp (Y := multicoequalizer I) (π I b)
      (Iso.hom
        (colimit.isoColimitCocone
          {
            cocone :=
              Functor.obj (Equivalence.inverse I.multicoforkEquivSigmaCofork)
                (colimit.cocone
                  (parallelPair (X := sigmaObj.{w, v, u} I.left) (Y := sigmaObj.{w', v, u} I.right) I.fstSigmaMap
                    I.sndSigmaMap)),
            isColimit :=
              IsColimit.ofPreservesCoconeInitial (Equivalence.inverse I.multicoforkEquivSigmaCofork)
                (colimit.isColimit
                  (parallelPair (X := sigmaObj.{w, v, u} I.left) (Y := sigmaObj.{w', v, u} I.right) I.fstSigmaMap
                    I.sndSigmaMap)) :
            ColimitCocone I.multispan }))
⊢ Eq (α := I.right b ⟶ multicoequalizer I)
    (CategoryStruct.comp (Y := sigmaObj.{w', v, u} I.right) (Sigma.ι I.right b) (sigmaπ I)) (π I b)

Tactic:
rw [sigmaπ, ← Category.assoc, Iso.comp_inv_eq, isoCoequalizer]

Premises used: CategoryTheory.Limits.Multicoequalizer.isoCoequalizer, CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Limits.Multicoequalizer.sigmaπ
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
inst_1 : HasMulticoequalizer I
inst_2 : HasCoproduct.{w, v, u} I.left
inst_3 : HasCoproduct.{w', v, u} I.right
b : J.R
simp :
  Sigma.ι I.right b ≫ coequalizer.π I.fstSigmaMap I.sndSigmaMap =
    Cofan.inj (colimit.cocone (Discrete.functor I.right)) b ≫
      Cofork.π
        (colimit.cocone
          (parallelPair (X := sigmaObj.{w, v, u} I.left) (Y := sigmaObj.{w', v, u} I.right) I.fstSigmaMap
            I.sndSigmaMap))
⊢ Sigma.ι I.right b ≫ coequalizer.π I.fstSigmaMap I.sndSigmaMap =
    CategoryStruct.comp (Y := multicoequalizer I) (π I b)
      (Iso.hom
        (colimit.isoColimitCocone
          {
            cocone :=
              Functor.obj (Equivalence.inverse I.multicoforkEquivSigmaCofork)
                (colimit.cocone
                  (parallelPair (X := sigmaObj.{w, v, u} I.left) (Y := sigmaObj.{w', v, u} I.right) I.fstSigmaMap
                    I.sndSigmaMap)),
            isColimit :=
              IsColimit.ofPreservesCoconeInitial (Equivalence.inverse I.multicoforkEquivSigmaCofork)
                (colimit.isColimit
                  (parallelPair (X := sigmaObj.{w, v, u} I.left) (Y := sigmaObj.{w', v, u} I.right) I.fstSigmaMap
                    I.sndSigmaMap)) :
            ColimitCocone I.multispan }))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
inst_1 : HasMulticoequalizer I
inst_2 : HasCoproduct.{w, v, u} I.left
inst_3 : HasCoproduct.{w', v, u} I.right
b : J.R
⊢ Sigma.ι I.right b ≫ coequalizer.π I.fstSigmaMap I.sndSigmaMap =
    Cofan.inj (colimit.cocone (Discrete.functor I.right)) b ≫
      Cofork.π
        (colimit.cocone
          (parallelPair (X := sigmaObj.{w, v, u} I.left) (Y := sigmaObj.{w', v, u} I.right) I.fstSigmaMap
            I.sndSigmaMap))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
inst_1 : HasMulticoequalizer I
inst_2 : HasCoproduct.{w, v, u} I.left
inst_3 : HasCoproduct.{w', v, u} I.right
⊢ Epi (X := sigmaObj.{w', v, u} I.right) (Y := multicoequalizer I) (sigmaπ I)

Tactic:
epi_comp _ _

Premises used: CategoryTheory.Limits.Multicoequalizer.sigmaπ, CategoryTheory.epi_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
inst_1 : LinearOrder ι
I : MultispanIndex.{w, w, v, u} (MultispanShape.prod ι) C
c : Multicofork (J := MultispanShape.ofLinearOrder ι) I.toLinearOrder
h : I.SymmStruct
x y : ι
inl :
  ∀ (hxy : x < y),
    Eq (α := I.left (x, y) ⟶ c.pt) (I.fst (x, y) ≫ c.π ((MultispanShape.prod ι).fst (x, y)))
      (I.snd (x, y) ≫ c.π ((MultispanShape.prod ι).snd (x, y)))
inr :
  Eq (α := I.left (x, x) ⟶ c.pt) (I.fst (x, x) ≫ c.π ((MultispanShape.prod ι).fst (x, x)))
    (I.snd (x, x) ≫ c.π ((MultispanShape.prod ι).snd (x, x)))
inr₁ :
  ∀ (hxy : y < x),
    Eq (α := I.left (x, y) ⟶ c.pt) (I.fst (x, y) ≫ c.π ((MultispanShape.prod ι).fst (x, y)))
      (I.snd (x, y) ≫ c.π ((MultispanShape.prod ι).snd (x, y)))
⊢ Eq (α := I.left (x, y) ⟶ c.pt) (I.fst (x, y) ≫ c.π ((MultispanShape.prod ι).fst (x, y)))
    (I.snd (x, y) ≫ c.π ((MultispanShape.prod ι).snd (x, y)))

Tactic:
obtain hxy | rfl | hxy := lt_trichotomy x y

Premises used: rfl, lt_trichotomy
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
inst_1 : LinearOrder ι
I : MultispanIndex.{w, w, v, u} (MultispanShape.prod ι) C
c : Multicofork (J := MultispanShape.ofLinearOrder ι) I.toLinearOrder
h : I.SymmStruct
x y : ι
hxy : x < y
⊢ Eq (α := I.left (x, y) ⟶ c.pt) (I.fst (x, y) ≫ c.π ((MultispanShape.prod ι).fst (x, y)))
    (I.snd (x, y) ≫ c.π ((MultispanShape.prod ι).snd (x, y)))

Tactic:
c.condition ⟨⟨x, y⟩, hxy⟩

Premises used: Prod.mk, Subtype.mk, CategoryTheory.Limits.Multicofork.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
inst_1 : LinearOrder ι
I : MultispanIndex.{w, w, v, u} (MultispanShape.prod ι) C
c : Multicofork (J := MultispanShape.ofLinearOrder ι) I.toLinearOrder
h : I.SymmStruct
x y : ι
hxy : x < y
⊢ Eq (α := I.left (x, y) ⟶ c.pt) (I.fst (x, y) ≫ c.π ((MultispanShape.prod ι).fst (x, y)))
    (I.snd (x, y) ≫ c.π ((MultispanShape.prod ι).snd (x, y)))

Tactic:
exact c.condition ⟨⟨x, y⟩, hxy⟩

Premises used: Prod.mk, Subtype.mk, CategoryTheory.Limits.Multicofork.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
inst_1 : LinearOrder ι
I : MultispanIndex.{w, w, v, u} (MultispanShape.prod ι) C
c : Multicofork (J := MultispanShape.ofLinearOrder ι) I.toLinearOrder
h : I.SymmStruct
x : ι
⊢ Eq (α := I.left (x, x) ⟶ c.pt) (I.fst (x, x) ≫ c.π ((MultispanShape.prod ι).fst (x, x)))
    (I.snd (x, x) ≫ c.π ((MultispanShape.prod ι).snd (x, x)))

Tactic:
simp [h.fst_eq_snd]

Premises used: CategoryTheory.Limits.MultispanIndex.SymmStruct.fst_eq_snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
inst_1 : LinearOrder ι
I : MultispanIndex.{w, w, v, u} (MultispanShape.prod ι) C
c : Multicofork (J := MultispanShape.ofLinearOrder ι) I.toLinearOrder
h : I.SymmStruct
x y : ι
hxy : y < x
⊢ Eq (α :=
    MultispanIndex.left (J := MultispanShape.ofLinearOrder ι) I.toLinearOrder
        (Subtype.mk (p := fun (x : ι × ι) ↦ Membership.mem (γ := Set (ι × ι)) {x : ι × ι | x.1 < x.2} x) (y, x) hxy) ⟶
      c.pt)
    (MultispanIndex.fst I.toLinearOrder
        (Subtype.mk (p := fun (x : ι × ι) ↦ Membership.mem (γ := Set (ι × ι)) {x : ι × ι | x.1 < x.2} x) (y, x) hxy) ≫
      c.π
        ((MultispanShape.ofLinearOrder ι).fst
          (Subtype.mk (p := fun (x : ι × ι) ↦ Membership.mem (γ := Set (ι × ι)) {x : ι × ι | x.1 < x.2} x) (y, x) hxy)))
    (MultispanIndex.snd I.toLinearOrder
        (Subtype.mk (p := fun (x : ι × ι) ↦ Membership.mem (γ := Set (ι × ι)) {x : ι × ι | x.1 < x.2} x) (y, x) hxy) ≫
      c.π
        ((MultispanShape.ofLinearOrder ι).snd
          (Subtype.mk (p := fun (x : ι × ι) ↦ Membership.mem (γ := Set (ι × ι)) {x : ι × ι | x.1 < x.2} x) (y, x) hxy)))

Tactic:
have := c.condition ⟨⟨y, x⟩, hxy⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
inst_1 : LinearOrder ι
I : MultispanIndex.{w, w, v, u} (MultispanShape.prod ι) C
c : Multicofork (J := MultispanShape.ofLinearOrder ι) I.toLinearOrder
h : I.SymmStruct
x y : ι
hxy : y < x
this :
  Eq (α :=
    MultispanIndex.left (J := MultispanShape.ofLinearOrder ι) I.toLinearOrder
        (Subtype.mk (p := fun (x : ι × ι) ↦ Membership.mem (γ := Set (ι × ι)) {x : ι × ι | x.1 < x.2} x) (y, x) hxy) ⟶
      c.pt)
    (MultispanIndex.fst I.toLinearOrder
        (Subtype.mk (p := fun (x : ι × ι) ↦ Membership.mem (γ := Set (ι × ι)) {x : ι × ι | x.1 < x.2} x) (y, x) hxy) ≫
      c.π
        ((MultispanShape.ofLinearOrder ι).fst
          (Subtype.mk (p := fun (x : ι × ι) ↦ Membership.mem (γ := Set (ι × ι)) {x : ι × ι | x.1 < x.2} x) (y, x) hxy)))
    (MultispanIndex.snd I.toLinearOrder
        (Subtype.mk (p := fun (x : ι × ι) ↦ Membership.mem (γ := Set (ι × ι)) {x : ι × ι | x.1 < x.2} x) (y, x) hxy) ≫
      c.π
        ((MultispanShape.ofLinearOrder ι).snd
          (Subtype.mk (p := fun (x : ι × ι) ↦ Membership.mem (γ := Set (ι × ι)) {x : ι × ι | x.1 < x.2} x) (y, x) hxy)))
inr : Eq (α := I.left (x, y) ⟶ c.pt) (I.fst (x, y) ≫ c.π x) (I.snd (x, y) ≫ c.π y)
⊢ Eq (α := I.left (x, y) ⟶ c.pt) (I.fst (x, y) ≫ c.π ((MultispanShape.prod ι).fst (x, y)))
    (I.snd (x, y) ≫ c.π ((MultispanShape.prod ι).snd (x, y)))

Tactic:
dsimp at this ⊢
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
inst_1 : LinearOrder ι
I : MultispanIndex.{w, w, v, u} (MultispanShape.prod ι) C
c : Multicofork (J := MultispanShape.ofLinearOrder ι) I.toLinearOrder
h : I.SymmStruct
x y : ι
hxy : y < x
this : Eq (α := I.left (y, x) ⟶ c.pt) (I.fst (y, x) ≫ c.π y) (I.snd (y, x) ≫ c.π x)
inr : Eq (α := I.left (x, y) ⟶ c.pt) (I.fst (x, y) ≫ c.π x) ((h.iso x y).hom ≫ I.fst (y, x) ≫ c.π y)
inr₁ : Eq (α := I.left (x, y) ⟶ c.pt) ((h.iso x y).hom ≫ I.snd (y, x) ≫ c.π x) ((h.iso x y).hom ≫ I.fst (y, x) ≫ c.π y)
inr₂ inr₃ :
  Eq (α := I.left (x, y) ⟶ c.pt) ((h.iso x y).hom ≫ I.snd (y, x) ≫ c.π x) ((h.iso x y).hom ≫ I.snd (y, x) ≫ c.π x)
⊢ Eq (α := I.left (x, y) ⟶ c.pt) (I.fst (x, y) ≫ c.π x) (I.snd (x, y) ≫ c.π y)

Tactic:
rw [← h.iso_hom_fst_assoc, ← h.iso_hom_snd_assoc, this]

Premises used: CategoryTheory.Limits.MultispanIndex.SymmStruct.iso_hom_snd_assoc, CategoryTheory.Limits.MultispanIndex.SymmStruct.iso_hom_fst_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
inst_1 : LinearOrder ι
I : MultispanIndex.{w, w, v, u} (MultispanShape.prod ι) C
c : Multicofork I
hc : IsColimit c
h : I.SymmStruct
s : Multicofork (J := MultispanShape.ofLinearOrder ι) I.toLinearOrder
m : Cocone.pt (J := WalkingMultispan (MultispanShape.ofLinearOrder ι)) c.toLinearOrder ⟶ s.pt
hm : ∀ (i : (MultispanShape.ofLinearOrder ι).R), π c.toLinearOrder i ≫ m = s.π i
i : (MultispanShape.prod ι).R
⊢ Eq (α := I.multispan.obj (WalkingMultispan.right i) ⟶ (s.ofLinearOrder h).pt)
    (c.ι.app (WalkingMultispan.right i) ≫ hc.desc (s.ofLinearOrder h))
    ((s.ofLinearOrder h).ι.app (WalkingMultispan.right i))

Tactic:
have := hc.fac (ofLinearOrder s h) (.right i)
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
inst_1 : LinearOrder ι
I : MultispanIndex.{w, w, v, u} (MultispanShape.prod ι) C
c : Multicofork I
hc : IsColimit c
h : I.SymmStruct
s : Multicofork (J := MultispanShape.ofLinearOrder ι) I.toLinearOrder
m : Cocone.pt (J := WalkingMultispan (MultispanShape.ofLinearOrder ι)) c.toLinearOrder ⟶ s.pt
hm : ∀ (i : (MultispanShape.ofLinearOrder ι).R), π c.toLinearOrder i ≫ m = s.π i
i : (MultispanShape.prod ι).R
this : c.π i ≫ hc.desc (s.ofLinearOrder h) = (s.ofLinearOrder h).π i
rw : c.π i ≫ m = (s.ofLinearOrder h).π i
⊢ c.π i ≫ m =
    c.π i ≫
      (fun (s : Multicofork (J := MultispanShape.ofLinearOrder ι) I.toLinearOrder) ↦
          (hc.desc (s.ofLinearOrder h) : c.pt ⟶ (s.ofLinearOrder h).pt))
        s

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
inst_1 : LinearOrder ι
I : MultispanIndex.{w, w, v, u} (MultispanShape.prod ι) C
c : Multicofork I
hc : IsColimit c
h : I.SymmStruct
s : Multicofork (J := MultispanShape.ofLinearOrder ι) I.toLinearOrder
m : Cocone.pt (J := WalkingMultispan (MultispanShape.ofLinearOrder ι)) c.toLinearOrder ⟶ s.pt
hm : ∀ (i : (MultispanShape.ofLinearOrder ι).R), π c.toLinearOrder i ≫ m = s.π i
i : (MultispanShape.prod ι).R
this : c.π i ≫ hc.desc (s.ofLinearOrder h) = (s.ofLinearOrder h).π i
⊢ c.π i ≫ m = (s.ofLinearOrder h).π i

Tactic:
apply hm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ c.π.app WalkingCospan.left = c.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ c.π.app WalkingCospan.right = c.snd

Tactic:
rfl

Premises used: rfl