-- Mathlib/CategoryTheory/Limits/Elements.lean
@[simp]
lemma map_lift_mapCone (c : Cone F) :
    A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd = liftedConeElement F

Proof state:
case a.w
C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
c : Cone F
i : I
⊢ limit.π ((F ⋙ π A) ⋙ A) i
      ((preservesLimitIso A (F ⋙ π A)).toEquiv (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd)) =
    limit.π ((F ⋙ π A) ⋙ A) i ((preservesLimitIso A (F ⋙ π A)).toEquiv (liftedConeElement F))

Tactic:
have h₁ := congrFun (preservesLimitIso_hom_π A (F ⋙ π A) i)
  (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd)

Result:
case a.w
C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
c : Cone F
i : I
h₁ :
  ((preservesLimitIso A (F ⋙ π A)).hom ≫ limit.π ((F ⋙ π A) ⋙ A) i)
      (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd) =
    A.map (limit.π (F ⋙ π A) i) (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd)
⊢ limit.π ((F ⋙ π A) ⋙ A) i
      ((preservesLimitIso A (F ⋙ π A)).toEquiv (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd)) =
    limit.π ((F ⋙ π A) ⋙ A) i ((preservesLimitIso A (F ⋙ π A)).toEquiv (liftedConeElement F))

Proof state:
case a.w
C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
c : Cone F
i : I
h₁ :
  ((preservesLimitIso A (F ⋙ π A)).hom ≫ limit.π ((F ⋙ π A) ⋙ A) i)
      (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd) =
    A.map (limit.π (F ⋙ π A) i) (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd)
⊢ limit.π ((F ⋙ π A) ⋙ A) i
      ((preservesLimitIso A (F ⋙ π A)).toEquiv (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd)) =
    limit.π ((F ⋙ π A) ⋙ A) i ((preservesLimitIso A (F ⋙ π A)).toEquiv (liftedConeElement F))

Tactic:
have h₂ := (c.π.app i).property

Result:
case a.w
C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
c : Cone F
i : I
h₁ :
  ((preservesLimitIso A (F ⋙ π A)).hom ≫ limit.π ((F ⋙ π A) ⋙ A) i)
      (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd) =
    A.map (limit.π (F ⋙ π A) i) (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd)
h₂ : A.map (↑(c.π.app i)) (((Functor.const I).obj c.pt).obj i).snd = (F.obj i).snd
⊢ limit.π ((F ⋙ π A) ⋙ A) i
      ((preservesLimitIso A (F ⋙ π A)).toEquiv (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd)) =
    limit.π ((F ⋙ π A) ⋙ A) i ((preservesLimitIso A (F ⋙ π A)).toEquiv (liftedConeElement F))

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
c : Cone F
⊢ A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd = liftedConeElement F

Tactic:
apply (preservesLimitIso A (F ⋙ π A)).toEquiv.injective

Result:
case a
C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
c : Cone F
⊢ (preservesLimitIso A (F ⋙ π A)).toEquiv (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd) =
    (preservesLimitIso A (F ⋙ π A)).toEquiv (liftedConeElement F)

Proof state:
case a.w
C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
c : Cone F
i : I
h₁ :
  ((preservesLimitIso A (F ⋙ π A)).hom ≫ limit.π ((F ⋙ π A) ⋙ A) i)
      (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd) =
    A.map (limit.π (F ⋙ π A) i) (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd)
h₂ : A.map (↑(c.π.app i)) (((Functor.const I).obj c.pt).obj i).snd = (F.obj i).snd
⊢ limit.π ((F ⋙ π A) ⋙ A) i
      ((preservesLimitIso A (F ⋙ π A)).toEquiv (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd)) =
    limit.π ((F ⋙ π A) ⋙ A) i ((preservesLimitIso A (F ⋙ π A)).toEquiv (liftedConeElement F))

Tactic:
simp_all [← FunctorToTypes.map_comp_apply, liftedConeElement]

Result:
no goals

Proof state:
case a
C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
c : Cone F
⊢ (preservesLimitIso A (F ⋙ π A)).toEquiv (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd) =
    (preservesLimitIso A (F ⋙ π A)).toEquiv (liftedConeElement F)

Tactic:
ext i

Result:
case a.w
C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
c : Cone F
i : I
⊢ limit.π ((F ⋙ π A) ⋙ A) i
      ((preservesLimitIso A (F ⋙ π A)).toEquiv (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd)) =
    limit.π ((F ⋙ π A) ⋙ A) i ((preservesLimitIso A (F ⋙ π A)).toEquiv (liftedConeElement F))