awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
a : J.L
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C)
      (match (motive := WalkingMultispan J → C) WalkingMultispan.left a with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b :
        C)
      (match (motive := WalkingMultispan J → C) WalkingMultispan.left a with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b :
        C))
    (match (motive :=
        (x y : WalkingMultispan J) →
          (x ⟶ y) →
            Quiver.Hom.{v, u} (V := C)
              (match (motive := WalkingMultispan J → C) x with
                | WalkingMultispan.left a => I.left a
                | WalkingMultispan.right b => I.right b :
                C)
              (match (motive := WalkingMultispan J → C) y with
                | WalkingMultispan.left a => I.left a
                | WalkingMultispan.right b => I.right b :
                C))
        WalkingMultispan.left a, WalkingMultispan.left a, 𝟙 (WalkingMultispan.left a) with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match (motive := WalkingMultispan J → C) x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingMultispan J → C) WalkingMultispan.left a with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b :
          C)
        (match (motive := WalkingMultispan J → C) WalkingMultispan.left a with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b :
          C))
    (𝟙
        (match (motive := WalkingMultispan J → C) WalkingMultispan.left a with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b) :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingMultispan J → C) WalkingMultispan.left a with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b :
          C)
        (match (motive := WalkingMultispan J → C) WalkingMultispan.left a with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b :
          C))

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
a : J.R
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C)
      (match (motive := WalkingMultispan J → C) WalkingMultispan.right a with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b :
        C)
      (match (motive := WalkingMultispan J → C) WalkingMultispan.right a with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b :
        C))
    (match (motive :=
        (x y : WalkingMultispan J) →
          (x ⟶ y) →
            Quiver.Hom.{v, u} (V := C)
              (match (motive := WalkingMultispan J → C) x with
                | WalkingMultispan.left a => I.left a
                | WalkingMultispan.right b => I.right b :
                C)
              (match (motive := WalkingMultispan J → C) y with
                | WalkingMultispan.left a => I.left a
                | WalkingMultispan.right b => I.right b :
                C))
        WalkingMultispan.right a, WalkingMultispan.right a, 𝟙 (WalkingMultispan.right a) with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match (motive := WalkingMultispan J → C) x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingMultispan J → C) WalkingMultispan.right a with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b :
          C)
        (match (motive := WalkingMultispan J → C) WalkingMultispan.right a with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b :
          C))
    (𝟙
        (match (motive := WalkingMultispan J → C) WalkingMultispan.right a with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b) :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingMultispan J → C) WalkingMultispan.right a with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b :
          C)
        (match (motive := WalkingMultispan J → C) WalkingMultispan.right a with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b :
          C))

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
a : J.L
⊢ I.multispan.obj (WalkingMultispan.left a) = I.left 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
b : J.R
⊢ I.multispan.obj (WalkingMultispan.right b) = I.right b

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
a : J.L
⊢ I.multispan.map (WalkingMultispan.Hom.fst a) = I.fst 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
a : J.L
⊢ I.multispan.map (WalkingMultispan.Hom.snd a) = I.snd 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
d : Cofan.{w', v, u} I.right
hc : IsColimit c
i : J.L
⊢ c.inj i ≫ I.fstSigmaMapOfIsColimit d hc = I.fst i ≫ d.inj (J.fst i)

Tactic:
simp [fstSigmaMapOfIsColimit]

Premises used: CategoryTheory.Limits.MultispanIndex.fstSigmaMapOfIsColimit
-- 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
d : Cofan.{w', v, u} I.right
hc : IsColimit c
i : J.L
⊢ c.inj i ≫ I.sndSigmaMapOfIsColimit d hc = I.snd i ≫ d.inj (J.snd i)

Tactic:
simp [sndSigmaMapOfIsColimit]

Premises used: CategoryTheory.Limits.MultispanIndex.sndSigmaMapOfIsColimit
-- 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
inst_1 : HasCoproduct.{w, v, u} I.left
inst_2 : HasCoproduct.{w', v, u} I.right
b : J.L
⊢ Eq (α := I.left b ⟶ sigmaObj.{w', v, u} I.right)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} I.left) (Sigma.ι I.left b) I.fstSigmaMap)
    (I.fst b ≫ Sigma.ι I.right (J.fst b))

Tactic:
inj_fstSigmaMapOfIsColimit ..

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.Limits.MultispanIndex.fstSigmaMap, CategoryTheory.Limits.MultispanIndex.inj_fstSigmaMapOfIsColimit, CategoryTheory.Limits.colimit.ι
-- 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
inst_1 : HasCoproduct.{w, v, u} I.left
inst_2 : HasCoproduct.{w', v, u} I.right
b : J.L
⊢ Eq (α := I.left b ⟶ sigmaObj.{w', v, u} I.right)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} I.left) (Sigma.ι I.left b) I.sndSigmaMap)
    (I.snd b ≫ Sigma.ι I.right (J.snd b))

Tactic:
inj_sndSigmaMapOfIsColimit ..

Premises used: CategoryTheory.Limits.MultispanIndex.inj_sndSigmaMapOfIsColimit, CategoryTheory.Limits.colimit, CategoryTheory.Limits.MultispanIndex.sndSigmaMap, CategoryTheory.Limits.colimit.ι
-- 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
a : J.L
⊢ K.π.app (WalkingMulticospan.left a) = K.ι a

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
K : Multifork I
b : J.R
rw :
  K.π.app (WalkingMulticospan.left (J.fst b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst b) =
    K.ι (J.fst b) ≫ I.fst b
⊢ K.π.app (WalkingMulticospan.right b) = K.ι (J.fst b) ≫ I.fst b

Tactic:
rw [← K.w (WalkingMulticospan.Hom.fst b)]

Premises used: CategoryTheory.Limits.Cone.w, CategoryTheory.Limits.WalkingMulticospan.Hom.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
b : J.R
⊢ K.π.app (WalkingMulticospan.left (J.fst b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst b) =
    K.ι (J.fst b) ≫ I.fst b

Tactic:
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
b : J.R
rw :
  K.π.app (WalkingMulticospan.left (J.snd b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.snd b) =
    K.ι (J.snd b) ≫ I.snd b
⊢ K.π.app (WalkingMulticospan.right b) = K.ι (J.snd b) ≫ I.snd b

Tactic:
rw [← K.w (WalkingMulticospan.Hom.snd b)]

Premises used: CategoryTheory.Limits.Cone.w, CategoryTheory.Limits.WalkingMulticospan.Hom.snd
-- 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
b : J.R
⊢ K.π.app (WalkingMulticospan.left (J.snd b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.snd b) =
    K.ι (J.snd b) ≫ I.snd b

Tactic:
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₁ K₂ : Multifork I
f : K₁ ⟶ K₂
j : J.L
⊢ f.hom ≫ K₂.ι j = K₁.ι j

Tactic:
f.w _

Premises used: CategoryTheory.Limits.ConeMorphism.w, CategoryTheory.Limits.Multifork.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MulticospanShape
I_1 : MulticospanIndex.{w, w', v, u} J_1 C
K : Multifork I_1
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a : J.L
left : 𝟙 P ≫ ι a = ι a ≫ 𝟙 (I.left a)
⊢ Eq.{v + 1} (α :=
    Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) (WalkingMulticospan.left a) ⟶
      I.multicospan.obj (WalkingMulticospan.left a))
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) (WalkingMulticospan.left a))
      (Functor.map (Functor.obj (Functor.const (WalkingMulticospan J)) P)
        (WalkingMulticospan.Hom.id (WalkingMulticospan.left a)))
      (match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.left a with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b))
    ((match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.left a with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
      I.multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MulticospanShape
I_1 : MulticospanIndex.{w, w', v, u} J_1 C
K : Multifork I_1
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a : J.R
left : 𝟙 P ≫ ι (J.fst a) ≫ I.fst a = ι (J.fst a) ≫ I.fst a
⊢ Eq.{v + 1} (α :=
    Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) (WalkingMulticospan.left (J.fst a)) ⟶
      I.multicospan.obj (WalkingMulticospan.right a))
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) (WalkingMulticospan.right a))
      (Functor.map (Functor.obj (Functor.const (WalkingMulticospan J)) P) (WalkingMulticospan.Hom.fst a))
      (match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.right a with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b))
    ((match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.left (J.fst a) with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
      I.multicospan.map (WalkingMulticospan.Hom.fst a))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MulticospanShape
I_1 : MulticospanIndex.{w, w', v, u} J_1 C
K : Multifork I_1
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a : J.R
left : 𝟙 P ≫ ι (J.fst a) ≫ I.fst a = ι (J.snd a) ≫ I.snd a
⊢ Eq.{v + 1} (α :=
    Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) (WalkingMulticospan.left (J.snd a)) ⟶
      I.multicospan.obj (WalkingMulticospan.right a))
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) (WalkingMulticospan.right a))
      (Functor.map (Functor.obj (Functor.const (WalkingMulticospan J)) P) (WalkingMulticospan.Hom.snd a))
      (match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.right a with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b))
    ((match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.left (J.snd a) with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
      I.multicospan.map (WalkingMulticospan.Hom.snd a))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MulticospanShape
I_1 : MulticospanIndex.{w, w', v, u} J_1 C
K : Multifork I_1
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a : J.R
right : 𝟙 P ≫ ι (J.fst a) ≫ I.fst a = (ι (J.fst a) ≫ I.fst a) ≫ 𝟙 (I.right a)
⊢ Eq.{v + 1} (α :=
    Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) (WalkingMulticospan.right a) ⟶
      I.multicospan.obj (WalkingMulticospan.right a))
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) (WalkingMulticospan.right a))
      (Functor.map (Functor.obj (Functor.const (WalkingMulticospan J)) P)
        (WalkingMulticospan.Hom.id (WalkingMulticospan.right a)))
      (match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.right a with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b))
    ((match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.right a with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
      I.multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.right a)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MulticospanShape
I_1 : MulticospanIndex.{w, w', v, u} J_1 C
K : Multifork I_1
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a : J.L
⊢ 𝟙 P ≫ ι a = ι a ≫ 𝟙 (I.left a)

Tactic:
simp only [Category.id_comp, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MulticospanShape
I_1 : MulticospanIndex.{w, w', v, u} J_1 C
K : Multifork I_1
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a : J.R
⊢ 𝟙 P ≫ ι (J.fst a) ≫ I.fst a = ι (J.fst a) ≫ I.fst a

Tactic:
simp only [Category.id_comp, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MulticospanShape
I_1 : MulticospanIndex.{w, w', v, u} J_1 C
K : Multifork I_1
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a : J.R
left : ι (J.fst a) ≫ I.fst a = ι (J.snd a) ≫ I.snd a
⊢ 𝟙 P ≫ ι (J.fst a) ≫ I.fst a = ι (J.snd a) ≫ I.snd a

Tactic:
simp only [Category.id_comp, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MulticospanShape
I_1 : MulticospanIndex.{w, w', v, u} J_1 C
K : Multifork I_1
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a : J.R
⊢ 𝟙 P ≫ ι (J.fst a) ≫ I.fst a = (ι (J.fst a) ≫ I.fst a) ≫ 𝟙 (I.right a)

Tactic:
simp only [Category.id_comp, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MulticospanShape
I_1 : MulticospanIndex.{w, w', v, u} J_1 C
K : Multifork I_1
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a : J.R
⊢ ι (J.fst a) ≫ I.fst a = ι (J.snd a) ≫ I.snd a

Tactic:
apply w
-- 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
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
i : J.L
⊢ (ofι I P ι w).ι i = ι 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
K : Multifork I
b : J.R
rw : K.π.app (WalkingMulticospan.right b) = K.ι (J.snd b) ≫ I.snd b
rw₁ rw₂ :
  Eq (α := K.pt ⟶ I.right b)
    (K.π.app (WalkingMulticospan.right b) :
      Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) K.pt) (WalkingMulticospan.right b) ⟶
        I.multicospan.obj (WalkingMulticospan.right b))
    (K.π.app (WalkingMulticospan.right b))
⊢ K.ι (J.fst b) ≫ I.fst b = K.ι (J.snd b) ≫ I.snd b

Tactic:
rw [← app_right_eq_ι_comp_fst, ← app_right_eq_ι_comp_snd]

Premises used: CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_snd, 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 t s : Multifork I
e : t.pt ≅ s.pt
h : ∀ (i : J.L), e.hom ≫ s.ι i = t.ι i
i : J.L
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) t.pt) (WalkingMulticospan.left i) ⟶
      I.multicospan.obj (WalkingMulticospan.left i))
    (t.π.app (WalkingMulticospan.left i)) (e.hom ≫ s.π.app (WalkingMulticospan.left i))

Tactic:
simp [← 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 t s : Multifork I
e : t.pt ≅ s.pt
h : ∀ (i : J.L), e.hom ≫ s.ι i = t.ι i
j : J.R
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) t.pt) (WalkingMulticospan.right j) ⟶
      I.multicospan.obj (WalkingMulticospan.right j))
    (t.π.app (WalkingMulticospan.right j)) (e.hom ≫ s.π.app (WalkingMulticospan.right j))

Tactic:
simp [← 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
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
a : J.L
⊢ Eq (α := E.pt ⟶ I.multicospan.obj (WalkingMulticospan.left a)) (lift E ≫ K.π.app (WalkingMulticospan.left a))
    (E.π.app (WalkingMulticospan.left a))

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
b : J.R
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)
⊢ Eq (α := E.pt ⟶ I.multicospan.obj (WalkingMulticospan.right b)) (lift E ≫ K.π.app (WalkingMulticospan.right b))
    (E.π.app (WalkingMulticospan.right b))

Tactic:
rw [← E.w (WalkingMulticospan.Hom.fst b), ← K.w (WalkingMulticospan.Hom.fst b), ←
          Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cone.w, CategoryTheory.Limits.WalkingMulticospan.Hom.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
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
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)))
⊢ (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:
congr 1