awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Comma (goal)
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
F : J ⥤ Comma L R
inst_4 : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ Eq (α :=
    F.obj j₁ ⟶
      obj
        (obj (const J)
          { left := c₁.pt, right := c₂.pt, hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) })
        j₂)
    (F.map t ≫ { left := c₁.ι.app j₂, right := c₂.ι.app j₂, w := ⋯ })
    ({ left := c₁.ι.app j₁, right := c₂.ι.app j₁, w := ⋯ } ≫
      Functor.map
        (obj (const J)
          { left := c₁.pt, right := c₂.pt, hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) :
            Comma L R })
        t)
have h₁ : Eq (α :=
  (F.obj j₁).left ⟶
    left.{v₁, v₂, v₃, u₁, u₂, u₃} (T := T) (L := L) (R := R)
      (obj
        (obj (const J)
          { left := c₁.pt, right := c₂.pt, hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) })
        j₂))
  (CommaMorphism.left (F.map t ≫ { left := c₁.ι.app j₂, right := c₂.ι.app j₂, w := sorry }))
  (CommaMorphism.left
    ({ left := c₁.ι.app j₁, right := c₂.ι.app j₁, w := sorry } ≫
      Functor.map
        (obj (const J)
          { left := c₁.pt, right := c₂.pt, hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) :
            Comma L R })
        t))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Comma (goal)
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
F : J ⥤ Comma L R
inst_4 : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
j₁ j₂ : J
t : j₁ ⟶ j₂
h₁ :
  Eq (α :=
    (F.obj j₁).left ⟶
      left.{v₁, v₂, v₃, u₁, u₂, u₃} (T := T) (L := L) (R := R)
        (obj
          (obj (const J)
            { left := c₁.pt, right := c₂.pt, hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) })
          j₂))
    (CommaMorphism.left (F.map t ≫ { left := c₁.ι.app j₂, right := c₂.ι.app j₂, w := ⋯ }))
    (CommaMorphism.left
      ({ left := c₁.ι.app j₁, right := c₂.ι.app j₁, w := ⋯ } ≫
        Functor.map
          (obj (const J)
            { left := c₁.pt, right := c₂.pt, hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) :
              Comma L R })
          t))
⊢ Eq (α :=
    F.obj j₁ ⟶
      obj
        (obj (const J)
          { left := c₁.pt, right := c₂.pt, hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) })
        j₂)
    (F.map t ≫ { left := c₁.ι.app j₂, right := c₂.ι.app j₂, w := ⋯ })
    ({ left := c₁.ι.app j₁, right := c₂.ι.app j₁, w := ⋯ } ≫
      Functor.map
        (obj (const J)
          { left := c₁.pt, right := c₂.pt, hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) :
            Comma L R })
        t)
have h₂ : Eq (α :=
  (F.obj j₁).right ⟶
    right.{v₁, v₂, v₃, u₁, u₂, u₃} (T := T) (L := L) (R := R)
      (obj
        (obj (const J)
          { left := c₁.pt, right := c₂.pt, hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) })
        j₂))
  (CommaMorphism.right (F.map t ≫ { left := c₁.ι.app j₂, right := c₂.ι.app j₂, w := sorry }))
  (CommaMorphism.right
    ({ left := c₁.ι.app j₁, right := c₂.ι.app j₁, w := sorry } ≫
      Functor.map
        (obj (const J)
          { left := c₁.pt, right := c₂.pt, hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) :
            Comma L R })
        t))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Comma (goal)
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
F : J ⥤ Comma L R
inst_4 : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
t₂ : IsColimit c₂
s : Cocone F
j : J
⊢ Eq (α := ((F ⋙ fst L R) ⋙ L).obj j ⟶ R.obj s.pt.right)
    ((L.mapCocone c₁).ι.app j ≫ L.map (t₁.desc ((fst L R).mapCocone s)) ≫ s.pt.hom :
      ((F ⋙ fst L R) ⋙ L).obj j ⟶ R.obj s.pt.right)
    ((L.mapCocone c₁).ι.app j ≫ (coconeOfPreserves F t₁ c₂).pt.hom ≫ R.map (t₂.desc ((snd L R).mapCocone s)) :
      ((F ⋙ fst L R) ⋙ L).obj j ⟶ R.obj s.pt.right)
have rw : L.map (((fst L R).mapCocone s).ι.app j) ≫ s.pt.hom = (F.obj j).hom ≫ R.map (((snd L R).mapCocone s).ι.app j)
Tactic: rw [coconeOfPreserves_pt_hom, (isColimitOfPreserves L t₁).fac_assoc,
            colimitAuxiliaryCocone_ι_app, assoc, ← R.map_comp, t₂.fac, L.mapCocone_ι_app, ←
            L.map_comp_assoc, t₁.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Comma (goal)
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
F : J ⥤ Comma L R
inst_4 : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
t₂ : IsColimit c₂
s : Cocone F
m : (coconeOfPreserves F t₁ c₂).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfPreserves F t₁ c₂).ι.app j ≫ m = s.ι.app j
⊢ m = { left := t₁.desc ((fst L R).mapCocone s), right := t₂.desc ((snd L R).mapCocone s), w := ⋯ }
have left : m.left =
  CommaMorphism.left { left := t₁.desc ((fst L R).mapCocone s), right := t₂.desc ((snd L R).mapCocone s), w := sorry }
Tactic: apply CommaMorphism.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Comma (goal)
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
F : J ⥤ Comma L R
inst_4 : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
t₂ : IsColimit c₂
s : Cocone F
m : (coconeOfPreserves F t₁ c₂).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfPreserves F t₁ c₂).ι.app j ≫ m = s.ι.app j
left :
  m.left =
    CommaMorphism.left { left := t₁.desc ((fst L R).mapCocone s), right := t₂.desc ((snd L R).mapCocone s), w := ⋯ }
⊢ m = { left := t₁.desc ((fst L R).mapCocone s), right := t₂.desc ((snd L R).mapCocone s), w := ⋯ }
have right : m.right =
  CommaMorphism.right { left := t₁.desc ((fst L R).mapCocone s), right := t₂.desc ((snd L R).mapCocone s), w := sorry }
Tactic: apply CommaMorphism.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Comma (hypothesis)
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
F : J ⥤ Arrow.{v₃, u₃} T
i₁ : HasLimit (F ⋙ leftFunc)
i₂ : HasLimit (F ⋙ rightFunc)
⊢ HasLimit F
have this : HasLimit (F ⋙ Comma.fst (𝟭 T) (𝟭 T))
Tactic: haveI : HasLimit (F ⋙ Comma.fst _ _) := i₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Comma (hypothesis)
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
F : J ⥤ Arrow.{v₃, u₃} T
i₁ : HasLimit (F ⋙ leftFunc)
i₂ : HasLimit (F ⋙ rightFunc)
this : HasLimit (F ⋙ Comma.fst (𝟭 T) (𝟭 T))
⊢ HasLimit F
have this₁ : HasLimit (F ⋙ Comma.snd (𝟭 T) (𝟭 T))
Tactic: haveI : HasLimit (F ⋙ Comma.snd _ _) := i₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Comma (hypothesis)
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
F : J ⥤ Arrow.{v₃, u₃} T
i₁ : HasColimit (F ⋙ leftFunc)
i₂ : HasColimit (F ⋙ rightFunc)
⊢ HasColimit F
have this : HasColimit (F ⋙ Comma.fst (𝟭 T) (𝟭 T))
Tactic: haveI : HasColimit (F ⋙ Comma.fst _ _) := i₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Comma (hypothesis)
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
F : J ⥤ Arrow.{v₃, u₃} T
i₁ : HasColimit (F ⋙ leftFunc)
i₂ : HasColimit (F ⋙ rightFunc)
this : HasColimit (F ⋙ Comma.fst (𝟭 T) (𝟭 T))
⊢ HasColimit F
have this₁ : HasColimit (F ⋙ Comma.snd (𝟭 T) (𝟭 T))
Tactic: haveI : HasColimit (F ⋙ Comma.snd _ _) := i₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Comma (hypothesis)
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
X : T
G : Functor.{v₁, v₃, u₁, u₃} A T
F : J ⥤ StructuredArrow X G
i₁ : HasLimit (F ⋙ proj X G)
i₂ : PreservesLimit (F ⋙ proj X G) G
⊢ HasLimit F
have this : HasLimit (F ⋙ Comma.snd (fromPUnit X) G)
Tactic: haveI : HasLimit (F ⋙ Comma.snd (Functor.fromPUnit X) G) := i₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Comma (hypothesis)
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
X : T
G : Functor.{v₁, v₃, u₁, u₃} A T
F : J ⥤ StructuredArrow X G
i₁ : HasLimit (F ⋙ proj X G)
i₂ : PreservesLimit (F ⋙ proj X G) G
this : HasLimit (F ⋙ Comma.snd (fromPUnit X) G)
⊢ HasLimit F
have this₁ : PreservesLimit (F ⋙ Comma.snd (fromPUnit X) G) G
Tactic: haveI : PreservesLimit (F ⋙ Comma.snd (Functor.fromPUnit X) G) _ := i₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Comma (hypothesis)
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
G : Functor.{v₁, v₃, u₁, u₃} A T
X : T
F : J ⥤ CostructuredArrow G X
i₁ : HasColimit (F ⋙ proj G X)
i₂ : PreservesColimit (F ⋙ proj G X) G
⊢ HasColimit F
have this : HasColimit (F ⋙ Comma.fst G (fromPUnit X))
Tactic: haveI : HasColimit (F ⋙ Comma.fst G (Functor.fromPUnit X)) := i₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Comma (hypothesis)
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
G : Functor.{v₁, v₃, u₁, u₃} A T
X : T
F : J ⥤ CostructuredArrow G X
i₁ : HasColimit (F ⋙ proj G X)
i₂ : PreservesColimit (F ⋙ proj G X) G
this : HasColimit (F ⋙ Comma.fst G (fromPUnit X))
⊢ HasColimit F
have this₁ : PreservesColimit (F ⋙ Comma.fst G (fromPUnit X)) G
Tactic: haveI : PreservesColimit (F ⋙ Comma.fst G (Functor.fromPUnit X)) _ := i₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic (goal)
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)
inst_3 : Functor.IsCorepresentable (forget C (FC := FC) (CC := CC))
J : Type w
inst_4 : Category.{t, w} J
G : Functor.{t, v, w, u} J C
inst_5 : HasLimit G
⊢ Small.{v, max v w} (↑(G ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max v w))
have rw : HasLimit (G ⋙ forget C (FC := FC) (CC := CC))
Tactic: rw [← Types.hasLimit_iff_small_sections]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic (goal)
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)
⊢ x = y
have a : Eq (α := (↑(F ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max r w)))
  ((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 :
    (↑(F ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max r w)))
  ((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 :
    (↑(F ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max r w)))
Tactic: apply (Types.isLimitEquivSections (isLimitOfPreserves _ hD)).injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic (goal)
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)
⊢ Eq (α := (↑(F ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max r w)))
    ((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 :
      (↑(F ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max r w)))
    ((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 :
      (↑(F ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max r w)))
have a : ∀ (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: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic (goal)
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
⊢ ∃ (a : (j : J) × ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)), ff a = x
have 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
Tactic: obtain ⟨j, y, hy⟩ := Types.jointly_surjective_of_isColimit hE x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic (goal)
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
⊢ ∃ (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
have 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)))))
Tactic: obtain ⟨a, rfl⟩ := Concrete.from_union_surjective_of_isColimit F hD x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic (goal)
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
⊢ 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))
have 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))
Tactic: obtain ⟨k, f, g, (hfg : (F ⋙ forget C).map f x = F.map g y)⟩ := h
Cleared hypotheses: h