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
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : J.L), lift E ≫ K.ι i = E.ι i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), m ≫ K.ι i = E.ι i) → m = lift E
E : Cone I.multicospan
b : J.R
⊢ Eq (α := E.pt ⟶ I.multicospan.obj (WalkingMulticospan.left (J.fst b)))
    (lift E ≫ K.π.app (WalkingMulticospan.left (J.fst b))) (E.π.app (WalkingMulticospan.left (J.fst b)))

Tactic:
apply fac
-- 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
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : J.L), lift E ≫ K.ι i = E.ι i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), m ≫ K.ι i = E.ι i) → m = lift E
E : Cone I.multicospan
m : E.pt ⟶ K.pt
hm : ∀ (j : WalkingMulticospan J), m ≫ K.π.app j = E.π.app j
a : ∀ (i : J.L), m ≫ K.ι i = ι E i
⊢ m = lift E

Tactic:
apply uniq
-- 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
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : J.L), lift E ≫ K.ι i = E.ι i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), m ≫ K.ι i = E.ι i) → m = lift E
E : Cone I.multicospan
m : E.pt ⟶ K.pt
hm : ∀ (j : WalkingMulticospan J), m ≫ K.π.app j = E.π.app j
i : J.L
⊢ m ≫ K.ι i = ι E i

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

Tactic:
apply hK.hom_ext

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

Tactic:
apply h
-- 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
K : Multifork I
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
b : J.R
right :
  Eq (α := T ⟶ I.right b) (f ≫ K.π.app (WalkingMulticospan.right b) : T ⟶ I.right b)
    (g ≫ K.π.app (WalkingMulticospan.right b) : T ⟶ I.right b)
⊢ Eq (α := T ⟶ I.multicospan.obj (WalkingMulticospan.right b)) (f ≫ K.π.app (WalkingMulticospan.right b))
    (g ≫ K.π.app (WalkingMulticospan.right b))

Tactic:
dsimp
-- 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
K : Multifork I
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
b : J.R
right : f ≫ K.ι (J.fst b) ≫ I.fst b = g ≫ K.ι (J.fst b) ≫ I.fst b
right₁ right₂ : g ≫ K.ι (J.fst b) ≫ I.fst b = g ≫ K.ι (J.fst b) ≫ I.fst b
⊢ Eq (α := T ⟶ I.right b) (f ≫ K.π.app (WalkingMulticospan.right b) : T ⟶ I.right b)
    (g ≫ K.π.app (WalkingMulticospan.right b) : T ⟶ I.right b)

Tactic:
rw [app_right_eq_ι_comp_fst, reassoc_of% h]

Premises used: CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_fst
-- 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
K : Multifork I
hK : IsLimit K
T : C
k : (a : J.L) → T ⟶ I.left a
hk : ∀ (b : J.R), k (J.fst b) ≫ I.fst b = k (J.snd b) ≫ I.snd b
a : J.L
⊢ lift hK k hk ≫ K.ι a = k a

Tactic:
hK.fac _ _

Premises used: CategoryTheory.Limits.Multifork.ι, CategoryTheory.Limits.Multifork.IsLimit.lift, CategoryTheory.Limits.IsLimit.fac
-- 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
K : Multifork I
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
h :
  ∀ (i : J.R),
    (Fan.IsLimit.lift hc K.ι ≫ I.fstPiMapOfIsLimit c hd) ≫ d.proj i =
      (Fan.IsLimit.lift hc K.ι ≫ I.sndPiMapOfIsLimit c hd) ≫ d.proj i
⊢ Fan.IsLimit.lift hc K.ι ≫ I.fstPiMapOfIsLimit c hd = Fan.IsLimit.lift hc K.ι ≫ I.sndPiMapOfIsLimit c hd

Tactic:
apply Fan.IsLimit.hom_ext hd

Premises used: CategoryTheory.Limits.Fan.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
K : Multifork I
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
⊢ ∀ (i : J.R),
    (Fan.IsLimit.lift hc K.ι ≫ I.fstPiMapOfIsLimit c hd) ≫ d.proj i =
      (Fan.IsLimit.lift hc K.ι ≫ I.sndPiMapOfIsLimit c hd) ≫ d.proj i

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
K_1 : Multifork I
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
K : Multifork I
⊢ Fan.IsLimit.lift hc K.ι ≫ I.fstPiMapOfIsLimit c hd = Fan.IsLimit.lift hc K.ι ≫ I.sndPiMapOfIsLimit c hd

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
K : Multifork I
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
⊢ (toPiFork hc hd K).ι = Fan.IsLimit.lift hc K.ι

Tactic:
rfl

Premises used: CategoryTheory.Limits.Fork.ι, CategoryTheory.Limits.Fan.IsLimit.lift, 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
K : Multifork I
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
⊢ (toPiFork hc hd K).π.app WalkingParallelPair.one = Fan.IsLimit.lift hc K.ι ≫ I.fstPiMapOfIsLimit c hd

Tactic:
rfl

Premises used: 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
K : Multifork I
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
a_1 : J.L
⊢ Eq.{v + 1} (α :=
    Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) a.pt) (WalkingMulticospan.left a_1) ⟶
      I.multicospan.obj (WalkingMulticospan.left a_1))
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) a.pt) (WalkingMulticospan.left a_1))
      (Functor.map (Functor.obj (Functor.const (WalkingMulticospan J)) a.pt)
        (WalkingMulticospan.Hom.id (WalkingMulticospan.left a_1)))
      (match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) a.pt) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.left a_1 with
      | WalkingMulticospan.left a_2 => a.ι ≫ c.proj a_2
      | WalkingMulticospan.right a_2 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_2))
    ((match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) a.pt) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.left a_1 with
      | WalkingMulticospan.left a_2 => a.ι ≫ c.proj a_2
      | WalkingMulticospan.right a_2 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_2) ≫
      I.multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a_1)))

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
K : Multifork I
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
a_1 : J.R
⊢ Eq.{v + 1} (α :=
    Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) a.pt) (WalkingMulticospan.left (J.fst a_1)) ⟶
      I.multicospan.obj (WalkingMulticospan.right a_1))
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) a.pt) (WalkingMulticospan.right a_1))
      (Functor.map (Functor.obj (Functor.const (WalkingMulticospan J)) a.pt) (WalkingMulticospan.Hom.fst a_1))
      (match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) a.pt) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.right a_1 with
      | WalkingMulticospan.left a_2 => a.ι ≫ c.proj a_2
      | WalkingMulticospan.right a_2 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_2))
    ((match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) a.pt) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.left (J.fst a_1) with
      | WalkingMulticospan.left a_2 => a.ι ≫ c.proj a_2
      | WalkingMulticospan.right a_2 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_2) ≫
      I.multicospan.map (WalkingMulticospan.Hom.fst a_1))

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
K : Multifork I
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
a_1 : J.R
left : 𝟙 a.pt ≫ a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1 = (a.ι ≫ c.proj (J.snd a_1)) ≫ I.snd a_1
⊢ Eq.{v + 1} (α :=
    Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) a.pt) (WalkingMulticospan.left (J.snd a_1)) ⟶
      I.multicospan.obj (WalkingMulticospan.right a_1))
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) a.pt) (WalkingMulticospan.right a_1))
      (Functor.map (Functor.obj (Functor.const (WalkingMulticospan J)) a.pt) (WalkingMulticospan.Hom.snd a_1))
      (match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) a.pt) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.right a_1 with
      | WalkingMulticospan.left a_2 => a.ι ≫ c.proj a_2
      | WalkingMulticospan.right a_2 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_2))
    ((match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) a.pt) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.left (J.snd a_1) with
      | WalkingMulticospan.left a_2 => a.ι ≫ c.proj a_2
      | WalkingMulticospan.right a_2 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_2) ≫
      I.multicospan.map (WalkingMulticospan.Hom.snd a_1))

Tactic:
dsimp
-- 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
K : Multifork I
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
a_1 : J.R
left : 𝟙 a.pt ≫ a.ι ≫ I.sndPiMapOfIsLimit c hd ≫ d.proj a_1 = (a.ι ≫ c.proj (J.snd a_1)) ≫ I.snd a_1
⊢ 𝟙 a.pt ≫ a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1 = (a.ι ≫ c.proj (J.snd a_1)) ≫ I.snd a_1

Tactic:
rw [a.condition_assoc]

Premises used: CategoryTheory.Limits.Fork.condition_assoc
-- 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
K : Multifork I
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
a_1 : J.R
⊢ 𝟙 a.pt ≫ a.ι ≫ I.sndPiMapOfIsLimit c hd ≫ d.proj a_1 = (a.ι ≫ c.proj (J.snd a_1)) ≫ I.snd a_1

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
K : Multifork I
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
a_1 : J.R
⊢ Eq.{v + 1} (α :=
    Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) a.pt) (WalkingMulticospan.right a_1) ⟶
      I.multicospan.obj (WalkingMulticospan.right a_1))
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) a.pt) (WalkingMulticospan.right a_1))
      (Functor.map (Functor.obj (Functor.const (WalkingMulticospan J)) a.pt)
        (WalkingMulticospan.Hom.id (WalkingMulticospan.right a_1)))
      (match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) a.pt) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.right a_1 with
      | WalkingMulticospan.left a_2 => a.ι ≫ c.proj a_2
      | WalkingMulticospan.right a_2 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_2))
    ((match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) a.pt) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.right a_1 with
      | WalkingMulticospan.left a_2 => a.ι ≫ c.proj a_2
      | WalkingMulticospan.right a_2 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_2) ≫
      I.multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.right a_1)))

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
c : Fan.{w, v, u} I.left
d : Fan.{w', v, u} I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
i : J.L
⊢ (ofPiFork a).ι i = a.ι ≫ c.proj i

Tactic:
rfl

Premises used: CategoryTheory.Limits.Multifork.ι, 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
c : Fan.{w, v, u} I.left
d : Fan.{w', v, u} I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
i : J.R
⊢ (ofPiFork a).π.app (WalkingMulticospan.right i) = a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj i

Tactic:
rfl

Premises used: 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
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
zero :
  ∀ (i : J.L),
    (f.hom ≫ (Multifork.toPiFork hc hd K₂).π.app WalkingParallelPair.zero) ≫ c.proj i =
      (Multifork.toPiFork hc hd K₁).π.app WalkingParallelPair.zero ≫ c.proj i
⊢ f.hom ≫ (Multifork.toPiFork hc hd K₂).π.app WalkingParallelPair.zero =
    (Multifork.toPiFork hc hd K₁).π.app WalkingParallelPair.zero

Tactic:
apply Fan.IsLimit.hom_ext hc

Premises used: CategoryTheory.Limits.Fan.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
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
⊢ ∀ (i : J.L),
    (f.hom ≫ (Multifork.toPiFork hc hd K₂).π.app WalkingParallelPair.zero) ≫ c.proj i =
      (Multifork.toPiFork hc hd K₁).π.app WalkingParallelPair.zero ≫ c.proj i

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
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
one :
  ∀ (i : J.R),
    (f.hom ≫ (Multifork.toPiFork hc hd K₂).π.app WalkingParallelPair.one) ≫ d.proj i =
      (Multifork.toPiFork hc hd K₁).π.app WalkingParallelPair.one ≫ d.proj i
⊢ f.hom ≫ (Multifork.toPiFork hc hd K₂).π.app WalkingParallelPair.one =
    (Multifork.toPiFork hc hd K₁).π.app WalkingParallelPair.one

Tactic:
apply Fan.IsLimit.hom_ext hd

Premises used: CategoryTheory.Limits.Fan.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
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
⊢ ∀ (i : J.R),
    (f.hom ≫ (Multifork.toPiFork hc hd K₂).π.app WalkingParallelPair.one) ≫ d.proj i =
      (Multifork.toPiFork hc hd K₁).π.app WalkingParallelPair.one ≫ d.proj i

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
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
K₁ K₂ : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
f : K₁ ⟶ K₂
a : J.L
⊢ Eq (α := (Multifork.ofPiFork K₁).pt ⟶ I.multicospan.obj (WalkingMulticospan.left a))
    (f.hom ≫ (Multifork.ofPiFork K₂).π.app (WalkingMulticospan.left a))
    ((Multifork.ofPiFork K₁).π.app (WalkingMulticospan.left a))

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
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
K₁ K₂ : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
f : K₁ ⟶ K₂
a : J.R
⊢ Eq (α := (Multifork.ofPiFork K₁).pt ⟶ I.multicospan.obj (WalkingMulticospan.right a))
    (f.hom ≫ (Multifork.ofPiFork K₂).π.app (WalkingMulticospan.right a))
    ((Multifork.ofPiFork K₁).π.app (WalkingMulticospan.right a))

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
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
K : Multifork I
a : J.L
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) (Functor.obj (𝟭 (Multifork I)) K).pt)
        (WalkingMulticospan.left a) ⟶
      I.multicospan.obj (WalkingMulticospan.left a))
    ((Functor.obj (𝟭 (Multifork I)) K).π.app (WalkingMulticospan.left a))
    (Iso.hom (Iso.refl (Functor.obj (𝟭 (Multifork I)) K).pt) ≫
      ((I.toPiForkFunctor hc hd ⋙ I.ofPiForkFunctor hd).obj K).π.app (WalkingMulticospan.left a))

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
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
K : Multifork I
a : J.R
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) (Functor.obj (𝟭 (Multifork I)) K).pt)
        (WalkingMulticospan.right a) ⟶
      I.multicospan.obj (WalkingMulticospan.right a))
    ((Functor.obj (𝟭 (Multifork I)) K).π.app (WalkingMulticospan.right a))
    (Iso.hom (Iso.refl (Functor.obj (𝟭 (Multifork I)) K).pt) ≫
      ((I.toPiForkFunctor hc hd ⋙ I.ofPiForkFunctor hd).obj K).π.app (WalkingMulticospan.right a))

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
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
K : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
⊢ ∀ (i : J.L),
    (Iso.hom (Iso.refl (Functor.obj (I.ofPiForkFunctor hd ⋙ I.toPiForkFunctor hc hd) K).pt) ≫
          (Functor.obj (𝟭 (Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd))) K).ι) ≫
        c.proj i =
      (Functor.obj (I.ofPiForkFunctor hd ⋙ I.toPiForkFunctor hc hd) K).ι ≫ c.proj i

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
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 =
    (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))))
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 =
    (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))))
⊢ Multifork (ofParallelHoms J f g) ≌ Fork f g

Tactic:
refine (multiforkEquivPiForkOfIsLimit _
      (Fan.isLimitMkOfUnique (Iso.refl X) _) (Fan.isLimitMkOfUnique (Iso.refl Y) _)).trans
      (Fork.equivOfIsos (.refl _) (.refl _) ?_ ?_)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Fork.equivOfIsos, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit, CategoryTheory.Equivalence.trans
-- 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)))) ≫
      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:
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