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 : 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.right b)) (lift E ≫ K.π.app (WalkingMulticospan.right b))
    (E.π.app (WalkingMulticospan.right b))
have right : (lift E ≫ K.π.app (WalkingMulticospan.left (J.fst b))) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst b) =
  E.π.app (WalkingMulticospan.left (J.fst b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst b)
Tactic: rw [← E.w (WalkingMulticospan.Hom.fst b), ← K.w (WalkingMulticospan.Hom.fst b), ←
          Category.assoc]
-- 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
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
⊢ (lift E ≫ K.π.app (WalkingMulticospan.left (J.fst b))) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst b) =
    E.π.app (WalkingMulticospan.left (J.fst b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst b)
have right : 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: congr 1
-- 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
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
⊢ m = lift E
have a : ∀ (i : J.L), m ≫ K.ι i = ι E 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 : 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
⊢ f = g
have apply : ∀ (j : WalkingMulticospan J), f ≫ K.π.app j = g ≫ K.π.app j
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 : 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
⊢ Eq (α := T ⟶ I.multicospan.obj (WalkingMulticospan.right b)) (f ≫ K.π.app (WalkingMulticospan.right b))
    (g ≫ K.π.app (WalkingMulticospan.right b))
have 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)
Tactic: dsimp
-- 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
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
⊢ 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)
have right : f ≫ K.ι (J.fst b) ≫ I.fst b = g ≫ K.ι (J.fst b) ≫ I.fst b
Tactic: rw [app_right_eq_ι_comp_fst, reassoc_of% h]
-- 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
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
⊢ 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)
have right₁ : g ≫ K.ι (J.fst b) ≫ I.fst b = g ≫ K.ι (J.fst b) ≫ I.fst b
Tactic: rw [app_right_eq_ι_comp_fst, reassoc_of% h]
-- 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
K : Multifork I
c : Fan.{w, v, u} I.left
hc : IsLimit c
d : Fan.{w', v, u} I.right
hd : IsLimit d
⊢ Fan.IsLimit.lift hc K.ι ≫ I.fstPiMapOfIsLimit c hd = Fan.IsLimit.lift hc K.ι ≫ I.sndPiMapOfIsLimit c hd
have 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
Tactic: apply Fan.IsLimit.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
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.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))
have left : 𝟙 a.pt ≫ a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1 = (a.ι ≫ c.proj (J.snd a_1)) ≫ I.snd a_1
Tactic: dsimp
-- 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
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.fstPiMapOfIsLimit c hd ≫ d.proj a_1 = (a.ι ≫ c.proj (J.snd a_1)) ≫ I.snd a_1
have left : 𝟙 a.pt ≫ a.ι ≫ I.sndPiMapOfIsLimit c hd ≫ d.proj a_1 = (a.ι ≫ c.proj (J.snd a_1)) ≫ I.snd a_1
Tactic: rw [a.condition_assoc]
-- 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
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₂
⊢ f.hom ≫ (Multifork.toPiFork hc hd K₂).π.app WalkingParallelPair.zero =
    (Multifork.toPiFork hc hd K₁).π.app WalkingParallelPair.zero
have 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
Tactic: apply Fan.IsLimit.hom_ext hc
-- 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
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₂
⊢ f.hom ≫ (Multifork.toPiFork hc hd K₂).π.app WalkingParallelPair.one =
    (Multifork.toPiFork hc hd K₁).π.app WalkingParallelPair.one
have 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
Tactic: apply Fan.IsLimit.hom_ext hd
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
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
⊢ Multifork (ofParallelHoms J f g) ≌ Fork f g
have 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))))
Tactic: refine (multiforkEquivPiForkOfIsLimit _
      (Fan.isLimitMkOfUnique (Iso.refl X) _) (Fan.isLimitMkOfUnique (Iso.refl Y) _)).trans
      (Fork.equivOfIsos (.refl _) (.refl _) ?_ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
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))))
⊢ Multifork (ofParallelHoms J f g) ≌ Fork f g
have 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))))
Tactic: refine (multiforkEquivPiForkOfIsLimit _
      (Fan.isLimitMkOfUnique (Iso.refl X) _) (Fan.isLimitMkOfUnique (Iso.refl Y) _)).trans
      (Fork.equivOfIsos (.refl _) (.refl _) ?_ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
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))))
have 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
Tactic: refine Fan.IsLimit.hom_ext (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) _ _ fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
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 =
    ((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
have 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
Tactic: rw [Category.assoc, Iso.refl_hom ((Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt),
      Category.comp_id, fstPiMapOfIsLimit_proj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
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))))
have 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
Tactic: refine Fan.IsLimit.hom_ext (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) _ _ fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
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 =
    ((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
have 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
Tactic: rw [Category.assoc, Iso.refl_hom ((Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt),
      Category.comp_id, sndPiMapOfIsLimit_proj]
-- 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
⊢ K.ι.app (WalkingMultispan.left a) = I.fst a ≫ K.π (J.fst a)
have rw : I.multispan.map (WalkingMultispan.Hom.fst a) ≫ K.ι.app (WalkingMultispan.right (J.fst a)) = I.fst a ≫ K.π (J.fst a)
Tactic: rw [← K.w (WalkingMultispan.Hom.fst a)]
-- 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
⊢ K.ι.app (WalkingMultispan.left a) = I.snd a ≫ K.π (J.snd a)
have rw : I.multispan.map (WalkingMultispan.Hom.snd a) ≫ K.ι.app (WalkingMultispan.right (J.snd a)) = I.snd a ≫ K.π (J.snd a)
Tactic: rw [← K.w (WalkingMultispan.Hom.snd a)]
-- 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.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))))
have left : I.multispan.map (𝟙 (WalkingMultispan.left a)) ≫ I.fst a ≫ π (J.fst 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.L
⊢ 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)))
have left : I.fst a ≫ π (J.fst a) = (I.fst a ≫ π (J.fst a)) ≫ 𝟙 P
Tactic: dsimp