awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MultispanShape
I_1 : MultispanIndex.{w, w', v, u} J_1 C
K : Multicofork I_1
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a : J.L
⊢ Eq (α :=
    I.multispan.obj (WalkingMultispan.left a) ⟶
      Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) P) (WalkingMultispan.right (J.snd a)))
    (I.multispan.map (WalkingMultispan.Hom.snd a) ≫
      match (motive :=
        (x : WalkingMultispan J) →
          I.multispan.obj x ⟶ Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) P) x)
        WalkingMultispan.right (J.snd a) with
      | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
      | WalkingMultispan.right a => π a)
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) P) (WalkingMultispan.left a))
      (match (motive :=
        (x : WalkingMultispan J) →
          I.multispan.obj x ⟶ Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) P) x)
        WalkingMultispan.left a with
      | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
      | WalkingMultispan.right a => π a)
      (Functor.map (Functor.obj (Functor.const (WalkingMultispan J)) P) (WalkingMultispan.Hom.snd a)))
have left : I.snd a ≫ π (J.snd a) = (I.fst a ≫ π (J.fst a)) ≫ 𝟙 P
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MultispanShape
I_1 : MultispanIndex.{w, w', v, u} J_1 C
K : Multicofork I_1
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a : J.R
⊢ Eq (α :=
    I.multispan.obj (WalkingMultispan.right a) ⟶
      Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) P) (WalkingMultispan.right a))
    (I.multispan.map (WalkingMultispan.Hom.id (WalkingMultispan.right a)) ≫
      match (motive :=
        (x : WalkingMultispan J) →
          I.multispan.obj x ⟶ Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) P) x)
        WalkingMultispan.right a with
      | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
      | WalkingMultispan.right a => π a)
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) P) (WalkingMultispan.right a))
      (match (motive :=
        (x : WalkingMultispan J) →
          I.multispan.obj x ⟶ Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) P) x)
        WalkingMultispan.right a with
      | WalkingMultispan.left a => I.fst a ≫ π (J.fst a)
      | WalkingMultispan.right a => π a)
      (Functor.map (Functor.obj (Functor.const (WalkingMultispan J)) P)
        (WalkingMultispan.Hom.id (WalkingMultispan.right a))))
have right : I.multispan.map (𝟙 (WalkingMultispan.right a)) ≫ π a = π a ≫ 𝟙 P
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MultispanShape
I_1 : MultispanIndex.{w, w', v, u} J_1 C
K : Multicofork I_1
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a : J.L
⊢ I.snd a ≫ π (J.snd a) = (I.fst a ≫ π (J.fst a)) ≫ 𝟙 P
have left : I.snd a ≫ π (J.snd a) = I.fst a ≫ π (J.fst a)
Tactic: simp only [Functor.map_id, MultispanIndex.multispan_obj_left,
            Category.id_comp, Category.comp_id, MultispanIndex.multispan_obj_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MultispanShape
I_1 : MultispanIndex.{w, w', v, u} J_1 C
K : Multicofork I_1
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
P : C
π : (b : J.R) → I.right b ⟶ P
w : ∀ (a : J.L), I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
a : J.L
⊢ I.snd a ≫ π (J.snd a) = I.fst a ≫ π (J.fst a)
have left : I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
K : Multicofork I
a : J.L
⊢ I.fst a ≫ K.π (J.fst a) = I.snd a ≫ K.π (J.snd a)
have rw : I.fst a ≫ K.π (J.fst a) = K.ι.app (WalkingMultispan.left a)
Tactic: rw [← K.snd_app_right, ← K.fst_app_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
K : Multicofork I
a : J.L
rw : I.fst a ≫ K.π (J.fst a) = K.ι.app (WalkingMultispan.left a)
⊢ I.fst a ≫ K.π (J.fst a) = I.snd a ≫ K.π (J.snd a)
have rw₁ : Eq (α := I.left a ⟶ K.pt)
  (K.ι.app (WalkingMultispan.left a) :
    I.multispan.obj (WalkingMultispan.left a) ⟶
      Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) K.pt) (WalkingMultispan.left a))
  (K.ι.app (WalkingMultispan.left a))
Tactic: rw [← K.snd_app_right, ← K.fst_app_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : J.R), K.π i ≫ desc E = E.π i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), K.π i ≫ m = E.π i) → m = desc E
S : Cocone I.multispan
a : J.L
⊢ Eq (α := I.multispan.obj (WalkingMultispan.left a) ⟶ S.pt) (K.ι.app (WalkingMultispan.left a) ≫ desc S)
    (S.ι.app (WalkingMultispan.left a))
have left : I.multispan.map (WalkingMultispan.Hom.fst a) ≫ K.ι.app (WalkingMultispan.right (J.fst a)) ≫ desc S =
  I.multispan.map (WalkingMultispan.Hom.fst a) ≫ S.ι.app (WalkingMultispan.right (J.fst a))
Tactic: rw [← K.w (WalkingMultispan.Hom.fst a), ← S.w (WalkingMultispan.Hom.fst a),
          Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : J.R), K.π i ≫ desc E = E.π i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), K.π i ≫ m = E.π i) → m = desc E
S : Cocone I.multispan
a : J.L
⊢ I.multispan.map (WalkingMultispan.Hom.fst a) ≫ K.ι.app (WalkingMultispan.right (J.fst a)) ≫ desc S =
    I.multispan.map (WalkingMultispan.Hom.fst a) ≫ S.ι.app (WalkingMultispan.right (J.fst a))
have left : Eq (α := I.multispan.obj (WalkingMultispan.right (J.fst a)) ⟶ S.pt)
  (K.ι.app (WalkingMultispan.right (J.fst a)) ≫ desc S) (S.ι.app (WalkingMultispan.right (J.fst a)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : J.R), K.π i ≫ desc E = E.π i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), K.π i ≫ m = E.π i) → m = desc E
S : Cocone I.multispan
m : K.pt ⟶ S.pt
hm : ∀ (j : WalkingMultispan J), K.ι.app j ≫ m = S.ι.app j
⊢ m = desc S
have a : ∀ (i : J.R), K.π i ≫ m = π S i
Tactic: apply uniq
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
K : Multicofork I
hK : IsColimit K
T : C
f g : K.pt ⟶ T
h : ∀ (a : J.R), K.π a ≫ f = K.π a ≫ g
⊢ f = g
have apply : ∀ (j : WalkingMultispan J), K.ι.app j ≫ f = K.ι.app j ≫ g
Tactic: apply hK.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
K : Multicofork I
c : Cofan.{w, v, u} I.left
hc : IsColimit c
d : Cofan.{w', v, u} I.right
hd : IsColimit d
⊢ I.fstSigmaMapOfIsColimit d hc ≫ Cofan.IsColimit.desc hd K.π =
    I.sndSigmaMapOfIsColimit d hc ≫ Cofan.IsColimit.desc hd K.π
have h : ∀ (i : J.L),
  c.inj i ≫ I.fstSigmaMapOfIsColimit d hc ≫ Cofan.IsColimit.desc hd K.π =
    c.inj i ≫ I.sndSigmaMapOfIsColimit d hc ≫ Cofan.IsColimit.desc hd K.π
Tactic: apply Cofan.IsColimit.hom_ext hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
c : Cofan.{w, v, u} I.left
hc : IsColimit c
d : Cofan.{w', v, u} I.right
hd : IsColimit d
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
⊢ (Multicofork.toSigmaCofork hc hd K₁).ι.app WalkingParallelPair.zero ≫ f.hom =
    (Multicofork.toSigmaCofork hc hd K₂).ι.app WalkingParallelPair.zero
have zero : ∀ (i : J.L),
  c.inj i ≫ (Multicofork.toSigmaCofork hc hd K₁).ι.app WalkingParallelPair.zero ≫ f.hom =
    c.inj i ≫ (Multicofork.toSigmaCofork hc hd K₂).ι.app WalkingParallelPair.zero
Tactic: apply Cofan.IsColimit.hom_ext hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
c : Cofan.{w, v, u} I.left
hc : IsColimit c
d : Cofan.{w', v, u} I.right
hd : IsColimit d
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
⊢ (Multicofork.toSigmaCofork hc hd K₁).ι.app WalkingParallelPair.one ≫ f.hom =
    (Multicofork.toSigmaCofork hc hd K₂).ι.app WalkingParallelPair.one
have one : ∀ (i : J.R),
  d.inj i ≫ (Multicofork.toSigmaCofork hc hd K₁).ι.app WalkingParallelPair.one ≫ f.hom =
    d.inj i ≫ (Multicofork.toSigmaCofork hc hd K₂).ι.app WalkingParallelPair.one
Tactic: apply Cofan.IsColimit.hom_ext hd
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : MultispanShape
I : MultispanIndex.{w, w', v, u} J C
c : Cofan.{w, v, u} I.left
hc : IsColimit c
d : Cofan.{w', v, u} I.right
hd : IsColimit d
K : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
⊢ (Functor.obj (I.ofSigmaCoforkFunctor hc ⋙ I.toSigmaCoforkFunctor hc hd) K).π ≫
      Iso.hom (Iso.refl (Functor.obj (I.ofSigmaCoforkFunctor hc ⋙ I.toSigmaCoforkFunctor hc hd) K).pt) =
    (Functor.obj (𝟭 (Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc))) K).π
have h : ∀ (i : J.R),
  d.inj i ≫
      (Functor.obj (I.ofSigmaCoforkFunctor hc ⋙ I.toSigmaCoforkFunctor hc hd) K).π ≫
        Iso.hom (Iso.refl (Functor.obj (I.ofSigmaCoforkFunctor hc ⋙ I.toSigmaCoforkFunctor hc hd) K).pt) =
    d.inj i ≫ (Functor.obj (𝟭 (Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc))) K).π
Tactic: apply Cofan.IsColimit.hom_ext hd
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
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
⊢ Eq (α := multiequalizer I ⟶ I.left a) (CategoryStruct.comp (Y := piObj.{w, v, u} I.left) (ιPi I) (Pi.π I.left a))
    (ι I a)
have 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)
Tactic: rw [ιPi, Category.assoc, ← Iso.eq_inv_comp, isoEqualizer]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
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 =
    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)
have 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
Tactic: simp only [limit.isoLimitCone_inv_π, MulticospanIndex.multiforkEquivPiFork_inverse_obj_pt,
    limit.cone_x, MulticospanIndex.multiforkEquivPiFork_inverse_obj_π_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
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
⊢ Eq (α := I.multispan.obj (WalkingMultispan.left a) ⟶ W) (colimit.ι I.multispan (WalkingMultispan.left a) ≫ i)
    (colimit.ι I.multispan (WalkingMultispan.left a) ≫ j)
have 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
Tactic: simp_rw [← colimit.w I.multispan (WalkingMultispan.Hom.fst a), Category.assoc, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
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
⊢ Eq (α := I.multispan.obj (WalkingMultispan.left a) ⟶ W) (colimit.ι I.multispan (WalkingMultispan.left a) ≫ i)
    (colimit.ι I.multispan (WalkingMultispan.left a) ≫ j)
have 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
Tactic: simp_rw [← colimit.w I.multispan (WalkingMultispan.Hom.fst a), Category.assoc, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
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
⊢ Eq (α := I.right b ⟶ multicoequalizer I)
    (CategoryStruct.comp (Y := sigmaObj.{w', v, u} I.right) (Sigma.ι I.right b) (sigmaπ I)) (π I b)
have 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 }))
Tactic: rw [sigmaπ, ← Category.assoc, Iso.comp_inv_eq, isoCoequalizer]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
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 =
    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 }))
have 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))
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
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 : ι
⊢ 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)))
have 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)))
Tactic: obtain hxy | rfl | hxy := lt_trichotomy x y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
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)))
⊢ 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)))
have 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)))
Tactic: obtain hxy | rfl | hxy := lt_trichotomy x y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
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)))
⊢ 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)))
have 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)))
Tactic: obtain hxy | rfl | hxy := lt_trichotomy x y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (hypothesis)
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 (α := 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)))
have 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)))
Tactic: have := c.condition ⟨⟨y, x⟩, hxy⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
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)))
⊢ 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)))
have inr : Eq (α := I.left (x, y) ⟶ c.pt) (I.fst (x, y) ≫ c.π x) (I.snd (x, y) ≫ c.π y)
Tactic: dsimp at this ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
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)
⊢ Eq (α := I.left (x, y) ⟶ c.pt) (I.fst (x, y) ≫ c.π x) (I.snd (x, y) ≫ c.π y)
have 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)
Tactic: rw [← h.iso_hom_fst_assoc, ← h.iso_hom_snd_assoc, this]