-- Module: Mathlib.CategoryTheory.Limits.Cones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
D : Type u₄
inst_3 : Category.{v₄, u₄} D
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F_1 F : Functor.{v₁, v₃, u₁, u₃} J C
h :
  ∀ (X : (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)),
    Sigma.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := Cone F)
              (↾fun (c : (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)) ↦
                { pt := unop (c.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)),
                  π := c.snd (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) : Cone F })
              (↾fun (c : Cone F) ↦ Sigma.mk (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) (op c.pt) c.π)))
          X) =
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 ((X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)))).toFun X).fst (β :=
        fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)
h₁ :
  ∀ (X : (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)),
    HEq (α :=
      obj (const J)
          (unop
            (Sigma.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)
              (TypeCat.Fun.toFun
                (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (CategoryStruct.comp (Y := Cone F)
                    (↾fun (c : (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)) ↦
                      { pt := unop (c.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)),
                        π := c.snd (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) : Cone F })
                    (↾fun (c : Cone F) ↦ Sigma.mk (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) (op c.pt) c.π)))
                X))) ⟶
        F)
      (Sigma.snd (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)
          (TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y := Cone F)
                (↾fun (c : (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)) ↦
                  { pt := unop (c.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)),
                    π := c.snd (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) : Cone F })
                (↾fun (c : Cone F) ↦ Sigma.mk (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) (op c.pt) c.π)))
            X) :
        obj (const J)
            (unop
              (Sigma.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)
                (TypeCat.Fun.toFun
                  (ConcreteCategory.hom (FC := TypeCat.Fun)
                    (CategoryStruct.comp (Y := Cone F)
                      (↾fun (c : (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)) ↦
                        { pt := unop (c.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)),
                          π := c.snd (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) : Cone F })
                      (↾fun (c : Cone F) ↦ Sigma.mk (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) (op c.pt) c.π)))
                  X))) ⟶
          F)
      (((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 ((X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)))).toFun X).snd (β :=
        fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F))
⊢ CategoryStruct.comp (Y := Cone F)
      (↾fun (c : (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)) ↦
        { pt := unop (c.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)),
          π := c.snd (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) })
      (↾fun (c : Cone F) ↦ Sigma.mk (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) (op c.pt) c.π) =
    𝟙 ((X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F))

Tactic:
ext X