-- 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
c : Cone F
i : I
h₁ :
  Eq (α := ((F ⋙ π A) ⋙ A).obj i)
    ((hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := limit ((F ⋙ π A) ⋙ A))
              (Iso.hom (preservesLimitIso A (F ⋙ π A)) : A.obj (limit (F ⋙ π A)) ⟶ limit ((F ⋙ π A) ⋙ A))
              (limit.π ((F ⋙ π A) ⋙ A) i : limit ((F ⋙ π A) ⋙ A) ⟶ ((F ⋙ π A) ⋙ A).obj i)) :
          (a : A.obj (limit (F ⋙ π A))) → ((F ⋙ π A) ⋙ A).obj i)
        ((hom (FC := TypeCat.Fun) (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c))) :
              (a : (fun (X : Type w) ↦ X) (A.obj ((π A).mapCone c).pt)) →
                (fun (X : Type w) ↦ X) (A.obj (limit (F ⋙ π A))))
            (c.pt.snd (β := fun (c : C) ↦ A.obj c)) :
          (fun (X : Type w) ↦ X) (A.obj (limit (F ⋙ π A)))) :
      ((F ⋙ π A) ⋙ A).obj i)
    ((hom (FC := TypeCat.Fun) (A.map (limit.π (F ⋙ π A) i)) : (a : A.obj (limit (F ⋙ π A))) → ((F ⋙ π A) ⋙ A).obj i)
        ((hom (FC := TypeCat.Fun) (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c))) :
              (a : (fun (X : Type w) ↦ X) (A.obj ((π A).mapCone c).pt)) →
                (fun (X : Type w) ↦ X) (A.obj (limit (F ⋙ π A))))
            (c.pt.snd (β := fun (c : C) ↦ A.obj c)) :
          (fun (X : Type w) ↦ X) (A.obj (limit (F ⋙ π A)))) :
      ((F ⋙ π A) ⋙ A).obj i)
h₂ :
  (hom (FC := TypeCat.Fun) (A.map (↑(c.π.app i) : (((Functor.const I).obj c.pt).obj i).fst ⟶ (F.obj i).fst)) :
        (a : (fun (X : Type w) ↦ X) (A.obj (((Functor.const I).obj c.pt).obj i).fst)) →
          (fun (X : Type w) ↦ X) (A.obj (F.obj i).fst))
      ((Functor.obj (Functor.obj (Functor.const I) c.pt) i).snd (β := fun (c : C) ↦ A.obj c)) =
    (F.obj i).snd (β := fun (c : C) ↦ A.obj c)
⊢ Eq (α := (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj i))
    ((hom (FC := TypeCat.Fun) (limit.π ((F ⋙ π A) ⋙ A) i) :
          (a : (fun (X : Type w) ↦ X) (limit ((F ⋙ π A) ⋙ A))) → (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj i))
        (((Iso.toEquiv (preservesLimitIso A (F ⋙ π A)) : A.obj (limit (F ⋙ π A)) ≃ limit ((F ⋙ π A) ⋙ A)) :
              (a : A.obj (limit (F ⋙ π A))) → limit ((F ⋙ π A) ⋙ A))
            ((@hom _ types TypeCat.Fun _ _ _ _ _ (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c))) :
                  (a : A.obj c.pt.fst) → A.obj (limit (F ⋙ π A)))
                (c.pt.snd (β := fun (c : C) ↦ A.obj c)) :
              A.obj (limit (F ⋙ π A))) :
          limit ((F ⋙ π A) ⋙ A)) :
      (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj i))
    ((hom (FC := TypeCat.Fun) (limit.π ((F ⋙ π A) ⋙ A) i) :
          (a : (fun (X : Type w) ↦ X) (limit ((F ⋙ π A) ⋙ A))) → (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj i))
        (((Iso.toEquiv (preservesLimitIso A (F ⋙ π A)) : A.obj (limit (F ⋙ π A)) ≃ limit ((F ⋙ π A) ⋙ A)) :
              (a : A.obj (limit (F ⋙ π A))) → limit ((F ⋙ π A) ⋙ A))
            (liftedConeElement F : A.obj (limit (F ⋙ π A))) :
          limit ((F ⋙ π A) ⋙ A)) :
      (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj i))

Tactic:
simpa [-Functor.comp_obj, ← comp_apply, ← Functor.map_comp, liftedConeElement, liftedConeElement']

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement, CategoryTheory.comp_apply, CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement', CategoryTheory.Functor.map_comp