-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, w, u, w + 1} C (Type w)
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : Small.{w, u₁} I
F : I ⥤ A.Elements
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} I C
inst_4 : PreservesLimitsOfShape.{v₁, u₁, v, w, u, w + 1} I A
i i' : I
f : i ⟶ i'
⊢ Eq (α :=
    Functor.obj
        (Functor.obj (Functor.const I)
          (Sigma.mk (β := fun (c : C) ↦ A.obj c) (limit (F ⋙ π A)) (liftedConeElement F : A.obj (limit (F ⋙ π A)))))
        i ⟶
      F.obj i')
    (Functor.map
        (Functor.obj (Functor.const I)
          (Sigma.mk (β := fun (c : C) ↦ A.obj c) (limit (F ⋙ π A)) (liftedConeElement F : A.obj (limit (F ⋙ π A)))))
        f ≫
      Subtype.mk (p :=
        fun
          (f :
            (Functor.obj
                    (Functor.obj (Functor.const I)
                      (Sigma.mk (β := fun (c : C) ↦ A.obj c) (limit (F ⋙ π A))
                        (liftedConeElement F : A.obj (limit (F ⋙ π A)))))
                    i').fst
                (β := fun (c : C) ↦ A.obj c) ⟶
              (F.obj i').fst (β := fun (c : C) ↦ A.obj c)) ↦
        (hom (FC := TypeCat.Fun) (A.map f) :
              (a :
                  (fun (X : Type w) ↦ X)
                    (A.obj (((Functor.const I).obj ⟨limit (F ⋙ π A), liftedConeElement F⟩).obj i').fst)) →
                (fun (X : Type w) ↦ X) (A.obj (F.obj i').fst))
            ((Functor.obj
                  (Functor.obj (Functor.const I)
                    (Sigma.mk (β := fun (c : C) ↦ A.obj c) (limit (F ⋙ π A))
                      (liftedConeElement F : A.obj (limit (F ⋙ π A)))))
                  i').snd
              (β := fun (c : C) ↦ A.obj c)) =
          (F.obj i').snd (β := fun (c : C) ↦ A.obj c))
        (limit.π (F ⋙ π A) i') ⋯)
    (Subtype.mk (p :=
        fun
          (f :
            (Functor.obj
                    (Functor.obj (Functor.const I)
                      (Sigma.mk (β := fun (c : C) ↦ A.obj c) (limit (F ⋙ π A))
                        (liftedConeElement F : A.obj (limit (F ⋙ π A)))))
                    i).fst
                (β := fun (c : C) ↦ A.obj c) ⟶
              (F.obj i).fst (β := fun (c : C) ↦ A.obj c)) ↦
        (hom (FC := TypeCat.Fun) (A.map f) :
              (a :
                  (fun (X : Type w) ↦ X)
                    (A.obj (((Functor.const I).obj ⟨limit (F ⋙ π A), liftedConeElement F⟩).obj i).fst)) →
                (fun (X : Type w) ↦ X) (A.obj (F.obj i).fst))
            ((Functor.obj
                  (Functor.obj (Functor.const I)
                    (Sigma.mk (β := fun (c : C) ↦ A.obj c) (limit (F ⋙ π A))
                      (liftedConeElement F : A.obj (limit (F ⋙ π A)))))
                  i).snd
              (β := fun (c : C) ↦ A.obj c)) =
          (F.obj i).snd (β := fun (c : C) ↦ A.obj c))
        (limit.π (F ⋙ π A) i) ⋯ ≫
      F.map f)
have w : Eq (α :=
  (Functor.obj
          (Functor.obj (Functor.const I)
            (Sigma.mk (β := fun (c : C) ↦ A.obj c) (limit (F ⋙ π A)) (liftedConeElement F : A.obj (limit (F ⋙ π A)))))
          i).fst
      (β := fun (c : C) ↦ A.obj c) ⟶
    (F.obj i').fst (β := fun (c : C) ↦ A.obj c))
  (↑(Functor.map
          (Functor.obj (Functor.const I)
            (Sigma.mk (β := fun (c : C) ↦ A.obj c) (limit (F ⋙ π A)) (liftedConeElement F : A.obj (limit (F ⋙ π A)))))
          f ≫
        Subtype.mk (p :=
          fun
            (f :
              (Functor.obj
                      (Functor.obj (Functor.const I)
                        (Sigma.mk (β := fun (c : C) ↦ A.obj c) (limit (F ⋙ π A))
                          (liftedConeElement F : A.obj (limit (F ⋙ π A)))))
                      i').fst
                  (β := fun (c : C) ↦ A.obj c) ⟶
                (F.obj i').fst (β := fun (c : C) ↦ A.obj c)) ↦
          (hom (FC := TypeCat.Fun) (A.map f) :
                (a :
                    (fun (X : Type w) ↦ X)
                      (A.obj (((Functor.const I).obj ⟨limit (F ⋙ π A), liftedConeElement F⟩).obj i').fst)) →
                  (fun (X : Type w) ↦ X) (A.obj (F.obj i').fst))
              ((Functor.obj
                    (Functor.obj (Functor.const I)
                      (Sigma.mk (β := fun (c : C) ↦ A.obj c) (limit (F ⋙ π A))
                        (liftedConeElement F : A.obj (limit (F ⋙ π A)))))
                    i').snd
                (β := fun (c : C) ↦ A.obj c)) =
            (F.obj i').snd (β := fun (c : C) ↦ A.obj c))
          (limit.π (F ⋙ π A) i') sorry) :
    (((Functor.const I).obj ⟨limit (F ⋙ π A), liftedConeElement F⟩).obj i).fst ⟶ (F.obj i').fst)
  (↑(Subtype.mk (p :=
          fun
            (f :
              (Functor.obj
                      (Functor.obj (Functor.const I)
                        (Sigma.mk (β := fun (c : C) ↦ A.obj c) (limit (F ⋙ π A))
                          (liftedConeElement F : A.obj (limit (F ⋙ π A)))))
                      i).fst
                  (β := fun (c : C) ↦ A.obj c) ⟶
                (F.obj i).fst (β := fun (c : C) ↦ A.obj c)) ↦
          (hom (FC := TypeCat.Fun) (A.map f) :
                (a :
                    (fun (X : Type w) ↦ X)
                      (A.obj (((Functor.const I).obj ⟨limit (F ⋙ π A), liftedConeElement F⟩).obj i).fst)) →
                  (fun (X : Type w) ↦ X) (A.obj (F.obj i).fst))
              ((Functor.obj
                    (Functor.obj (Functor.const I)
                      (Sigma.mk (β := fun (c : C) ↦ A.obj c) (limit (F ⋙ π A))
                        (liftedConeElement F : A.obj (limit (F ⋙ π A)))))
                    i).snd
                (β := fun (c : C) ↦ A.obj c)) =
            (F.obj i).snd (β := fun (c : C) ↦ A.obj c))
          (limit.π (F ⋙ π A) i) sorry ≫
        F.map f) :
    (((Functor.const I).obj ⟨limit (F ⋙ π A), liftedConeElement F⟩).obj i).fst ⟶ (F.obj i').fst)
Tactic: ext