awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst_1 : (X Y : C) → FunLike.{u_1 + 1, s + 1, s + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{s, v, u, u_1} C FC (CC := CC)
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
x : (↑(I.multicospan ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max (max s w) w'))
i : J.R
a :
  (hom (FC := TypeCat.Fun) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map (WalkingMulticospan.Hom.fst i)) :
        (a : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left (J.fst i)))) →
          (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right i)))
      ((↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left (J.fst i))) =
    (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.right i)
b :
  (hom (FC := TypeCat.Fun) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map (WalkingMulticospan.Hom.snd i)) :
        (a : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left (J.snd i)))) →
          (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right i)))
      ((↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left (J.snd i))) =
    (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.right i)
⊢ Eq (α := (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right i)))
    ((hom (FC := TypeCat.Fun) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map (WalkingMulticospan.Hom.fst i)) :
          (a : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left (J.fst i)))) →
            (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right i)))
        ((↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left (J.fst i))) :
      (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right i)))
    ((hom (FC := TypeCat.Fun) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map (WalkingMulticospan.Hom.snd i)) :
          (a : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left (J.snd i)))) →
            (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right i)))
        ((↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left (J.snd i))) :
      (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right i)))

Tactic:
rw [← b] at a
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst_1 : (X Y : C) → FunLike.{u_1 + 1, s + 1, s + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{s, v, u, u_1} C FC (CC := CC)
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
x : (↑(I.multicospan ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max (max s w) w'))
i : J.R
a :
  Eq (α := (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right i)))
    ((hom (FC := TypeCat.Fun) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map (WalkingMulticospan.Hom.fst i)) :
          (a : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left (J.fst i)))) →
            (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right i)))
        ((↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left (J.fst i))) :
      (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right i)))
    ((hom (FC := TypeCat.Fun) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map (WalkingMulticospan.Hom.snd i)) :
          (a : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left (J.snd i)))) →
            (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right i)))
        ((↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left (J.snd i))) :
      (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right i)))
b :
  (hom (FC := TypeCat.Fun) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map (WalkingMulticospan.Hom.snd i)) :
        (a : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left (J.snd i)))) →
          (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right i)))
      ((↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left (J.snd i))) =
    (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.right i)
⊢ Eq.{s + 1} (α := CC (I.right i))
    ((hom (FC := FC) (CC := CC) (I.fst i) : (a : CC (I.left (J.fst i))) → CC (I.right i))
        ((fun (x_1 : J.L) ↦
            (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left x_1))
          (J.fst i)) :
      CC (I.right i))
    ((hom (FC := FC) (CC := CC) (I.snd i) : (a : CC (I.left (J.snd i))) → CC (I.right i))
        ((fun (x_1 : J.L) ↦
            (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left x_1))
          (J.snd i)) :
      CC (I.right i))

Tactic:
a
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst_1 : (X Y : C) → FunLike.{u_1 + 1, s + 1, s + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{s, v, u, u_1} C FC (CC := CC)
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
x : (↑(I.multicospan ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max (max s w) w'))
i : J.R
a :
  Eq (α := (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right i)))
    ((hom (FC := TypeCat.Fun) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map (WalkingMulticospan.Hom.fst i)) :
          (a : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left (J.fst i)))) →
            (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right i)))
        ((↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left (J.fst i))) :
      (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right i)))
    ((hom (FC := TypeCat.Fun) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map (WalkingMulticospan.Hom.snd i)) :
          (a : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left (J.snd i)))) →
            (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right i)))
        ((↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left (J.snd i))) :
      (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right i)))
b :
  (hom (FC := TypeCat.Fun) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map (WalkingMulticospan.Hom.snd i)) :
        (a : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left (J.snd i)))) →
          (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right i)))
      ((↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left (J.snd i))) =
    (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.right i)
⊢ Eq.{s + 1} (α := CC (I.right i))
    ((hom (FC := FC) (CC := CC) (I.fst i) : (a : CC (I.left (J.fst i))) → CC (I.right i))
        ((fun (x_1 : J.L) ↦
            (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left x_1))
          (J.fst i)) :
      CC (I.right i))
    ((hom (FC := FC) (CC := CC) (I.snd i) : (a : CC (I.left (J.snd i))) → CC (I.right i))
        ((fun (x_1 : J.L) ↦
            (↑x : (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C).obj j) (WalkingMulticospan.left x_1))
          (J.snd i)) :
      CC (I.right i))

Tactic:
exact a
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst_1 : (X Y : C) → FunLike.{u_1 + 1, s + 1, s + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{s, v, u, u_1} C FC (CC := CC)
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
x :
  { x : (i : J.L) → ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (I.left i) //
    ∀ (i : J.R),
      Eq.{s + 1} (α := CC (I.right i))
        ((hom (FC := FC) (CC := CC) (I.fst i) : (a : CC (I.left (J.fst i))) → CC (I.right i)) (x (J.fst i)) :
          CC (I.right i))
        ((hom (FC := FC) (CC := CC) (I.snd i) : (a : CC (I.left (J.snd i))) → CC (I.right i)) (x (J.snd i)) :
          CC (I.right i)) }
a : J.L
⊢ Eq (α := (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.left a)))
    ((hom (FC := TypeCat.Fun)
            ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map
              (WalkingMulticospan.Hom.id (WalkingMulticospan.left a))) :
          (a_1 : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left a))) →
            (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left a)))
        ((fun (j : WalkingMulticospan J) ↦
            (match (motive := (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j)
                j with
              | WalkingMulticospan.left a => (↑x : (i : J.L) → ToType (I.left i)) a
              | WalkingMulticospan.right b =>
                (hom (FC := FC) (CC := CC) (I.fst b) : (a : CC (I.left (J.fst b))) → CC (I.right b))
                  ((↑x : (i : J.L) → ToType (I.left i)) (J.fst b)) :
              (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j))
          (WalkingMulticospan.left a)) :
      (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.left a)))
    ((fun (j : WalkingMulticospan J) ↦
          (match (motive := (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j) j with
            | WalkingMulticospan.left a => (↑x : (i : J.L) → ToType (I.left i)) a
            | WalkingMulticospan.right b =>
              (hom (FC := FC) (CC := CC) (I.fst b) : (a : CC (I.left (J.fst b))) → CC (I.right b))
                ((↑x : (i : J.L) → ToType (I.left i)) (J.fst b)) :
            (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j))
        (WalkingMulticospan.left a) :
      (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.left a))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst_1 : (X Y : C) → FunLike.{u_1 + 1, s + 1, s + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{s, v, u, u_1} C FC (CC := CC)
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
x :
  { x : (i : J.L) → ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (I.left i) //
    ∀ (i : J.R),
      Eq.{s + 1} (α := CC (I.right i))
        ((hom (FC := FC) (CC := CC) (I.fst i) : (a : CC (I.left (J.fst i))) → CC (I.right i)) (x (J.fst i)) :
          CC (I.right i))
        ((hom (FC := FC) (CC := CC) (I.snd i) : (a : CC (I.left (J.snd i))) → CC (I.right i)) (x (J.snd i)) :
          CC (I.right i)) }
b' : J.R
⊢ Eq (α := (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right b')))
    ((hom (FC := TypeCat.Fun) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map (WalkingMulticospan.Hom.fst b')) :
          (a : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left (J.fst b')))) →
            (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right b')))
        ((fun (j : WalkingMulticospan J) ↦
            (match (motive := (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j)
                j with
              | WalkingMulticospan.left a => (↑x : (i : J.L) → ToType (I.left i)) a
              | WalkingMulticospan.right b =>
                (hom (FC := FC) (CC := CC) (I.fst b) : (a : CC (I.left (J.fst b))) → CC (I.right b))
                  ((↑x : (i : J.L) → ToType (I.left i)) (J.fst b)) :
              (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j))
          (WalkingMulticospan.left (J.fst b'))) :
      (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right b')))
    ((fun (j : WalkingMulticospan J) ↦
          (match (motive := (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j) j with
            | WalkingMulticospan.left a => (↑x : (i : J.L) → ToType (I.left i)) a
            | WalkingMulticospan.right b =>
              (hom (FC := FC) (CC := CC) (I.fst b) : (a : CC (I.left (J.fst b))) → CC (I.right b))
                ((↑x : (i : J.L) → ToType (I.left i)) (J.fst b)) :
            (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j))
        (WalkingMulticospan.right b') :
      (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right b'))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst_1 : (X Y : C) → FunLike.{u_1 + 1, s + 1, s + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{s, v, u, u_1} C FC (CC := CC)
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
x :
  { x : (i : J.L) → ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (I.left i) //
    ∀ (i : J.R),
      Eq.{s + 1} (α := CC (I.right i))
        ((hom (FC := FC) (CC := CC) (I.fst i) : (a : CC (I.left (J.fst i))) → CC (I.right i)) (x (J.fst i)) :
          CC (I.right i))
        ((hom (FC := FC) (CC := CC) (I.snd i) : (a : CC (I.left (J.snd i))) → CC (I.right i)) (x (J.snd i)) :
          CC (I.right i)) }
b' : J.R
left :
  Eq (α := ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (I.right b'))
    ((hom (FC := FC) (CC := CC) (I.snd b') : (a : CC (I.left (J.snd b'))) → CC (I.right b'))
        ((↑x : (i : J.L) → ToType (I.left i)) (J.snd b')) :
      CC (I.right b'))
    ((hom (FC := FC) (CC := CC) (I.fst b') : (a : CC (I.left (J.fst b'))) → CC (I.right b'))
        ((↑x : (i : J.L) → ToType (I.left i)) (J.fst b')) :
      CC (I.right b'))
⊢ Eq (α := (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right b')))
    ((hom (FC := TypeCat.Fun) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map (WalkingMulticospan.Hom.snd b')) :
          (a : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left (J.snd b')))) →
            (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right b')))
        ((fun (j : WalkingMulticospan J) ↦
            (match (motive := (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j)
                j with
              | WalkingMulticospan.left a => (↑x : (i : J.L) → ToType (I.left i)) a
              | WalkingMulticospan.right b =>
                (hom (FC := FC) (CC := CC) (I.fst b) : (a : CC (I.left (J.fst b))) → CC (I.right b))
                  ((↑x : (i : J.L) → ToType (I.left i)) (J.fst b)) :
              (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j))
          (WalkingMulticospan.left (J.snd b'))) :
      (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right b')))
    ((fun (j : WalkingMulticospan J) ↦
          (match (motive := (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j) j with
            | WalkingMulticospan.left a => (↑x : (i : J.L) → ToType (I.left i)) a
            | WalkingMulticospan.right b =>
              (hom (FC := FC) (CC := CC) (I.fst b) : (a : CC (I.left (J.fst b))) → CC (I.right b))
                ((↑x : (i : J.L) → ToType (I.left i)) (J.fst b)) :
            (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j))
        (WalkingMulticospan.right b') :
      (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right b'))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst_1 : (X Y : C) → FunLike.{u_1 + 1, s + 1, s + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{s, v, u, u_1} C FC (CC := CC)
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
x :
  { x : (i : J.L) → ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (I.left i) //
    ∀ (i : J.R),
      Eq.{s + 1} (α := CC (I.right i))
        ((hom (FC := FC) (CC := CC) (I.fst i) : (a : CC (I.left (J.fst i))) → CC (I.right i)) (x (J.fst i)) :
          CC (I.right i))
        ((hom (FC := FC) (CC := CC) (I.snd i) : (a : CC (I.left (J.snd i))) → CC (I.right i)) (x (J.snd i)) :
          CC (I.right i)) }
b' : J.R
⊢ Eq (α := ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (I.right b'))
    ((hom (FC := FC) (CC := CC) (I.snd b') : (a : CC (I.left (J.snd b'))) → CC (I.right b'))
        ((↑x : (i : J.L) → ToType (I.left i)) (J.snd b')) :
      CC (I.right b'))
    ((hom (FC := FC) (CC := CC) (I.fst b') : (a : CC (I.left (J.fst b'))) → CC (I.right b'))
        ((↑x : (i : J.L) → ToType (I.left i)) (J.fst b')) :
      CC (I.right b'))

Tactic:
(x.2 b').symm

Premises used: Eq.symm, Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst_1 : (X Y : C) → FunLike.{u_1 + 1, s + 1, s + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{s, v, u, u_1} C FC (CC := CC)
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
x :
  { x : (i : J.L) → ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (I.left i) //
    ∀ (i : J.R),
      Eq.{s + 1} (α := CC (I.right i))
        ((hom (FC := FC) (CC := CC) (I.fst i) : (a : CC (I.left (J.fst i))) → CC (I.right i)) (x (J.fst i)) :
          CC (I.right i))
        ((hom (FC := FC) (CC := CC) (I.snd i) : (a : CC (I.left (J.snd i))) → CC (I.right i)) (x (J.snd i)) :
          CC (I.right i)) }
b' : J.R
⊢ Eq (α := ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (I.right b'))
    ((hom (FC := FC) (CC := CC) (I.snd b') : (a : CC (I.left (J.snd b'))) → CC (I.right b'))
        ((↑x : (i : J.L) → ToType (I.left i)) (J.snd b')) :
      CC (I.right b'))
    ((hom (FC := FC) (CC := CC) (I.fst b') : (a : CC (I.left (J.fst b'))) → CC (I.right b'))
        ((↑x : (i : J.L) → ToType (I.left i)) (J.fst b')) :
      CC (I.right b'))

Tactic:
exact (x.2 b').symm

Premises used: Eq.symm, Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst_1 : (X Y : C) → FunLike.{u_1 + 1, s + 1, s + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{s, v, u, u_1} C FC (CC := CC)
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
x :
  { x : (i : J.L) → ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (I.left i) //
    ∀ (i : J.R),
      Eq.{s + 1} (α := CC (I.right i))
        ((hom (FC := FC) (CC := CC) (I.fst i) : (a : CC (I.left (J.fst i))) → CC (I.right i)) (x (J.fst i)) :
          CC (I.right i))
        ((hom (FC := FC) (CC := CC) (I.snd i) : (a : CC (I.left (J.snd i))) → CC (I.right i)) (x (J.snd i)) :
          CC (I.right i)) }
b : J.R
⊢ Eq (α := (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right b)))
    ((hom (FC := TypeCat.Fun)
            ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map
              (WalkingMulticospan.Hom.id (WalkingMulticospan.right b))) :
          (a : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right b))) →
            (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right b)))
        ((fun (j : WalkingMulticospan J) ↦
            (match (motive := (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j)
                j with
              | WalkingMulticospan.left a => (↑x : (i : J.L) → ToType (I.left i)) a
              | WalkingMulticospan.right b =>
                (hom (FC := FC) (CC := CC) (I.fst b) : (a : CC (I.left (J.fst b))) → CC (I.right b))
                  ((↑x : (i : J.L) → ToType (I.left i)) (J.fst b)) :
              (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j))
          (WalkingMulticospan.right b)) :
      (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right b)))
    ((fun (j : WalkingMulticospan J) ↦
          (match (motive := (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j) j with
            | WalkingMulticospan.left a => (↑x : (i : J.L) → ToType (I.left i)) a
            | WalkingMulticospan.right b =>
              (hom (FC := FC) (CC := CC) (I.fst b) : (a : CC (I.left (J.fst b))) → CC (I.right b))
                ((↑x : (i : J.L) → ToType (I.left i)) (J.fst b)) :
            (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j))
        (WalkingMulticospan.right b) :
      (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right b))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst_1 : (X Y : C) → FunLike.{u_1 + 1, s + 1, s + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{s, v, u, u_1} C FC (CC := CC)
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
inst_3 : HasMultiequalizer I
inst_4 : PreservesLimit I.multicospan (forget C (FC := FC) (CC := CC))
x : ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (multiequalizer I)
i : J.L
⊢ Eq.{s + 1} (α := ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (I.left i))
    ((↑((multiequalizerEquiv (FC := FC) (CC := CC) I :
                (a : ToType (multiequalizer I)) →
                  { x : (i : J.L) → ToType (I.left i) //
                    ∀ (i : J.R),
                      (hom (I.fst i) : (a : CC (I.left (J.fst i))) → CC (I.right i)) (x (J.fst i)) =
                        (hom (I.snd i) : (a : CC (I.left (J.snd i))) → CC (I.right i)) (x (J.snd i)) })
              x) :
          (i : J.L) → ToType (I.left i))
        i :
      ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (I.left i))
    ((hom (FC := FC) (CC := CC) (Multiequalizer.ι I i) : (a : CC (multiequalizer I)) → CC (I.left i)) x : CC (I.left i))

Tactic:
rfl

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