awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.snd a ≫ π (J.snd a)

Tactic:
apply 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
rw : I.fst a ≫ K.π (J.fst a) = K.ι.app (WalkingMultispan.left a)
rw₁ 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))
⊢ I.fst a ≫ K.π (J.fst a) = I.snd a ≫ K.π (J.snd a)

Tactic:
rw [← K.snd_app_right, ← K.fst_app_right]

Premises used: CategoryTheory.Limits.Multicofork.fst_app_right, CategoryTheory.Limits.Multicofork.snd_app_right
-- 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
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
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))
⊢ Eq (α := I.multispan.obj (WalkingMultispan.left a) ⟶ S.pt) (K.ι.app (WalkingMultispan.left a) ≫ desc S)
    (S.ι.app (WalkingMultispan.left a))

Tactic:
rw [← K.w (WalkingMultispan.Hom.fst a), ← S.w (WalkingMultispan.Hom.fst a),
          Category.assoc]

Premises used: CategoryTheory.Category.assoc, 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
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
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)))
⊢ 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:
congr 1
-- 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
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.right (J.fst a)) ⟶ S.pt)
    (K.ι.app (WalkingMultispan.right (J.fst a)) ≫ desc S) (S.ι.app (WalkingMultispan.right (J.fst a)))

Tactic:
apply fac
-- 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
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
b : J.R
⊢ Eq (α := I.multispan.obj (WalkingMultispan.right b) ⟶ S.pt) (K.ι.app (WalkingMultispan.right b) ≫ desc S)
    (S.ι.app (WalkingMultispan.right b))

Tactic:
apply fac
-- 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
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
a : ∀ (i : J.R), K.π i ≫ m = π S i
⊢ m = desc S

Tactic:
apply uniq
-- 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
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
i : J.R
⊢ K.π i ≫ m = π S i

Tactic:
apply hm
-- 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
hK : IsColimit K
T : C
f g : K.pt ⟶ T
h : ∀ (a : J.R), K.π a ≫ f = K.π a ≫ g
apply : ∀ (j : WalkingMultispan J), K.ι.app j ≫ f = K.ι.app j ≫ g
⊢ f = g

Tactic:
apply hK.hom_ext

Premises used: CategoryTheory.Limits.IsColimit.hom_ext
-- 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
hK : IsColimit K
T : C
f g : K.pt ⟶ T
h : ∀ (a : J.R), K.π a ≫ f = K.π a ≫ g
a : J.L
⊢ Eq (α := I.multispan.obj (WalkingMultispan.left a) ⟶ T) (K.ι.app (WalkingMultispan.left a) ≫ f)
    (K.ι.app (WalkingMultispan.left a) ≫ g)

Tactic:
simp [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
K : Multicofork I
hK : IsColimit K
T : C
f g : K.pt ⟶ T
h : ∀ (a : J.R), K.π a ≫ f = K.π a ≫ g
a : J.R
⊢ Eq (α := I.multispan.obj (WalkingMultispan.right a) ⟶ T) (K.ι.app (WalkingMultispan.right a) ≫ f)
    (K.ι.app (WalkingMultispan.right a) ≫ g)

Tactic:
simp [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
K : Multicofork I
hK : IsColimit K
T : C
k : (a : J.R) → I.right a ⟶ T
hk : ∀ (b : J.L), I.fst b ≫ k (J.fst b) = I.snd b ≫ k (J.snd b)
a : J.R
⊢ K.π a ≫ desc hK k hk = k a

Tactic:
hK.fac _ _

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.Multicofork.IsColimit.desc, CategoryTheory.Limits.Multicofork.π
-- 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
c : Cofan.{w, v, u} I.left
hc : IsColimit c
d : Cofan.{w', v, u} I.right
hd : IsColimit d
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.π
⊢ I.fstSigmaMapOfIsColimit d hc ≫ Cofan.IsColimit.desc hd K.π =
    I.sndSigmaMapOfIsColimit d hc ≫ Cofan.IsColimit.desc hd K.π

Tactic:
apply Cofan.IsColimit.hom_ext hc

Premises used: CategoryTheory.Limits.Cofan.IsColimit.hom_ext
-- 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
c : Cofan.{w, v, u} I.left
hc : IsColimit c
d : Cofan.{w', v, u} I.right
hd : IsColimit d
⊢ ∀ (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:
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
K_1 : Multicofork I
c : Cofan.{w, v, u} I.left
hc : IsColimit c
d : Cofan.{w', v, u} I.right
hd : IsColimit d
K : Multicofork I
⊢ I.fstSigmaMapOfIsColimit d hc ≫ Cofan.IsColimit.desc hd K.π =
    I.sndSigmaMapOfIsColimit d hc ≫ Cofan.IsColimit.desc hd K.π

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
K : Multicofork I
c : Cofan.{w, v, u} I.left
hc : IsColimit c
d : Cofan.{w', v, u} I.right
hd : IsColimit d
⊢ (toSigmaCofork hc hd K).π = Cofan.IsColimit.desc hd K.π

Tactic:
rfl

Premises used: CategoryTheory.Limits.Cofan.IsColimit.desc, rfl, CategoryTheory.Limits.Cofork.π
-- 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
c : Cofan.{w, v, u} I.left
hc : IsColimit c
d : Cofan.{w', v, u} I.right
hd : IsColimit d
a : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
a_1 : J.L
⊢ Eq (α :=
    I.multispan.obj (WalkingMultispan.left a_1) ⟶
      Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) a.pt) (WalkingMultispan.left a_1))
    (I.multispan.map (WalkingMultispan.Hom.id (WalkingMultispan.left a_1)) ≫
      match (motive :=
        (x : WalkingMultispan J) →
          I.multispan.obj x ⟶ Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) a.pt) x)
        WalkingMultispan.left a_1 with
      | WalkingMultispan.left a_2 => c.inj a_2 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
      | WalkingMultispan.right a_2 => d.inj a_2 ≫ a.π)
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) a.pt) (WalkingMultispan.left a_1))
      (match (motive :=
        (x : WalkingMultispan J) →
          I.multispan.obj x ⟶ Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) a.pt) x)
        WalkingMultispan.left a_1 with
      | WalkingMultispan.left a_2 => c.inj a_2 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
      | WalkingMultispan.right a_2 => d.inj a_2 ≫ a.π)
      (Functor.map (Functor.obj (Functor.const (WalkingMultispan J)) a.pt)
        (WalkingMultispan.Hom.id (WalkingMultispan.left a_1))))

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
K : Multicofork I
c : Cofan.{w, v, u} I.left
hc : IsColimit c
d : Cofan.{w', v, u} I.right
hd : IsColimit d
a : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
a_1 : J.L
⊢ Eq (α :=
    I.multispan.obj (WalkingMultispan.left a_1) ⟶
      Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) a.pt) (WalkingMultispan.right (J.fst a_1)))
    (I.multispan.map (WalkingMultispan.Hom.fst a_1) ≫
      match (motive :=
        (x : WalkingMultispan J) →
          I.multispan.obj x ⟶ Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) a.pt) x)
        WalkingMultispan.right (J.fst a_1) with
      | WalkingMultispan.left a_2 => c.inj a_2 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
      | WalkingMultispan.right a_2 => d.inj a_2 ≫ a.π)
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) a.pt) (WalkingMultispan.left a_1))
      (match (motive :=
        (x : WalkingMultispan J) →
          I.multispan.obj x ⟶ Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) a.pt) x)
        WalkingMultispan.left a_1 with
      | WalkingMultispan.left a_2 => c.inj a_2 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
      | WalkingMultispan.right a_2 => d.inj a_2 ≫ a.π)
      (Functor.map (Functor.obj (Functor.const (WalkingMultispan J)) a.pt) (WalkingMultispan.Hom.fst a_1)))

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
K : Multicofork I
c : Cofan.{w, v, u} I.left
hc : IsColimit c
d : Cofan.{w', v, u} I.right
hd : IsColimit d
a : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
a_1 : J.L
⊢ Eq (α :=
    I.multispan.obj (WalkingMultispan.left a_1) ⟶
      Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) a.pt) (WalkingMultispan.right (J.snd a_1)))
    (I.multispan.map (WalkingMultispan.Hom.snd a_1) ≫
      match (motive :=
        (x : WalkingMultispan J) →
          I.multispan.obj x ⟶ Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) a.pt) x)
        WalkingMultispan.right (J.snd a_1) with
      | WalkingMultispan.left a_2 => c.inj a_2 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
      | WalkingMultispan.right a_2 => d.inj a_2 ≫ a.π)
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) a.pt) (WalkingMultispan.left a_1))
      (match (motive :=
        (x : WalkingMultispan J) →
          I.multispan.obj x ⟶ Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) a.pt) x)
        WalkingMultispan.left a_1 with
      | WalkingMultispan.left a_2 => c.inj a_2 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
      | WalkingMultispan.right a_2 => d.inj a_2 ≫ a.π)
      (Functor.map (Functor.obj (Functor.const (WalkingMultispan J)) a.pt) (WalkingMultispan.Hom.snd a_1)))

Tactic:
simp [a.condition]

Premises used: CategoryTheory.Limits.Cofork.condition
-- 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
c : Cofan.{w, v, u} I.left
hc : IsColimit c
d : Cofan.{w', v, u} I.right
hd : IsColimit d
a : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
a_1 : J.R
⊢ Eq (α :=
    I.multispan.obj (WalkingMultispan.right a_1) ⟶
      Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) a.pt) (WalkingMultispan.right a_1))
    (I.multispan.map (WalkingMultispan.Hom.id (WalkingMultispan.right a_1)) ≫
      match (motive :=
        (x : WalkingMultispan J) →
          I.multispan.obj x ⟶ Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) a.pt) x)
        WalkingMultispan.right a_1 with
      | WalkingMultispan.left a_2 => c.inj a_2 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
      | WalkingMultispan.right a_2 => d.inj a_2 ≫ a.π)
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) a.pt) (WalkingMultispan.right a_1))
      (match (motive :=
        (x : WalkingMultispan J) →
          I.multispan.obj x ⟶ Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) a.pt) x)
        WalkingMultispan.right a_1 with
      | WalkingMultispan.left a_2 => c.inj a_2 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
      | WalkingMultispan.right a_2 => d.inj a_2 ≫ a.π)
      (Functor.map (Functor.obj (Functor.const (WalkingMultispan J)) a.pt)
        (WalkingMultispan.Hom.id (WalkingMultispan.right a_1))))

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
c : Cofan.{w, v, u} I.left
hc : IsColimit c
d : Cofan.{w', v, u} I.right
a : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
i : J.L
⊢ (ofSigmaCofork a).ι.app (WalkingMultispan.left i) = c.inj i ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π

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
c : Cofan.{w, v, u} I.left
hc : IsColimit c
d : Cofan.{w', v, u} I.right
a : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
i : J.R
⊢ (ofSigmaCofork a).π i = d.inj i ≫ a.π

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_1 : Multicofork I
c : Cofan.{w, v, u} I.left
hc : IsColimit c
d : Cofan.{w', v, u} I.right
hd : IsColimit d
K K' : Multicofork I
e : K.pt ≅ K'.pt
h : ∀ (i : J.R), K.π i ≫ e.hom = K'.π i
i : J.L
⊢ Eq (α := I.multispan.obj (WalkingMultispan.left i) ⟶ K'.pt) (K.ι.app (WalkingMultispan.left i) ≫ e.hom)
    (K'.ι.app (WalkingMultispan.left i))

Tactic:
simp [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
K_1 : Multicofork I
c : Cofan.{w, v, u} I.left
hc : IsColimit c
d : Cofan.{w', v, u} I.right
hd : IsColimit d
K K' : Multicofork I
e : K.pt ≅ K'.pt
h : ∀ (i : J.R), K.π i ≫ e.hom = K'.π i
j : J.R
⊢ Eq (α := I.multispan.obj (WalkingMultispan.right j) ⟶ K'.pt) (K.ι.app (WalkingMultispan.right j) ≫ e.hom)
    (K'.ι.app (WalkingMultispan.right j))

Tactic:
simp [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
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₂
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
⊢ (Multicofork.toSigmaCofork hc hd K₁).ι.app WalkingParallelPair.zero ≫ f.hom =
    (Multicofork.toSigmaCofork hc hd K₂).ι.app WalkingParallelPair.zero

Tactic:
apply Cofan.IsColimit.hom_ext hc

Premises used: CategoryTheory.Limits.Cofan.IsColimit.hom_ext
-- 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
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₂
⊢ ∀ (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:
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
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₂
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
⊢ (Multicofork.toSigmaCofork hc hd K₁).ι.app WalkingParallelPair.one ≫ f.hom =
    (Multicofork.toSigmaCofork hc hd K₂).ι.app WalkingParallelPair.one

Tactic:
apply Cofan.IsColimit.hom_ext hd

Premises used: CategoryTheory.Limits.Cofan.IsColimit.hom_ext
-- 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
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₂
⊢ ∀ (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:
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
c : Cofan.{w, v, u} I.left
hc : IsColimit c
d : Cofan.{w', v, u} I.right
hd : IsColimit d
K₁ K₂ : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
f : K₁ ⟶ K₂
a : J.L
⊢ Eq (α := I.multispan.obj (WalkingMultispan.left a) ⟶ (Multicofork.ofSigmaCofork K₂).pt)
    ((Multicofork.ofSigmaCofork K₁).ι.app (WalkingMultispan.left a) ≫ f.hom)
    ((Multicofork.ofSigmaCofork K₂).ι.app (WalkingMultispan.left a))

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
c : Cofan.{w, v, u} I.left
hc : IsColimit c
d : Cofan.{w', v, u} I.right
hd : IsColimit d
K₁ K₂ : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
f : K₁ ⟶ K₂
a : J.R
⊢ Eq (α := I.multispan.obj (WalkingMultispan.right a) ⟶ (Multicofork.ofSigmaCofork K₂).pt)
    ((Multicofork.ofSigmaCofork K₁).ι.app (WalkingMultispan.right a) ≫ f.hom)
    ((Multicofork.ofSigmaCofork K₂).ι.app (WalkingMultispan.right a))

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
c : Cofan.{w, v, u} I.left
hc : IsColimit c
d : Cofan.{w', v, u} I.right
hd : IsColimit d
K : Multicofork I
a : J.L
⊢ Eq (α :=
    I.multispan.obj (WalkingMultispan.left a) ⟶ ((I.toSigmaCoforkFunctor hc hd ⋙ I.ofSigmaCoforkFunctor hc).obj K).pt)
    ((Functor.obj (𝟭 (Multicofork I)) K).ι.app (WalkingMultispan.left a) ≫
      Iso.hom (Iso.refl (Functor.obj (𝟭 (Multicofork I)) K).pt))
    (((I.toSigmaCoforkFunctor hc hd ⋙ I.ofSigmaCoforkFunctor hc).obj K).ι.app (WalkingMultispan.left a))

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
c : Cofan.{w, v, u} I.left
hc : IsColimit c
d : Cofan.{w', v, u} I.right
hd : IsColimit d
K : Multicofork I
a : J.R
⊢ Eq (α :=
    I.multispan.obj (WalkingMultispan.right a) ⟶ ((I.toSigmaCoforkFunctor hc hd ⋙ I.ofSigmaCoforkFunctor hc).obj K).pt)
    ((Functor.obj (𝟭 (Multicofork I)) K).ι.app (WalkingMultispan.right a) ≫
      Iso.hom (Iso.refl (Functor.obj (𝟭 (Multicofork I)) K).pt))
    (((I.toSigmaCoforkFunctor hc hd ⋙ I.ofSigmaCoforkFunctor hc).obj K).ι.app (WalkingMultispan.right a))

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
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)
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).π
⊢ (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).π

Tactic:
apply Cofan.IsColimit.hom_ext hd

Premises used: CategoryTheory.Limits.Cofan.IsColimit.hom_ext
-- 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
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)
⊢ ∀ (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:
simp
-- 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
⊢ (multifork I).ι a = ι I a

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, rfl