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 v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
inst_3 : HasPullback f₁ f₂
inst_4 : PreservesLimit (cospan f₁ f₂) (forget C (FC := FC) (CC := CC))
x₁ : ToType (FC := FC) (CC := CC) X₁
x₂ : ToType (FC := FC) (CC := CC) X₂
h :
  Eq (α := CC S) ((hom (FC := FC) (CC := CC) f₁ : (a : CC X₁) → CC S) x₁ : CC S)
    ((hom (FC := FC) (CC := CC) f₂ : (a : CC X₂) → CC S) x₂ : CC S)
⊢ (hom (FC := FC) (CC := CC) (pullback.fst f₁ f₂) : (a : CC (pullback f₁ f₂)) → CC X₁)
      (pullbackMk (FC := FC) (CC := CC) f₁ f₂ x₁ x₂ h) =
    x₁

Tactic:
(congr_hom (PreservesPullback.iso_inv_fst (forget C) f₁ f₂) _).trans
    (congr_hom (Types.pullbackIsoPullback_inv_fst (↾f₁) (↾f₂)) _)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.PreservesPullback.iso_inv_fst, TypeCat.ofHom, CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst, CategoryTheory.Limits.Concrete.pullbackMk, CategoryTheory.forget, CategoryTheory.ConcreteCategory.congr_hom, DFunLike.coe, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
inst_3 : HasPullback f₁ f₂
inst_4 : PreservesLimit (cospan f₁ f₂) (forget C (FC := FC) (CC := CC))
x₁ : ToType (FC := FC) (CC := CC) X₁
x₂ : ToType (FC := FC) (CC := CC) X₂
h :
  Eq (α := CC S) ((hom (FC := FC) (CC := CC) f₁ : (a : CC X₁) → CC S) x₁ : CC S)
    ((hom (FC := FC) (CC := CC) f₂ : (a : CC X₂) → CC S) x₂ : CC S)
⊢ (hom (FC := FC) (CC := CC) (pullback.snd f₁ f₂) : (a : CC (pullback f₁ f₂)) → CC X₂)
      (pullbackMk (FC := FC) (CC := CC) f₁ f₂ x₁ x₂ h) =
    x₂

Tactic:
(congr_hom (PreservesPullback.iso_inv_snd (forget C) f₁ f₂) _).trans
    (congr_hom (Types.pullbackIsoPullback_inv_snd (↾f₁) (↾f₂)) _)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.PreservesPullback.iso_inv_snd, TypeCat.ofHom, CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd, CategoryTheory.Limits.Concrete.pullbackMk, CategoryTheory.forget, CategoryTheory.ConcreteCategory.congr_hom, DFunLike.coe, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
B : C
ι : Type w
X : ι → C
f : (j : ι) → X j ⟶ B
inst_3 : HasWidePullback B X f
inst_4 : PreservesLimit (wideCospan B X f) (forget C (FC := FC) (CC := CC))
x y : ToType (FC := FC) (CC := CC) (widePullback B X f)
h₀ :
  Eq (α := CC B) ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) x : CC B)
    ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) y : CC B)
h :
  ∀ (j : ι),
    Eq (α := CC (X j)) ((hom (FC := FC) (CC := CC) (π f j) : (a : CC (widePullback B X f)) → CC (X j)) x : CC (X j))
      ((hom (FC := FC) (CC := CC) (π f j) : (a : CC (widePullback B X f)) → CC (X j)) y : CC (X j))
a :
  ∀ (j : WidePullbackShape ι),
    Eq (α := CC ((wideCospan B X f).obj j))
      ((hom (FC := FC) (CC := CC) (limit.π (wideCospan B X f) j) :
            (a : CC (limit (wideCospan B X f))) → CC ((wideCospan B X f).obj j))
          x :
        CC ((wideCospan B X f).obj j))
      ((hom (FC := FC) (CC := CC) (limit.π (wideCospan B X f) j) :
            (a : CC (limit (wideCospan B X f))) → CC ((wideCospan B X f).obj j))
          y :
        CC ((wideCospan B X f).obj j))
⊢ x = y

Tactic:
apply Concrete.limit_ext

Premises used: CategoryTheory.Limits.Concrete.limit_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
B : C
ι : Type w
X : ι → C
f : (j : ι) → X j ⟶ B
inst_3 : HasWidePullback B X f
inst_4 : PreservesLimit (wideCospan B X f) (forget C (FC := FC) (CC := CC))
x y : ToType (FC := FC) (CC := CC) (widePullback B X f)
h₀ :
  Eq (α := CC B) ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) x : CC B)
    ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) y : CC B)
h :
  ∀ (j : ι),
    Eq (α := CC (X j)) ((hom (FC := FC) (CC := CC) (π f j) : (a : CC (widePullback B X f)) → CC (X j)) x : CC (X j))
      ((hom (FC := FC) (CC := CC) (π f j) : (a : CC (widePullback B X f)) → CC (X j)) y : CC (X j))
⊢ Eq (α := CC ((wideCospan B X f).obj none))
    ((hom (FC := FC) (CC := CC) (limit.π (wideCospan B X f) none) :
          (a : CC (limit (wideCospan B X f))) → CC ((wideCospan B X f).obj none))
        x :
      CC ((wideCospan B X f).obj none))
    ((hom (FC := FC) (CC := CC) (limit.π (wideCospan B X f) none) :
          (a : CC (limit (wideCospan B X f))) → CC ((wideCospan B X f).obj none))
        y :
      CC ((wideCospan B X f).obj none))

Tactic:
h₀
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
B : C
ι : Type w
X : ι → C
f : (j : ι) → X j ⟶ B
inst_3 : HasWidePullback B X f
inst_4 : PreservesLimit (wideCospan B X f) (forget C (FC := FC) (CC := CC))
x y : ToType (FC := FC) (CC := CC) (widePullback B X f)
h₀ :
  Eq (α := CC B) ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) x : CC B)
    ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) y : CC B)
h :
  ∀ (j : ι),
    Eq (α := CC (X j)) ((hom (FC := FC) (CC := CC) (π f j) : (a : CC (widePullback B X f)) → CC (X j)) x : CC (X j))
      ((hom (FC := FC) (CC := CC) (π f j) : (a : CC (widePullback B X f)) → CC (X j)) y : CC (X j))
⊢ Eq (α := CC ((wideCospan B X f).obj none))
    ((hom (FC := FC) (CC := CC) (limit.π (wideCospan B X f) none) :
          (a : CC (limit (wideCospan B X f))) → CC ((wideCospan B X f).obj none))
        x :
      CC ((wideCospan B X f).obj none))
    ((hom (FC := FC) (CC := CC) (limit.π (wideCospan B X f) none) :
          (a : CC (limit (wideCospan B X f))) → CC ((wideCospan B X f).obj none))
        y :
      CC ((wideCospan B X f).obj none))

Tactic:
exact h₀
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
B : C
ι : Type w
X : ι → C
f : (j : ι) → X j ⟶ B
inst_3 : HasWidePullback B X f
inst_4 : PreservesLimit (wideCospan B X f) (forget C (FC := FC) (CC := CC))
x y : ToType (FC := FC) (CC := CC) (widePullback B X f)
h₀ :
  Eq (α := CC B) ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) x : CC B)
    ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) y : CC B)
h :
  ∀ (j : ι),
    Eq (α := CC (X j)) ((hom (FC := FC) (CC := CC) (π f j) : (a : CC (widePullback B X f)) → CC (X j)) x : CC (X j))
      ((hom (FC := FC) (CC := CC) (π f j) : (a : CC (widePullback B X f)) → CC (X j)) y : CC (X j))
j : ι
⊢ Eq (α := CC ((wideCospan B X f).obj (some j)))
    ((hom (FC := FC) (CC := CC) (limit.π (wideCospan B X f) (some j)) :
          (a : CC (limit (wideCospan B X f))) → CC ((wideCospan B X f).obj (some j)))
        x :
      CC ((wideCospan B X f).obj (some j)))
    ((hom (FC := FC) (CC := CC) (limit.π (wideCospan B X f) (some j)) :
          (a : CC (limit (wideCospan B X f))) → CC ((wideCospan B X f).obj (some j)))
        y :
      CC ((wideCospan B X f).obj (some j)))

Tactic:
apply h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
B : C
ι : Type w
inst_3 : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst_4 : HasWidePullback B X f
inst_5 : PreservesLimit (wideCospan B X f) (forget C (FC := FC) (CC := CC))
x y : ToType (FC := FC) (CC := CC) (widePullback B X f)
h :
  ∀ (j : ι),
    Eq (α := CC (X j)) ((hom (FC := FC) (CC := CC) (π f j) : (a : CC (widePullback B X f)) → CC (X j)) x : CC (X j))
      ((hom (FC := FC) (CC := CC) (π f j) : (a : CC (widePullback B X f)) → CC (X j)) y : CC (X j))
apply :
  Eq (α := CC B) ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) x : CC B)
    ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) y : CC B)
⊢ x = y

Tactic:
apply Concrete.widePullback_ext _ _ _ _ h

Premises used: CategoryTheory.Limits.Concrete.widePullback_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
B : C
ι : Type w
inst_3 : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst_4 : HasWidePullback B X f
inst_5 : PreservesLimit (wideCospan B X f) (forget C (FC := FC) (CC := CC))
x y : ToType (FC := FC) (CC := CC) (widePullback B X f)
h :
  ∀ (j : ι),
    Eq (α := CC (X j)) ((hom (FC := FC) (CC := CC) (π f j) : (a : CC (widePullback B X f)) → CC (X j)) x : CC (X j))
      ((hom (FC := FC) (CC := CC) (π f j) : (a : CC (widePullback B X f)) → CC (X j)) y : CC (X j))
inhabit :
  ∀ (inhabited_h : Inhabited ι),
    Eq (α := CC B) ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) x : CC B)
      ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) y : CC B)
⊢ Eq (α := CC B) ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) x : CC B)
    ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) y : CC B)

Tactic:
inhabit ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
B : C
ι : Type w
inst_3 : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst_4 : HasWidePullback B X f
inst_5 : PreservesLimit (wideCospan B X f) (forget C (FC := FC) (CC := CC))
x y : ToType (FC := FC) (CC := CC) (widePullback B X f)
h :
  ∀ (j : ι),
    Eq (α := CC (X j)) ((hom (FC := FC) (CC := CC) (π f j) : (a : CC (widePullback B X f)) → CC (X j)) x : CC (X j))
      ((hom (FC := FC) (CC := CC) (π f j) : (a : CC (widePullback B X f)) → CC (X j)) y : CC (X j))
inhabited_h : Inhabited ι
⊢ Eq (α := CC B) ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) x : CC B)
    ((hom (FC := FC) (CC := CC) (base f) : (a : CC (widePullback B X f)) → CC B) y : CC B)

Tactic:
simp only [← π_arrow f default, ConcreteCategory.comp_apply, h]

Premises used: Inhabited.default, CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.Limits.WidePullback.π_arrow
-- 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 y : ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (multiequalizer I)
h :
  ∀ (t : J.L),
    Eq (α := CC (I.left t))
      ((hom (FC := FC) (CC := CC) (Multiequalizer.ι I t) : (a : CC (multiequalizer I)) → CC (I.left t)) x :
        CC (I.left t))
      ((hom (FC := FC) (CC := CC) (Multiequalizer.ι I t) : (a : CC (multiequalizer I)) → CC (I.left t)) y :
        CC (I.left t))
a :
  ∀ (j : WalkingMulticospan J),
    Eq (α := CC (I.multicospan.obj j))
      ((hom (FC := FC) (CC := CC) (limit.π I.multicospan j) : (a : CC (limit I.multicospan)) → CC (I.multicospan.obj j))
          x :
        CC (I.multicospan.obj j))
      ((hom (FC := FC) (CC := CC) (limit.π I.multicospan j) : (a : CC (limit I.multicospan)) → CC (I.multicospan.obj j))
          y :
        CC (I.multicospan.obj j))
⊢ x = y

Tactic:
apply Concrete.limit_ext

Premises used: CategoryTheory.Limits.Concrete.limit_ext
-- 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 y : ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (multiequalizer I)
h :
  ∀ (t : J.L),
    Eq (α := CC (I.left t))
      ((hom (FC := FC) (CC := CC) (Multiequalizer.ι I t) : (a : CC (multiequalizer I)) → CC (I.left t)) x :
        CC (I.left t))
      ((hom (FC := FC) (CC := CC) (Multiequalizer.ι I t) : (a : CC (multiequalizer I)) → CC (I.left t)) y :
        CC (I.left t))
a : J.L
⊢ Eq (α := CC (I.multicospan.obj (WalkingMulticospan.left a)))
    ((hom (FC := FC) (CC := CC) (limit.π I.multicospan (WalkingMulticospan.left a)) :
          (a_1 : CC (limit I.multicospan)) → CC (I.multicospan.obj (WalkingMulticospan.left a)))
        x :
      CC (I.multicospan.obj (WalkingMulticospan.left a)))
    ((hom (FC := FC) (CC := CC) (limit.π I.multicospan (WalkingMulticospan.left a)) :
          (a_1 : CC (limit I.multicospan)) → CC (I.multicospan.obj (WalkingMulticospan.left a)))
        y :
      CC (I.multicospan.obj (WalkingMulticospan.left a)))

Tactic:
apply h
-- 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 y : ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (multiequalizer I)
h :
  ∀ (t : J.L),
    Eq (α := CC (I.left t))
      ((hom (FC := FC) (CC := CC) (Multiequalizer.ι I t) : (a : CC (multiequalizer I)) → CC (I.left t)) x :
        CC (I.left t))
      ((hom (FC := FC) (CC := CC) (Multiequalizer.ι I t) : (a : CC (multiequalizer I)) → CC (I.left t)) y :
        CC (I.left t))
b : J.R
a :
  Eq (α := CC (I.multicospan.obj (WalkingMulticospan.right b)))
    ((hom (FC := FC) (CC := CC) (I.multicospan.map (WalkingMulticospan.Hom.fst b)) :
          (a : CC (I.multicospan.obj (WalkingMulticospan.left (J.fst b)))) →
            CC (I.multicospan.obj (WalkingMulticospan.right b)))
        ((hom (FC := FC) (CC := CC) (limit.π I.multicospan (WalkingMulticospan.left (J.fst b))) :
              (a : CC (limit I.multicospan)) → CC (I.multicospan.obj (WalkingMulticospan.left (J.fst b))))
            x :
          CC (I.multicospan.obj (WalkingMulticospan.left (J.fst b)))) :
      CC (I.multicospan.obj (WalkingMulticospan.right b)))
    ((hom (FC := FC) (CC := CC) (I.multicospan.map (WalkingMulticospan.Hom.fst b)) :
          (a : CC (I.multicospan.obj (WalkingMulticospan.left (J.fst b)))) →
            CC (I.multicospan.obj (WalkingMulticospan.right b)))
        ((hom (FC := FC) (CC := CC) (limit.π I.multicospan (WalkingMulticospan.left (J.fst b))) :
              (a : CC (limit I.multicospan)) → CC (I.multicospan.obj (WalkingMulticospan.left (J.fst b))))
            y :
          CC (I.multicospan.obj (WalkingMulticospan.left (J.fst b)))) :
      CC (I.multicospan.obj (WalkingMulticospan.right b)))
⊢ Eq (α := CC (I.multicospan.obj (WalkingMulticospan.right b)))
    ((hom (FC := FC) (CC := CC) (limit.π I.multicospan (WalkingMulticospan.right b)) :
          (a : CC (limit I.multicospan)) → CC (I.multicospan.obj (WalkingMulticospan.right b)))
        x :
      CC (I.multicospan.obj (WalkingMulticospan.right b)))
    ((hom (FC := FC) (CC := CC) (limit.π I.multicospan (WalkingMulticospan.right b)) :
          (a : CC (limit I.multicospan)) → CC (I.multicospan.obj (WalkingMulticospan.right b)))
        y :
      CC (I.multicospan.obj (WalkingMulticospan.right b)))

Tactic:
rw [← limit.w I.multicospan (WalkingMulticospan.Hom.fst b), ConcreteCategory.comp_apply,
      ConcreteCategory.comp_apply]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.Limits.MulticospanIndex.multicospan, CategoryTheory.Limits.limit.w, CategoryTheory.Limits.WalkingMulticospan.Hom.fst
-- 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 y : ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (multiequalizer I)
h :
  ∀ (t : J.L),
    Eq (α := CC (I.left t))
      ((hom (FC := FC) (CC := CC) (Multiequalizer.ι I t) : (a : CC (multiequalizer I)) → CC (I.left t)) x :
        CC (I.left t))
      ((hom (FC := FC) (CC := CC) (Multiequalizer.ι I t) : (a : CC (multiequalizer I)) → CC (I.left t)) y :
        CC (I.left t))
b : J.R
⊢ Eq (α := CC (I.multicospan.obj (WalkingMulticospan.right b)))
    ((hom (FC := FC) (CC := CC) (I.multicospan.map (WalkingMulticospan.Hom.fst b)) :
          (a : CC (I.multicospan.obj (WalkingMulticospan.left (J.fst b)))) →
            CC (I.multicospan.obj (WalkingMulticospan.right b)))
        ((hom (FC := FC) (CC := CC) (limit.π I.multicospan (WalkingMulticospan.left (J.fst b))) :
              (a : CC (limit I.multicospan)) → CC (I.multicospan.obj (WalkingMulticospan.left (J.fst b))))
            x :
          CC (I.multicospan.obj (WalkingMulticospan.left (J.fst b)))) :
      CC (I.multicospan.obj (WalkingMulticospan.right b)))
    ((hom (FC := FC) (CC := CC) (I.multicospan.map (WalkingMulticospan.Hom.fst b)) :
          (a : CC (I.multicospan.obj (WalkingMulticospan.left (J.fst b)))) →
            CC (I.multicospan.obj (WalkingMulticospan.right b)))
        ((hom (FC := FC) (CC := CC) (limit.π I.multicospan (WalkingMulticospan.left (J.fst b))) :
              (a : CC (limit I.multicospan)) → CC (I.multicospan.obj (WalkingMulticospan.left (J.fst b))))
            y :
          CC (I.multicospan.obj (WalkingMulticospan.left (J.fst b)))) :
      CC (I.multicospan.obj (WalkingMulticospan.right b)))

Tactic:
simp [h]
-- 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
⊢ (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)

Tactic:
have a := x.2 (WalkingMulticospan.Hom.fst i)
-- 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)
⊢ (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)

Tactic:
have b := x.2 (WalkingMulticospan.Hom.snd i)