Module: Mathlib.CategoryTheory.Presentable.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
j₁ : J
α : j₀ ⟶ j₁
hα :
  ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
    (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
      (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')
s : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j₁)).sections :=
  ⟨fun k ↦ (ConcreteCategory.hom ((F.obj k).map (X.map α))) (z k), ⋯⟩
k : K
h₁ :
  ↑((Types.isLimitEquivSections (hc cX.pt))
          ((ConcreteCategory.hom (c.pt.map (cX.ι.app j₁))) ((Types.isLimitEquivSections (hc (X.obj j₁))).symm s)))
      k =
    (ConcreteCategory.hom ((c.π.app k).app cX.pt))
      ((ConcreteCategory.hom (c.pt.map (cX.ι.app j₁))) ((Types.isLimitEquivSections (hc (X.obj j₁))).symm s))
h₂ : (ConcreteCategory.hom ((c.π.app k).app (X.obj j₁))) ((Types.isLimitEquivSections (hc (X.obj j₁))).symm s) = ↑s k
⊢ ↑y k =
    ↑((Types.isLimitEquivSections (hc cX.pt))
          ((ConcreteCategory.hom (c.pt.map (cX.ι.app j₁))) ((Types.isLimitEquivSections (hc (X.obj j₁))).symm s)))
      k

Tactic:
rw [h₁, hz, NatTrans.naturality_apply, h₂, ← comp_apply, ← Functor.map_comp, cX.w]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
j₁ : J
α : j₀ ⟶ j₁
hα :
  ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
    (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
      (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')
s : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j₁)).sections :=
  ⟨fun k ↦ (ConcreteCategory.hom ((F.obj k).map (X.map α))) (z k), ⋯⟩
k : K
h₁ :
  ↑((Types.isLimitEquivSections (hc cX.pt))
          ((ConcreteCategory.hom (c.pt.map (cX.ι.app j₁))) ((Types.isLimitEquivSections (hc (X.obj j₁))).symm s)))
      k =
    (ConcreteCategory.hom ((c.π.app k).app cX.pt))
      ((ConcreteCategory.hom (c.pt.map (cX.ι.app j₁))) ((Types.isLimitEquivSections (hc (X.obj j₁))).symm s))
h₂ : (ConcreteCategory.hom ((c.π.app k).app (X.obj j₁))) ((Types.isLimitEquivSections (hc (X.obj j₁))).symm s) = ↑s k
⊢ (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k) =
    (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)