awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J_1 C
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
inst_1 : HasProduct.{w, v, u} I.left
inst_2 : HasProduct.{w', v, u} I.right
J : MulticospanShape
inst_3 : Unique J.L
inst_4 : Unique J.R
X Y : C
f g : X ⟶ Y
refine_1 :
  ∀ (x : J.R),
    (Iso.hom
            (Iso.refl
              (Cone.pt.{u_1, v, u_1, u} (J := Discrete J.L) (F := Discrete.functor (ofParallelHoms J f g).left)
                (Fan.mk X fun (x : J.L) ↦ Iso.hom (Iso.refl X)))) ≫
          f) ≫
        Fan.proj (Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y)) x =
      ((ofParallelHoms J f g).fstPiMapOfIsLimit (Fan.mk X fun (x : J.L) ↦ Iso.hom (Iso.refl X)) (d :=
            Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y)) (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
          Iso.hom
            (Iso.refl
              (Cone.pt.{u_2, v, u_2, u} (J := Discrete J.R) (F := Discrete.functor (ofParallelHoms J f g).right)
                (Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y))))) ≫
        Fan.proj (Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y)) x
⊢ Iso.hom
        (Iso.refl
          (Cone.pt.{u_1, v, u_1, u} (J := Discrete J.L) (F := Discrete.functor (ofParallelHoms J f g).left)
            (Fan.mk X fun (x : J.L) ↦ Iso.hom (Iso.refl X)))) ≫
      f =
    (ofParallelHoms J f g).fstPiMapOfIsLimit (Fan.mk X fun (x : J.L) ↦ Iso.hom (Iso.refl X)) (d :=
        Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y)) (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
      Iso.hom
        (Iso.refl
          (Cone.pt.{u_2, v, u_2, u} (J := Discrete J.R) (F := Discrete.functor (ofParallelHoms J f g).right)
            (Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y))))

Tactic:
refine Fan.IsLimit.hom_ext (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) _ _ fun _ ↦ ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Fan.isLimitMkOfUnique, CategoryTheory.Limits.MulticospanShape.R, CategoryTheory.Limits.Fan.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J_1 C
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
inst_1 : HasProduct.{w, v, u} I.left
inst_2 : HasProduct.{w', v, u} I.right
J : MulticospanShape
inst_3 : Unique J.L
inst_4 : Unique J.R
X Y : C
f g : X ⟶ Y
x : J.R
refine_1 :
  Iso.hom
        (Iso.refl
          (Cone.pt.{u_1, v, u_1, u} (J := Discrete J.L) (F := Discrete.functor (ofParallelHoms J f g).left)
            (Fan.mk X fun (x : J.L) ↦ Iso.hom (Iso.refl X)))) ≫
      f ≫ Fan.proj (Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y)) x =
    Fan.proj (Fan.mk X fun (x : J.L) ↦ Iso.hom (Iso.refl X)) (J.fst x) ≫ (ofParallelHoms J f g).fst x
⊢ (Iso.hom
          (Iso.refl
            (Cone.pt.{u_1, v, u_1, u} (J := Discrete J.L) (F := Discrete.functor (ofParallelHoms J f g).left)
              (Fan.mk X fun (x : J.L) ↦ Iso.hom (Iso.refl X)))) ≫
        f) ≫
      Fan.proj (Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y)) x =
    ((ofParallelHoms J f g).fstPiMapOfIsLimit (Fan.mk X fun (x : J.L) ↦ Iso.hom (Iso.refl X)) (d :=
          Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y)) (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
        Iso.hom
          (Iso.refl
            (Cone.pt.{u_2, v, u_2, u} (J := Discrete J.R) (F := Discrete.functor (ofParallelHoms J f g).right)
              (Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y))))) ≫
      Fan.proj (Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y)) x

Tactic:
rw [Category.assoc, Iso.refl_hom ((Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt),
      Category.comp_id, fstPiMapOfIsLimit_proj]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Fan.mk, CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimit_proj, CategoryTheory.Iso.refl, CategoryTheory.Category.comp_id, CategoryTheory.Limits.Cone.pt, CategoryTheory.Iso.hom, CategoryTheory.Iso.refl_hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J_1 C
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
inst_1 : HasProduct.{w, v, u} I.left
inst_2 : HasProduct.{w', v, u} I.right
J : MulticospanShape
inst_3 : Unique J.L
inst_4 : Unique J.R
X Y : C
f g : X ⟶ Y
x : J.R
⊢ Iso.hom
        (Iso.refl
          (Cone.pt.{u_1, v, u_1, u} (J := Discrete J.L) (F := Discrete.functor (ofParallelHoms J f g).left)
            (Fan.mk X fun (x : J.L) ↦ Iso.hom (Iso.refl X)))) ≫
      f ≫ Fan.proj (Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y)) x =
    Fan.proj (Fan.mk X fun (x : J.L) ↦ Iso.hom (Iso.refl X)) (J.fst x) ≫ (ofParallelHoms J f g).fst x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J_1 C
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
inst_1 : HasProduct.{w, v, u} I.left
inst_2 : HasProduct.{w', v, u} I.right
J : MulticospanShape
inst_3 : Unique J.L
inst_4 : Unique J.R
X Y : C
f g : X ⟶ Y
⊢ Iso.hom
        (Iso.refl
          (Cone.pt.{u_1, v, u_1, u} (J := Discrete J.L) (F := Discrete.functor (ofParallelHoms J f g).left)
            (Fan.mk X fun (x : J.L) ↦ Iso.hom (Iso.refl X)))) ≫
      g =
    (ofParallelHoms J f g).sndPiMapOfIsLimit (Fan.mk X fun (x : J.L) ↦ Iso.hom (Iso.refl X)) (d :=
        Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y)) (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
      Iso.hom
        (Iso.refl
          (Cone.pt.{u_2, v, u_2, u} (J := Discrete J.R) (F := Discrete.functor (ofParallelHoms J f g).right)
            (Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y))))

Tactic:
Fan.IsLimit.hom_ext (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) _ _ fun _ ↦ ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Fan.isLimitMkOfUnique, CategoryTheory.Limits.MulticospanShape.R, CategoryTheory.Limits.Fan.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J_1 C
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
inst_1 : HasProduct.{w, v, u} I.left
inst_2 : HasProduct.{w', v, u} I.right
J : MulticospanShape
inst_3 : Unique J.L
inst_4 : Unique J.R
X Y : C
f g : X ⟶ Y
refine_2 :
  ∀ (x : J.R),
    (Iso.hom
            (Iso.refl
              (Cone.pt.{u_1, v, u_1, u} (J := Discrete J.L) (F := Discrete.functor (ofParallelHoms J f g).left)
                (Fan.mk X fun (x : J.L) ↦ Iso.hom (Iso.refl X)))) ≫
          g) ≫
        Fan.proj (Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y)) x =
      ((ofParallelHoms J f g).sndPiMapOfIsLimit (Fan.mk X fun (x : J.L) ↦ Iso.hom (Iso.refl X)) (d :=
            Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y)) (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
          Iso.hom
            (Iso.refl
              (Cone.pt.{u_2, v, u_2, u} (J := Discrete J.R) (F := Discrete.functor (ofParallelHoms J f g).right)
                (Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y))))) ≫
        Fan.proj (Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y)) x
⊢ Iso.hom
        (Iso.refl
          (Cone.pt.{u_1, v, u_1, u} (J := Discrete J.L) (F := Discrete.functor (ofParallelHoms J f g).left)
            (Fan.mk X fun (x : J.L) ↦ Iso.hom (Iso.refl X)))) ≫
      g =
    (ofParallelHoms J f g).sndPiMapOfIsLimit (Fan.mk X fun (x : J.L) ↦ Iso.hom (Iso.refl X)) (d :=
        Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y)) (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
      Iso.hom
        (Iso.refl
          (Cone.pt.{u_2, v, u_2, u} (J := Discrete J.R) (F := Discrete.functor (ofParallelHoms J f g).right)
            (Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y))))

Tactic:
refine Fan.IsLimit.hom_ext (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) _ _ fun _ ↦ ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Fan.isLimitMkOfUnique, CategoryTheory.Limits.MulticospanShape.R, CategoryTheory.Limits.Fan.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J_1 C
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
inst_1 : HasProduct.{w, v, u} I.left
inst_2 : HasProduct.{w', v, u} I.right
J : MulticospanShape
inst_3 : Unique J.L
inst_4 : Unique J.R
X Y : C
f g : X ⟶ Y
x : J.R
refine_2 :
  Iso.hom
        (Iso.refl
          (Cone.pt.{u_1, v, u_1, u} (J := Discrete J.L) (F := Discrete.functor (ofParallelHoms J f g).left)
            (Fan.mk X fun (x : J.L) ↦ Iso.hom (Iso.refl X)))) ≫
      g ≫ Fan.proj (Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y)) x =
    Fan.proj (Fan.mk X fun (x : J.L) ↦ Iso.hom (Iso.refl X)) (J.snd x) ≫ (ofParallelHoms J f g).snd x
⊢ (Iso.hom
          (Iso.refl
            (Cone.pt.{u_1, v, u_1, u} (J := Discrete J.L) (F := Discrete.functor (ofParallelHoms J f g).left)
              (Fan.mk X fun (x : J.L) ↦ Iso.hom (Iso.refl X)))) ≫
        g) ≫
      Fan.proj (Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y)) x =
    ((ofParallelHoms J f g).sndPiMapOfIsLimit (Fan.mk X fun (x : J.L) ↦ Iso.hom (Iso.refl X)) (d :=
          Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y)) (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
        Iso.hom
          (Iso.refl
            (Cone.pt.{u_2, v, u_2, u} (J := Discrete J.R) (F := Discrete.functor (ofParallelHoms J f g).right)
              (Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y))))) ≫
      Fan.proj (Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y)) x

Tactic:
rw [Category.assoc, Iso.refl_hom ((Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt),
      Category.comp_id, sndPiMapOfIsLimit_proj]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit_proj, CategoryTheory.Limits.Fan.mk, CategoryTheory.Iso.refl, CategoryTheory.Category.comp_id, CategoryTheory.Limits.Cone.pt, CategoryTheory.Iso.hom, CategoryTheory.Iso.refl_hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J_1 C
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
inst_1 : HasProduct.{w, v, u} I.left
inst_2 : HasProduct.{w', v, u} I.right
J : MulticospanShape
inst_3 : Unique J.L
inst_4 : Unique J.R
X Y : C
f g : X ⟶ Y
x : J.R
⊢ Iso.hom
        (Iso.refl
          (Cone.pt.{u_1, v, u_1, u} (J := Discrete J.L) (F := Discrete.functor (ofParallelHoms J f g).left)
            (Fan.mk X fun (x : J.L) ↦ Iso.hom (Iso.refl X)))) ≫
      g ≫ Fan.proj (Fan.mk Y fun (x : J.R) ↦ Iso.hom (Iso.refl Y)) x =
    Fan.proj (Fan.mk X fun (x : J.L) ↦ Iso.hom (Iso.refl X)) (J.snd x) ≫ (ofParallelHoms J f g).snd x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MulticospanShape
inst_1 : Unique J.L
inst_2 : Unique J.R
X Y : C
f g : X ⟶ Y
c : Multifork (ofParallelHoms J f g)
⊢ ((multiforkOfParallelHomsEquivFork J f g).functor.obj c).ι = c.ι default

Tactic:
Fan.IsLimit.fac (Fan.isLimitMkOfUnique (Iso.refl X) J.L) _ default

Premises used: Inhabited.default, CategoryTheory.Limits.Fan.proj, CategoryTheory.Limits.MulticospanShape.L, CategoryTheory.Iso.refl, CategoryTheory.Limits.Fan.IsLimit.fac, CategoryTheory.Limits.Fan.isLimitMkOfUnique, CategoryTheory.Limits.Fork.ι, CategoryTheory.Limits.MulticospanIndex.multicospan, CategoryTheory.Limits.Fan.IsLimit.lift
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J : MulticospanShape
inst_1 : Unique J.L
inst_2 : Unique J.R
X Y : C
f g : X ⟶ Y
c : Fork f g
a : J.L
⊢ ((multiforkOfParallelHomsEquivFork J f g).inverse.obj c).ι a = c.ι

Tactic:
simp [multiforkOfParallelHomsEquivFork]

Premises used: CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork
-- 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
K : Multicofork I
b : J.R
⊢ K.ι.app (WalkingMultispan.right b) = K.π b

Tactic:
rfl

Premises used: CategoryTheory.Limits.Multicofork.π, 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
K : Multicofork I
a : J.L
rw : I.multispan.map (WalkingMultispan.Hom.fst a) ≫ K.ι.app (WalkingMultispan.right (J.fst a)) = I.fst a ≫ K.π (J.fst a)
⊢ K.ι.app (WalkingMultispan.left a) = I.fst a ≫ K.π (J.fst a)

Tactic:
rw [← K.w (WalkingMultispan.Hom.fst a)]

Premises used: CategoryTheory.Limits.WalkingMultispan.Hom.fst, CategoryTheory.Limits.Cocone.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
K : Multicofork I
a : J.L
⊢ I.multispan.map (WalkingMultispan.Hom.fst a) ≫ K.ι.app (WalkingMultispan.right (J.fst a)) = I.fst a ≫ K.π (J.fst a)

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
K : Multicofork I
a : J.L
rw : I.multispan.map (WalkingMultispan.Hom.snd a) ≫ K.ι.app (WalkingMultispan.right (J.snd a)) = I.snd a ≫ K.π (J.snd a)
⊢ K.ι.app (WalkingMultispan.left a) = I.snd a ≫ K.π (J.snd a)

Tactic:
rw [← K.w (WalkingMultispan.Hom.snd a)]

Premises used: CategoryTheory.Limits.Cocone.w, CategoryTheory.Limits.WalkingMultispan.Hom.snd
-- 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
K : Multicofork I
a : J.L
⊢ I.multispan.map (WalkingMultispan.Hom.snd a) ≫ K.ι.app (WalkingMultispan.right (J.snd a)) = I.snd a ≫ K.π (J.snd a)

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
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
b : J.R
⊢ K₁.π b ≫ f.hom = K₂.π b

Tactic:
f.w _

Premises used: CategoryTheory.Limits.CoconeMorphism.w, CategoryTheory.Limits.Multicofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
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
left : I.multispan.map (𝟙 (WalkingMultispan.left a)) ≫ I.fst a ≫ π (J.fst a) = (I.fst a ≫ π (J.fst a)) ≫ 𝟙 P
⊢ Eq (α :=
    I.multispan.obj (WalkingMultispan.left a) ⟶
      Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) P) (WalkingMultispan.left a))
    (I.multispan.map (WalkingMultispan.Hom.id (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)
    (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.id (WalkingMultispan.left a))))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
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
left : I.fst a ≫ π (J.fst a) = (I.fst a ≫ π (J.fst a)) ≫ 𝟙 P
⊢ Eq (α :=
    I.multispan.obj (WalkingMultispan.left a) ⟶
      Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) P) (WalkingMultispan.right (J.fst a)))
    (I.multispan.map (WalkingMultispan.Hom.fst a) ≫
      match (motive :=
        (x : WalkingMultispan J) →
          I.multispan.obj x ⟶ Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) P) x)
        WalkingMultispan.right (J.fst 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.fst a)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
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
left : I.snd a ≫ π (J.snd a) = (I.fst a ≫ π (J.fst a)) ≫ 𝟙 P
⊢ 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)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
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
right : I.multispan.map (𝟙 (WalkingMultispan.right a)) ≫ π a = π a ≫ 𝟙 P
⊢ 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))))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
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.multispan.map (𝟙 (WalkingMultispan.left a)) ≫ I.fst a ≫ π (J.fst a) = (I.fst a ≫ π (J.fst a)) ≫ 𝟙 P

Tactic:
simp only [Functor.map_id, MultispanIndex.multispan_obj_left,
            Category.id_comp, Category.comp_id, MultispanIndex.multispan_obj_right]

Premises used: CategoryTheory.Limits.MultispanIndex.multispan_obj_right, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Limits.MultispanIndex.multispan_obj_left, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
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.fst a ≫ π (J.fst a) = (I.fst a ≫ π (J.fst a)) ≫ 𝟙 P

Tactic:
simp only [Functor.map_id, MultispanIndex.multispan_obj_left,
            Category.id_comp, Category.comp_id, MultispanIndex.multispan_obj_right]

Premises used: CategoryTheory.Limits.MultispanIndex.multispan_obj_right, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Limits.MultispanIndex.multispan_obj_left, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
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
left : I.snd a ≫ π (J.snd a) = I.fst a ≫ π (J.fst a)
⊢ I.snd a ≫ π (J.snd a) = (I.fst a ≫ π (J.fst a)) ≫ 𝟙 P

Tactic:
simp only [Functor.map_id, MultispanIndex.multispan_obj_left,
            Category.id_comp, Category.comp_id, MultispanIndex.multispan_obj_right]

Premises used: CategoryTheory.Limits.MultispanIndex.multispan_obj_right, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Limits.MultispanIndex.multispan_obj_left, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
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
⊢ I.multispan.map (𝟙 (WalkingMultispan.right a)) ≫ π a = π a ≫ 𝟙 P

Tactic:
simp only [Functor.map_id, MultispanIndex.multispan_obj_left,
            Category.id_comp, Category.comp_id, MultispanIndex.multispan_obj_right]

Premises used: CategoryTheory.Limits.MultispanIndex.multispan_obj_right, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Limits.MultispanIndex.multispan_obj_left, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
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
left : I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)
⊢ I.snd a ≫ π (J.snd a) = I.fst a ≫ π (J.fst a)

Tactic:
symm