-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Cones (goal)
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)
⊢ 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))
have 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))
Tactic: ext X