-- Module: Mathlib.CategoryTheory.Limits.Elements
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).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') ⋯) :
      (((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) ⋯ ≫
          F.map f) :
      (((Functor.const I).obj ⟨limit (F ⋙ π A), liftedConeElement F⟩).obj i).fst ⟶ (F.obj i').fst)

Tactic:
simpa using (limit.w _ _).symm

Premises used: Eq.symm, CategoryTheory.Limits.limit.w