awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type r
inst_1 : (X Y : C) → FunLike.{u_1 + 1, r + 1, r + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{r, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
inst_4 : PreservesLimit F (forget C (FC := FC) (CC := CC))
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C (FC := FC) (CC := CC)) := Functor.mapCone (forget C (FC := FC) (CC := CC)) D
x : E.pt
y : ToType.{r, v, u, u_1} (FC := FC) (CC := CC) D.pt
H :
  Eq (α := (j : J) → CC (F.obj j))
    ((fun (x : ToType.{r, v, u, u_1} (FC := FC) (CC := CC) D.pt) (j : J) ↦
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.π.app j) :
              (a : CC (((Functor.const J).obj D.pt).obj j)) → CC (F.obj j))
            x :
          CC (F.obj j)))
      x)
    ((fun (x : ToType.{r, v, u, u_1} (FC := FC) (CC := CC) D.pt) (j : J) ↦
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.π.app j) :
              (a : CC (((Functor.const J).obj D.pt).obj j)) → CC (F.obj j))
            x :
          CC (F.obj j)))
      y)
j : J
⊢ Eq.{r + 1} (α := (F ⋙ forget C (FC := FC) (CC := CC)).obj j)
    ((↑((Types.isLimitEquivSections (isLimitOfPreserves (forget C (FC := FC) (CC := CC)) hD) :
              (a : ((forget C).mapCone D).pt) → (↑(F ⋙ forget C).sections : Type (max r w)))
            x) :
        (j : J) → (F ⋙ forget C).obj j)
      j)
    ((↑((Types.isLimitEquivSections (isLimitOfPreserves (forget C (FC := FC) (CC := CC)) hD) :
              (a : ((forget C).mapCone D).pt) → (↑(F ⋙ forget C).sections : Type (max r w)))
            y) :
        (j : J) → (F ⋙ forget C).obj j)
      j)

Tactic:
funext_iff.mp H j

Premises used: funext_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type r
inst_1 : (X Y : C) → FunLike.{u_1 + 1, r + 1, r + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{r, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
inst_4 : PreservesLimit F (forget C (FC := FC) (CC := CC))
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C (FC := FC) (CC := CC)) := Functor.mapCone (forget C (FC := FC) (CC := CC)) D
x : E.pt
y : ToType.{r, v, u, u_1} (FC := FC) (CC := CC) D.pt
H :
  Eq (α := (j : J) → CC (F.obj j))
    ((fun (x : ToType.{r, v, u, u_1} (FC := FC) (CC := CC) D.pt) (j : J) ↦
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.π.app j) :
              (a : CC (((Functor.const J).obj D.pt).obj j)) → CC (F.obj j))
            x :
          CC (F.obj j)))
      x)
    ((fun (x : ToType.{r, v, u, u_1} (FC := FC) (CC := CC) D.pt) (j : J) ↦
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.π.app j) :
              (a : CC (((Functor.const J).obj D.pt).obj j)) → CC (F.obj j))
            x :
          CC (F.obj j)))
      y)
j : J
⊢ Eq.{r + 1} (α := (F ⋙ forget C (FC := FC) (CC := CC)).obj j)
    ((↑((Types.isLimitEquivSections (isLimitOfPreserves (forget C (FC := FC) (CC := CC)) hD) :
              (a : ((forget C).mapCone D).pt) → (↑(F ⋙ forget C).sections : Type (max r w)))
            x) :
        (j : J) → (F ⋙ forget C).obj j)
      j)
    ((↑((Types.isLimitEquivSections (isLimitOfPreserves (forget C (FC := FC) (CC := CC)) hD) :
              (a : ((forget C).mapCone D).pt) → (↑(F ⋙ forget C).sections : Type (max r w)))
            y) :
        (j : J) → (F ⋙ forget C).obj j)
      j)

Tactic:
exact funext_iff.mp H j

Premises used: funext_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type r
inst_1 : (X Y : C) → FunLike.{u_1 + 1, r + 1, r + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{r, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
inst_4 : PreservesLimit F (forget C (FC := FC) (CC := CC))
D : Cone F
hD : IsLimit D
x y : ToType.{r, v, u, u_1} (FC := FC) (CC := CC) D.pt
⊢ (∀ (j : J),
      Eq (α := CC (F.obj j))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.π.app j) :
              (a : CC (((Functor.const J).obj D.pt).obj j)) → CC (F.obj j))
            x :
          CC (F.obj j))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.π.app j) :
              (a : CC (((Functor.const J).obj D.pt).obj j)) → CC (F.obj j))
            y :
          CC (F.obj j))) →
    x = y

Tactic:
fun h =>
  Concrete.to_product_injective_of_isLimit _ hD (funext h)

Premises used: CategoryTheory.Limits.Concrete.to_product_injective_of_isLimit, funext
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type r
inst_1 : (X Y : C) → FunLike.{u_1 + 1, r + 1, r + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{r, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
inst_4 : PreservesLimit F (forget C (FC := FC) (CC := CC))
inst_5 : HasLimit F
x y : ToType.{r, v, u, u_1} (FC := FC) (CC := CC) (limit F)
⊢ (∀ (j : J),
      Eq (α := CC (F.obj j))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (limit.π F j) : (a : CC (limit F)) → CC (F.obj j)) x :
          CC (F.obj j))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (limit.π F j) : (a : CC (limit F)) → CC (F.obj j)) y :
          CC (F.obj j))) →
    x = y

Tactic:
Concrete.isLimit_ext F (limit.isLimit _) _ _

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, CategoryTheory.Limits.Concrete.isLimit_ext
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_2
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_2 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesLimitsOfShape ℕᵒᵖ (forget C (FC := FC) (CC := CC))
F : Functor.{0, v, 0, u} ℕᵒᵖ C
c : Cone F
hc : IsLimit c
hF :
  ∀ (n : ℕ),
    Function.Surjective.{v + 1, v + 1} (α := CC (F.obj (Opposite.op n.succ))) (β := CC (F.obj (Opposite.op n)))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op)) :
        (a : CC (F.obj (Opposite.op n.succ))) → CC (F.obj (Opposite.op n)))
⊢ Function.Surjective.{v + 1, v + 1} (α :=
    CC (Functor.obj.{0, v, 0, u} (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (Opposite.op 0))) (β :=
    CC (F.obj (Opposite.op 0)))
    (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (c.π.app (Opposite.op 0))) :
      (a : CC (((Functor.const ℕᵒᵖ).obj c.pt).obj (Opposite.op 0))) → CC (F.obj (Opposite.op 0)))

Tactic:
Types.surjective_π_app_zero_of_surjective_map (isLimitOfPreserves (forget C) hc) hF

Premises used: CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map, CategoryTheory.forget, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst_1 : (X Y : C) → FunLike.{u_1 + 1, t + 1, t + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{t, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{r, w} J
F : Functor.{r, v, w, u} J C
inst_4 : PreservesColimit F (forget C (FC := FC) (CC := CC))
D : Cocone F
hD : IsColimit D
ff : (j : J) × ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j) →
  ToType.{t, v, u, u_1} (FC := FC) (CC := CC) D.pt :=
  fun (a : (j : J) × ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)) ↦
    (ConcreteCategory.hom (FC := FC) (CC := CC)
          (D.ι.app (a.fst (β := fun (j : J) ↦ ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)))) :
        (a_1 : CC (F.obj a.fst)) → CC (((Functor.const J).obj D.pt).obj a.fst))
      (a.snd (β := fun (j : J) ↦ ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)))
x : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) D.pt
E : Cocone (F ⋙ forget C (FC := FC) (CC := CC)) := Functor.mapCocone (forget C (FC := FC) (CC := CC)) D
hE : IsColimit E := isColimitOfPreserves (forget C (FC := FC) (CC := CC)) hD
obtain :
  ∀ (j : J) (y : (F ⋙ forget C (FC := FC) (CC := CC)).obj j)
    (hy :
      (ConcreteCategory.hom (FC := TypeCat.Fun) (E.ι.app j) :
            (a : (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj j)) →
              (fun (X : Type t) ↦ X) (((Functor.const J).obj E.pt).obj j))
          y =
        x),
    ∃ (a : (j : J) × ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)), ff a = x
⊢ ∃ (a : (j : J) × ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)), ff a = x

Tactic:
obtain ⟨j, y, hy⟩ := Types.jointly_surjective_of_isColimit hE x

Premises used: CategoryTheory.Limits.Types.jointly_surjective_of_isColimit
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst_1 : (X Y : C) → FunLike.{u_1 + 1, t + 1, t + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{t, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{r, w} J
F : Functor.{r, v, w, u} J C
inst_4 : PreservesColimit F (forget C (FC := FC) (CC := CC))
D : Cocone F
hD : IsColimit D
ff : (j : J) × ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j) →
  ToType.{t, v, u, u_1} (FC := FC) (CC := CC) D.pt :=
  fun (a : (j : J) × ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)) ↦
    (ConcreteCategory.hom (FC := FC) (CC := CC)
          (D.ι.app (a.fst (β := fun (j : J) ↦ ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)))) :
        (a_1 : CC (F.obj a.fst)) → CC (((Functor.const J).obj D.pt).obj a.fst))
      (a.snd (β := fun (j : J) ↦ ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)))
x : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) D.pt
E : Cocone (F ⋙ forget C (FC := FC) (CC := CC)) := Functor.mapCocone (forget C (FC := FC) (CC := CC)) D
hE : IsColimit E := isColimitOfPreserves (forget C (FC := FC) (CC := CC)) hD
j : J
y : (F ⋙ forget C (FC := FC) (CC := CC)).obj j
hy :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (E.ι.app j) :
        (a : (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj j)) →
          (fun (X : Type t) ↦ X) (((Functor.const J).obj E.pt).obj j))
      y =
    x
⊢ ∃ (a : (j : J) × ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)), ff a = x

Tactic:
⟨⟨j, y⟩, hy⟩

Premises used: Exists.intro, Sigma.mk
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst_1 : (X Y : C) → FunLike.{u_1 + 1, t + 1, t + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{t, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{r, w} J
F : Functor.{r, v, w, u} J C
inst_4 : PreservesColimit F (forget C (FC := FC) (CC := CC))
D : Cocone F
hD : IsColimit D
ff : (j : J) × ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j) →
  ToType.{t, v, u, u_1} (FC := FC) (CC := CC) D.pt :=
  fun (a : (j : J) × ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)) ↦
    (ConcreteCategory.hom (FC := FC) (CC := CC)
          (D.ι.app (a.fst (β := fun (j : J) ↦ ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)))) :
        (a_1 : CC (F.obj a.fst)) → CC (((Functor.const J).obj D.pt).obj a.fst))
      (a.snd (β := fun (j : J) ↦ ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)))
x : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) D.pt
E : Cocone (F ⋙ forget C (FC := FC) (CC := CC)) := Functor.mapCocone (forget C (FC := FC) (CC := CC)) D
hE : IsColimit E := isColimitOfPreserves (forget C (FC := FC) (CC := CC)) hD
j : J
y : (F ⋙ forget C (FC := FC) (CC := CC)).obj j
hy :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (E.ι.app j) :
        (a : (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj j)) →
          (fun (X : Type t) ↦ X) (((Functor.const J).obj E.pt).obj j))
      y =
    x
⊢ ∃ (a : (j : J) × ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)), ff a = x

Tactic:
exact ⟨⟨j, y⟩, hy⟩
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst_1 : (X Y : C) → FunLike.{u_1 + 1, t + 1, t + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{t, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{r, w} J
F : Functor.{r, v, w, u} J C
inst_4 : PreservesColimit F (forget C (FC := FC) (CC := CC))
D : Cocone F
hD : IsColimit D
x : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) D.pt
obtain :
  ∀ (a : (j : J) × ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)),
    ∃ (j : J) (y : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)),
      Eq (α := CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) j))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.ι.app j) :
              (a : CC (F.obj j)) → CC (((Functor.const J).obj D.pt).obj j))
            y :
          CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) j))
        ((fun (a : (j : J) × ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)) ↦
              ((ConcreteCategory.hom (FC := FC) (CC := CC)
                      (D.ι.app (a.fst (β := fun (j : J) ↦ ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)))) :
                    (a_1 : CC (F.obj a.fst)) → CC (((Functor.const J).obj D.pt).obj a.fst))
                  (a.snd (β := fun (j : J) ↦ ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j))) :
                CC
                  (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt)
                    (a.fst (β := fun (j : J) ↦ ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j))))))
            a :
          CC
            (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt)
              (a.fst (β := fun (j : J) ↦ ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)))))
⊢ ∃ (j : J) (y : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)),
    (ConcreteCategory.hom (FC := FC) (CC := CC) (D.ι.app j) :
          (a : CC (F.obj j)) → CC (((Functor.const J).obj D.pt).obj j))
        y =
      x

Tactic:
obtain ⟨a, rfl⟩ := Concrete.from_union_surjective_of_isColimit F hD x

Premises used: CategoryTheory.Limits.Concrete.from_union_surjective_of_isColimit, rfl
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst_1 : (X Y : C) → FunLike.{u_1 + 1, t + 1, t + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{t, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{r, w} J
F : Functor.{r, v, w, u} J C
inst_4 : PreservesColimit F (forget C (FC := FC) (CC := CC))
D : Cocone F
hD : IsColimit D
a : (j : J) × ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)
⊢ ∃ (j : J) (y : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)),
    Eq (α := CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) j))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.ι.app j) :
            (a : CC (F.obj j)) → CC (((Functor.const J).obj D.pt).obj j))
          y :
        CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) j))
      ((fun (a : (j : J) × ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)) ↦
            ((ConcreteCategory.hom (FC := FC) (CC := CC)
                    (D.ι.app (a.fst (β := fun (j : J) ↦ ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)))) :
                  (a_1 : CC (F.obj a.fst)) → CC (((Functor.const J).obj D.pt).obj a.fst))
                (a.snd (β := fun (j : J) ↦ ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j))) :
              CC
                (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt)
                  (a.fst (β := fun (j : J) ↦ ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j))))))
          a :
        CC
          (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt)
            (a.fst (β := fun (j : J) ↦ ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)))))

Tactic:
⟨a.1, a.2, rfl⟩

Premises used: Sigma.fst, Exists.intro, Sigma.snd, rfl
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst_1 : (X Y : C) → FunLike.{u_1 + 1, t + 1, t + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{t, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{r, w} J
F : Functor.{r, v, w, u} J C
inst_4 : PreservesColimit F (forget C (FC := FC) (CC := CC))
D : Cocone F
hD : IsColimit D
a : (j : J) × ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)
⊢ ∃ (j : J) (y : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)),
    Eq (α := CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) j))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.ι.app j) :
            (a : CC (F.obj j)) → CC (((Functor.const J).obj D.pt).obj j))
          y :
        CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) j))
      ((fun (a : (j : J) × ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)) ↦
            ((ConcreteCategory.hom (FC := FC) (CC := CC)
                    (D.ι.app (a.fst (β := fun (j : J) ↦ ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)))) :
                  (a_1 : CC (F.obj a.fst)) → CC (((Functor.const J).obj D.pt).obj a.fst))
                (a.snd (β := fun (j : J) ↦ ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j))) :
              CC
                (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt)
                  (a.fst (β := fun (j : J) ↦ ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j))))))
          a :
        CC
          (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt)
            (a.fst (β := fun (j : J) ↦ ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)))))

Tactic:
exact ⟨a.1, a.2, rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst_1 : (X Y : C) → FunLike.{u_1 + 1, t + 1, t + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{t, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{r, w} J
F : Functor.{r, v, w, u} J C
inst_4 : PreservesColimit F (forget C (FC := FC) (CC := CC))
inst_5 : HasColimit F
x : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (colimit F)
⊢ ∃ (j : J) (y : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)),
    (ConcreteCategory.hom (FC := FC) (CC := CC) (colimit.ι F j) : (a : CC (F.obj j)) → CC (colimit F)) y = x

Tactic:
Concrete.isColimit_exists_rep F (colimit.isColimit _) x

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.Concrete.isColimit_exists_rep, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst_1 : (X Y : C) → FunLike.{u_1 + 1, t + 1, t + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{t, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{r, w} J
F : Functor.{r, v, w, u} J C
D : Cocone F
i j : J
x : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj i)
y : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)
h :
  ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k),
    Eq (α := CC (F.obj k))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map f) : (a : CC (F.obj i)) → CC (F.obj k)) x : CC (F.obj k))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map g) : (a : CC (F.obj j)) → CC (F.obj k)) y : CC (F.obj k))
E : Cocone (F ⋙ forget C (FC := FC) (CC := CC)) := Functor.mapCocone (forget C (FC := FC) (CC := CC)) D
obtain :
  ∀ (k : J) (f : i ⟶ k) (g : j ⟶ k)
    (hfg :
      Eq (α := (fun (X : Type t) ↦ X) ((F ⋙ forget C (FC := FC) (CC := CC)).obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget C (FC := FC) (CC := CC)).map f) :
              (a : (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj i)) → (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj k))
            x :
          (fun (X : Type t) ↦ X) ((F ⋙ forget C (FC := FC) (CC := CC)).obj k))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map g) : (a : CC (F.obj j)) → CC (F.obj k)) y : CC (F.obj k))),
    Eq (α := CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) i))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.ι.app i) :
            (a : CC (F.obj i)) → CC (((Functor.const J).obj D.pt).obj i))
          x :
        CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) i))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.ι.app j) :
            (a : CC (F.obj j)) → CC (((Functor.const J).obj D.pt).obj j))
          y :
        CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) j))
⊢ Eq (α := CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) i))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.ι.app i) :
          (a : CC (F.obj i)) → CC (((Functor.const J).obj D.pt).obj i))
        x :
      CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) i))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.ι.app j) :
          (a : CC (F.obj j)) → CC (((Functor.const J).obj D.pt).obj j))
        y :
      CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) j))

Tactic:
obtain ⟨k, f, g, (hfg : (F ⋙ forget C).map f x = F.map g y)⟩ := h
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst_1 : (X Y : C) → FunLike.{u_1 + 1, t + 1, t + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{t, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{r, w} J
F : Functor.{r, v, w, u} J C
D : Cocone F
i j : J
x : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj i)
y : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)
E : Cocone (F ⋙ forget C (FC := FC) (CC := CC)) := Functor.mapCocone (forget C (FC := FC) (CC := CC)) D
k : J
f : i ⟶ k
g : j ⟶ k
hfg :
  Eq (α := (fun (X : Type t) ↦ X) ((F ⋙ forget C (FC := FC) (CC := CC)).obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget C (FC := FC) (CC := CC)).map f) :
          (a : (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj i)) → (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj k))
        x :
      (fun (X : Type t) ↦ X) ((F ⋙ forget C (FC := FC) (CC := CC)).obj k))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map g) : (a : CC (F.obj j)) → CC (F.obj k)) y : CC (F.obj k))
h1 : (F ⋙ forget C (FC := FC) (CC := CC)).map f ≫ E.ι.app k = E.ι.app i := ⋯
h2 : (F ⋙ forget C (FC := FC) (CC := CC)).map g ≫ E.ι.app k = E.ι.app j := ⋯
change :
  Eq (α := (fun (X : Type t) ↦ X) (Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (E.ι.app i) :
          (a : (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj i)) →
            (fun (X : Type t) ↦ X) (((Functor.const J).obj E.pt).obj i))
        x :
      (fun (X : Type t) ↦ X) (Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (E.ι.app j) :
          (a : (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj j)) →
            (fun (X : Type t) ↦ X) (((Functor.const J).obj E.pt).obj j))
        y :
      (fun (X : Type t) ↦ X) (Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) j))
⊢ Eq (α := CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) i))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.ι.app i) :
          (a : CC (F.obj i)) → CC (((Functor.const J).obj D.pt).obj i))
        x :
      CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) i))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.ι.app j) :
          (a : CC (F.obj j)) → CC (((Functor.const J).obj D.pt).obj j))
        y :
      CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) j))

Tactic:
change E.ι.app i x = E.ι.app j y

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.Cocone.ι, DFunLike.coe, CategoryTheory.NatTrans.app