awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a b : J.R
h : ¬a = b
this : IsEmpty (right a ⟶ right b)
⊢ Subsingleton (right a ⟶ right b)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
l l' : J.L
⊢ Small.{t, max w w'} (left l ⟶ left l')

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
l : J.L
r' : J.R
T₁ : Type := { u : Unit // J.fst l = r' }
T₂ : Type := { u : Unit // J.snd l = r' }
x : T₁
val : Unit
h : J.fst l = r'
subst :
  let T₁ := { u : Unit // J.fst l = J.fst l };
  T₁ → (left l ⟶ right (J.fst l))
⊢ left l ⟶ right r'

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
l : J.L
val : Unit
T₁ : Type := { u : Unit // J.fst l = J.fst l }
T₂ : Type := { u : Unit // J.snd l = J.fst l }
x : T₁
⊢ left l ⟶ right (J.fst l)

Tactic:
exact Hom.fst l

Premises used: CategoryTheory.Limits.WalkingMultispan.Hom.fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
l : J.L
r' : J.R
T₁ : Type := { u : Unit // J.fst l = r' }
T₂ : Type := { u : Unit // J.snd l = r' }
x : T₂
val : Unit
h : J.snd l = r'
subst :
  let T₂ := { u : Unit // J.snd l = J.snd l };
  T₂ → (left l ⟶ right (J.snd l))
⊢ left l ⟶ right r'

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
l : J.L
val : Unit
T₁ : Type := { u : Unit // J.fst l = J.snd l }
T₂ : Type := { u : Unit // J.snd l = J.snd l }
x : T₂
⊢ left l ⟶ right (J.snd l)

Tactic:
exact Hom.snd l

Premises used: CategoryTheory.Limits.WalkingMultispan.Hom.snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
l : J.L
r' : J.R
T₁ : Type := { u : Unit // J.fst l = r' }
T₂ : Type := { u : Unit // J.snd l = r' }
f : T₁ ⊕ T₂ → (left l ⟶ right r') :=
  Sum.elim
    (fun (x : T₁) ↦
      match (motive := T₁ → (left l ⟶ right r')) x with
      | ⟨val, h⟩ =>
        Eq.ndrec (motive := fun (r' : J.R) ↦
          let T₁ := { u : Unit // J.fst l = r' };
          let T₂ := { u : Unit // J.snd l = r' };
          T₁ → (left l ⟶ right r'))
          (let T₁ := { u : Unit // J.fst l = J.fst l };
          let T₂ := { u : Unit // J.snd l = J.fst l };
          fun (x : T₁) ↦ Hom.fst l)
          h x)
    fun (x : T₂) ↦
    match (motive := T₂ → (left l ⟶ right r')) x with
    | ⟨val, h⟩ =>
      Eq.ndrec (motive := fun (r' : J.R) ↦
        let T₁ := { u : Unit // J.fst l = r' };
        let T₂ := { u : Unit // J.snd l = r' };
        T₂ → (left l ⟶ right r'))
        (let T₁ := { u : Unit // J.fst l = J.snd l };
        let T₂ := { u : Unit // J.snd l = J.snd l };
        fun (x : T₂) ↦ Hom.snd l)
        h x
⊢ Small.{t, max w w'} (left l ⟶ right r')

Tactic:
small_of_surjective (f := f) ?_

Premises used: small_of_surjective
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
l : J.L
r' : J.R
T₁ : Type := { u : Unit // J.fst l = r' }
T₂ : Type := { u : Unit // J.snd l = r' }
f : T₁ ⊕ T₂ → (WalkingMultispan.left l ⟶ right r') :=
  Sum.elim
    (fun (x : T₁) ↦
      match (motive := T₁ → (WalkingMultispan.left l ⟶ right r')) x with
      | ⟨val, h⟩ =>
        Eq.ndrec (motive := fun (r' : J.R) ↦
          let T₁ := { u : Unit // J.fst l = r' };
          let T₂ := { u : Unit // J.snd l = r' };
          T₁ → (WalkingMultispan.left l ⟶ right r'))
          (let T₁ := { u : Unit // J.fst l = J.fst l };
          let T₂ := { u : Unit // J.snd l = J.fst l };
          fun (x : T₁) ↦ Hom.fst l)
          h x)
    fun (x : T₂) ↦
    match (motive := T₂ → (WalkingMultispan.left l ⟶ right r')) x with
    | ⟨val, h⟩ =>
      Eq.ndrec (motive := fun (r' : J.R) ↦
        let T₁ := { u : Unit // J.fst l = r' };
        let T₂ := { u : Unit // J.snd l = r' };
        T₂ → (WalkingMultispan.left l ⟶ right r'))
        (let T₁ := { u : Unit // J.fst l = J.snd l };
        let T₂ := { u : Unit // J.snd l = J.snd l };
        fun (x : T₂) ↦ Hom.snd l)
        h x
left : Function.Surjective f
⊢ Small.{t, max w w'} (WalkingMultispan.left l ⟶ right r')

Tactic:
refine small_of_surjective (f := f) ?_

Premises used: small_of_surjective
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
l : J.L
T₁ : Type := { u : Unit // J.fst l = J.fst l }
T₂ : Type := { u : Unit // J.snd l = J.fst l }
f : T₁ ⊕ T₂ → (left l ⟶ right (J.fst l)) :=
  Sum.elim
    (fun (x : T₁) ↦
      match (motive := T₁ → (left l ⟶ right (J.fst l))) x with
      | ⟨val, h⟩ =>
        Eq.ndrec (motive := fun (r' : J.R) ↦
          let T₁ := { u : Unit // J.fst l = r' };
          let T₂ := { u : Unit // J.snd l = r' };
          T₁ → (left l ⟶ right r'))
          (let T₁ := { u : Unit // J.fst l = J.fst l };
          let T₂ := { u : Unit // J.snd l = J.fst l };
          fun (x : T₁) ↦ Hom.fst l)
          h x)
    fun (x : T₂) ↦
    match (motive := T₂ → (left l ⟶ right (J.fst l))) x with
    | ⟨val, h⟩ =>
      Eq.ndrec (motive := fun (r' : J.R) ↦
        let T₁ := { u : Unit // J.fst l = r' };
        let T₂ := { u : Unit // J.snd l = r' };
        T₂ → (left l ⟶ right r'))
        (let T₁ := { u : Unit // J.fst l = J.snd l };
        let T₂ := { u : Unit // J.snd l = J.snd l };
        fun (x : T₂) ↦ Hom.snd l)
        h x
⊢ ∃ (a : T₁ ⊕ T₂), f a = Hom.fst l

Tactic:
⟨Sum.inl ⟨⟨⟩, rfl⟩, rfl⟩

Premises used: Sum.inl, Subtype.mk, Exists.intro, PUnit.unit, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
l : J.L
T₁ : Type := { u : Unit // J.fst l = J.fst l }
T₂ : Type := { u : Unit // J.snd l = J.fst l }
f : T₁ ⊕ T₂ → (left l ⟶ right (J.fst l)) :=
  Sum.elim
    (fun (x : T₁) ↦
      match (motive := T₁ → (left l ⟶ right (J.fst l))) x with
      | ⟨val, h⟩ =>
        Eq.ndrec (motive := fun (r' : J.R) ↦
          let T₁ := { u : Unit // J.fst l = r' };
          let T₂ := { u : Unit // J.snd l = r' };
          T₁ → (left l ⟶ right r'))
          (let T₁ := { u : Unit // J.fst l = J.fst l };
          let T₂ := { u : Unit // J.snd l = J.fst l };
          fun (x : T₁) ↦ Hom.fst l)
          h x)
    fun (x : T₂) ↦
    match (motive := T₂ → (left l ⟶ right (J.fst l))) x with
    | ⟨val, h⟩ =>
      Eq.ndrec (motive := fun (r' : J.R) ↦
        let T₁ := { u : Unit // J.fst l = r' };
        let T₂ := { u : Unit // J.snd l = r' };
        T₂ → (left l ⟶ right r'))
        (let T₁ := { u : Unit // J.fst l = J.snd l };
        let T₂ := { u : Unit // J.snd l = J.snd l };
        fun (x : T₂) ↦ Hom.snd l)
        h x
⊢ ∃ (a : T₁ ⊕ T₂), f a = Hom.fst l

Tactic:
exact ⟨Sum.inl ⟨⟨⟩, rfl⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
l : J.L
T₁ : Type := { u : Unit // J.fst l = J.snd l }
T₂ : Type := { u : Unit // J.snd l = J.snd l }
f : T₁ ⊕ T₂ → (left l ⟶ right (J.snd l)) :=
  Sum.elim
    (fun (x : T₁) ↦
      match (motive := T₁ → (left l ⟶ right (J.snd l))) x with
      | ⟨val, h⟩ =>
        Eq.ndrec (motive := fun (r' : J.R) ↦
          let T₁ := { u : Unit // J.fst l = r' };
          let T₂ := { u : Unit // J.snd l = r' };
          T₁ → (left l ⟶ right r'))
          (let T₁ := { u : Unit // J.fst l = J.fst l };
          let T₂ := { u : Unit // J.snd l = J.fst l };
          fun (x : T₁) ↦ Hom.fst l)
          h x)
    fun (x : T₂) ↦
    match (motive := T₂ → (left l ⟶ right (J.snd l))) x with
    | ⟨val, h⟩ =>
      Eq.ndrec (motive := fun (r' : J.R) ↦
        let T₁ := { u : Unit // J.fst l = r' };
        let T₂ := { u : Unit // J.snd l = r' };
        T₂ → (left l ⟶ right r'))
        (let T₁ := { u : Unit // J.fst l = J.snd l };
        let T₂ := { u : Unit // J.snd l = J.snd l };
        fun (x : T₂) ↦ Hom.snd l)
        h x
⊢ ∃ (a : T₁ ⊕ T₂), f a = Hom.snd l

Tactic:
⟨Sum.inr ⟨⟨⟩, rfl⟩, rfl⟩

Premises used: Subtype.mk, Sum.inr, Exists.intro, PUnit.unit, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
l : J.L
T₁ : Type := { u : Unit // J.fst l = J.snd l }
T₂ : Type := { u : Unit // J.snd l = J.snd l }
f : T₁ ⊕ T₂ → (left l ⟶ right (J.snd l)) :=
  Sum.elim
    (fun (x : T₁) ↦
      match (motive := T₁ → (left l ⟶ right (J.snd l))) x with
      | ⟨val, h⟩ =>
        Eq.ndrec (motive := fun (r' : J.R) ↦
          let T₁ := { u : Unit // J.fst l = r' };
          let T₂ := { u : Unit // J.snd l = r' };
          T₁ → (left l ⟶ right r'))
          (let T₁ := { u : Unit // J.fst l = J.fst l };
          let T₂ := { u : Unit // J.snd l = J.fst l };
          fun (x : T₁) ↦ Hom.fst l)
          h x)
    fun (x : T₂) ↦
    match (motive := T₂ → (left l ⟶ right (J.snd l))) x with
    | ⟨val, h⟩ =>
      Eq.ndrec (motive := fun (r' : J.R) ↦
        let T₁ := { u : Unit // J.fst l = r' };
        let T₂ := { u : Unit // J.snd l = r' };
        T₂ → (left l ⟶ right r'))
        (let T₁ := { u : Unit // J.fst l = J.snd l };
        let T₂ := { u : Unit // J.snd l = J.snd l };
        fun (x : T₂) ↦ Hom.snd l)
        h x
⊢ ∃ (a : T₁ ⊕ T₂), f a = Hom.snd l

Tactic:
exact ⟨Sum.inr ⟨⟨⟩, rfl⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
r : J.R
l' : J.L
⊢ Small.{t, max w w'} (right r ⟶ left l')

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
r r' : J.R
⊢ Small.{t, max w w'} (right r ⟶ right r')

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : J.L
⊢ Sum.elim left right
      ((fun (x : WalkingMultispan J) ↦
          (match (motive := WalkingMultispan J → Sum.{w, w'} J.L J.R) x with
            | left a => Sum.inl a
            | right b => Sum.inr b :
            Sum.{w, w'} J.L J.R))
        (left a)) =
    left a

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : J.R
⊢ Sum.elim left right
      ((fun (x : WalkingMultispan J) ↦
          (match (motive := WalkingMultispan J → Sum.{w, w'} J.L J.R) x with
            | left a => Sum.inl a
            | right b => Sum.inr b :
            Sum.{w, w'} J.L J.R))
        (right a)) =
    right a

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
val : J.L
⊢ Eq (α := Sum.{w, w'} J.L J.R)
    ((fun (x : WalkingMultispan J) ↦
        (match (motive := WalkingMultispan J → Sum.{w, w'} J.L J.R) x with
          | left a => Sum.inl a
          | right b => Sum.inr b :
          Sum.{w, w'} J.L J.R))
      (Sum.elim left right (Sum.inl val)))
    (Sum.inl val)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
val : J.R
⊢ Eq (α := Sum.{w, w'} J.L J.R)
    ((fun (x : WalkingMultispan J) ↦
        (match (motive := WalkingMultispan J → Sum.{w, w'} J.L J.R) x with
          | left a => Sum.inl a
          | right b => Sum.inr b :
          Sum.{w, w'} J.L J.R))
      (Sum.elim left right (Sum.inr val)))
    (Sum.inr val)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
left : WalkingMultispan J
⊢ Eq (α := Arrow (WalkingMultispan J))
    (Sum.elim (β := J.L ⊕ J.L) (fun (X : WalkingMultispan J) ↦ Arrow.mk (𝟙 X))
      (Sum.elim (fun (a : J.L) ↦ Arrow.mk (Hom.fst a)) fun (a : J.L) ↦ Arrow.mk (Hom.snd a))
      ((fun (f : Arrow (WalkingMultispan J)) ↦
          (match (motive := (x x_1 : WalkingMultispan J) → (x_1 ⟶ x) → WalkingMultispan J ⊕ J.L ⊕ J.L) f.right, f.left,
              f.hom with
            | x, .(x), Hom.id .(x) => Sum.inl x
            | .(right (J.fst a)), .(WalkingMultispan.left a), Hom.fst a => Sum.inr (Sum.inl a)
            | .(right (J.snd a)), .(WalkingMultispan.left a), Hom.snd a => Sum.inr (Sum.inr a) :
            WalkingMultispan J ⊕ J.L ⊕ J.L))
        { left := left, right := left, hom := Hom.id (Functor.obj (𝟭 (WalkingMultispan J)) left) }))
    { left := left, right := left, hom := Hom.id (Functor.obj (𝟭 (WalkingMultispan J)) left) }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : J.L
⊢ Eq (α := Arrow (WalkingMultispan J))
    (Sum.elim (β := J.L ⊕ J.L) (fun (X : WalkingMultispan J) ↦ Arrow.mk (𝟙 X))
      (Sum.elim (fun (a : J.L) ↦ Arrow.mk (Hom.fst a)) fun (a : J.L) ↦ Arrow.mk (Hom.snd a))
      ((fun (f : Arrow (WalkingMultispan J)) ↦
          (match (motive := (x x_1 : WalkingMultispan J) → (x_1 ⟶ x) → WalkingMultispan J ⊕ J.L ⊕ J.L) f.right, f.left,
              f.hom with
            | x, .(x), Hom.id .(x) => Sum.inl x
            | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
            | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a) :
            WalkingMultispan J ⊕ J.L ⊕ J.L))
        { left := left a, right := right (J.fst a), hom := Hom.fst a }))
    { left := left a, right := right (J.fst a), hom := Hom.fst a }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : J.L
⊢ Eq (α := Arrow (WalkingMultispan J))
    (Sum.elim (β := J.L ⊕ J.L) (fun (X : WalkingMultispan J) ↦ Arrow.mk (𝟙 X))
      (Sum.elim (fun (a : J.L) ↦ Arrow.mk (Hom.fst a)) fun (a : J.L) ↦ Arrow.mk (Hom.snd a))
      ((fun (f : Arrow (WalkingMultispan J)) ↦
          (match (motive := (x x_1 : WalkingMultispan J) → (x_1 ⟶ x) → WalkingMultispan J ⊕ J.L ⊕ J.L) f.right, f.left,
              f.hom with
            | x, .(x), Hom.id .(x) => Sum.inl x
            | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
            | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a) :
            WalkingMultispan J ⊕ J.L ⊕ J.L))
        { left := left a, right := right (J.snd a), hom := Hom.snd a }))
    { left := left a, right := right (J.snd a), hom := Hom.snd a }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
val : WalkingMultispan J
⊢ Eq (α := WalkingMultispan J ⊕ J.L ⊕ J.L)
    ((fun (f : Arrow (WalkingMultispan J)) ↦
        (match (motive := (x x_1 : WalkingMultispan J) → (x_1 ⟶ x) → WalkingMultispan J ⊕ J.L ⊕ J.L) f.right, f.left,
            f.hom with
          | x, .(x), Hom.id .(x) => Sum.inl x
          | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
          | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a) :
          WalkingMultispan J ⊕ J.L ⊕ J.L))
      (Sum.elim (β := J.L ⊕ J.L) (fun (X : WalkingMultispan J) ↦ Arrow.mk (𝟙 X))
        (Sum.elim (fun (a : J.L) ↦ Arrow.mk (Hom.fst a)) fun (a : J.L) ↦ Arrow.mk (Hom.snd a)) (Sum.inl val)))
    (Sum.inl val)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
val : J.L
⊢ Eq (α := WalkingMultispan J ⊕ J.L ⊕ J.L)
    ((fun (f : Arrow (WalkingMultispan J)) ↦
        (match (motive := (x x_1 : WalkingMultispan J) → (x_1 ⟶ x) → WalkingMultispan J ⊕ J.L ⊕ J.L) f.right, f.left,
            f.hom with
          | x, .(x), Hom.id .(x) => Sum.inl x
          | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
          | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a) :
          WalkingMultispan J ⊕ J.L ⊕ J.L))
      (Sum.elim (β := J.L ⊕ J.L) (fun (X : WalkingMultispan J) ↦ Arrow.mk (𝟙 X))
        (Sum.elim (fun (a : J.L) ↦ Arrow.mk (Hom.fst a)) fun (a : J.L) ↦ Arrow.mk (Hom.snd a)) (Sum.inr (Sum.inl val))))
    (Sum.inr (Sum.inl val))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
val : J.L
⊢ Eq (α := WalkingMultispan J ⊕ J.L ⊕ J.L)
    ((fun (f : Arrow (WalkingMultispan J)) ↦
        (match (motive := (x x_1 : WalkingMultispan J) → (x_1 ⟶ x) → WalkingMultispan J ⊕ J.L ⊕ J.L) f.right, f.left,
            f.hom with
          | x, .(x), Hom.id .(x) => Sum.inl x
          | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
          | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a) :
          WalkingMultispan J ⊕ J.L ⊕ J.L))
      (Sum.elim (β := J.L ⊕ J.L) (fun (X : WalkingMultispan J) ↦ Arrow.mk (𝟙 X))
        (Sum.elim (fun (a : J.L) ↦ Arrow.mk (Hom.fst a)) fun (a : J.L) ↦ Arrow.mk (Hom.snd a)) (Sum.inr (Sum.inr val))))
    (Sum.inr (Sum.inr val))

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

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

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

Tactic:
simp [fstPiMapOfIsLimit]

Premises used: CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimit
-- 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
i : J.R
⊢ I.sndPiMapOfIsLimit c hd ≫ d.proj i = c.proj (J.snd i) ≫ I.snd i

Tactic:
simp [sndPiMapOfIsLimit]

Premises used: CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit
-- 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 : HasProduct.{w, v, u} I.left
inst_2 : HasProduct.{w', v, u} I.right
b : J.R
⊢ Eq (α := piObj.{w, v, u} I.left ⟶ I.right b)
    (CategoryStruct.comp (Y := piObj.{w', v, u} I.right) I.fstPiMap (Pi.π I.right b)) (Pi.π I.left (J.fst b) ≫ I.fst b)

Tactic:
fstPiMapOfIsLimit_proj ..

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimit_proj, CategoryTheory.Limits.limit, CategoryTheory.Limits.MulticospanIndex.fstPiMap
-- 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 : HasProduct.{w, v, u} I.left
inst_2 : HasProduct.{w', v, u} I.right
b : J.R
⊢ Eq (α := piObj.{w, v, u} I.left ⟶ I.right b)
    (CategoryStruct.comp (Y := piObj.{w', v, u} I.right) I.sndPiMap (Pi.π I.right b)) (Pi.π I.left (J.snd b) ≫ I.snd b)

Tactic:
sndPiMapOfIsLimit_proj ..

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit_proj, CategoryTheory.Limits.limit, CategoryTheory.Limits.MulticospanIndex.sndPiMap