-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type u₁
inst_2 : Category.{v₁, u₁} J
K : Type u₂
inst_3 : Category.{v₂, u₂} K
F : J ⥤ Functor.{v₂, v, u₂, u} K C
c : (k : K) → LimitCone (F.flip.obj k)
j₁ j₂ : J
g : j₁ ⟶ j₂
w :
  ∀ (k : K),
    (map
              (obj (const J)
                { obj := fun (k : K) ↦ (c k).cone.pt,
                  map := fun {k₁ k₂ : K} (f : k₁ ⟶ k₂) ↦
                    (c k₂).isLimit.lift
                      { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map f : Cone (F.flip.obj k₂) },
                  map_id := ⋯, map_comp := ⋯ : Functor.{v₂, v, u₂, u} K C })
              g ≫
            { app := fun (k : K) ↦ (c k).cone.π.app j₂, naturality := ⋯ :
              NatTrans
                (obj
                  (obj (const J)
                    { obj := fun (k : K) ↦ (c k).cone.pt,
                      map := fun {k₁ k₂ : K} (f : k₁ ⟶ k₂) ↦
                        (c k₂).isLimit.lift
                          { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map f : Cone (F.flip.obj k₂) },
                      map_id := ⋯, map_comp := ⋯ : Functor.{v₂, v, u₂, u} K C })
                  j₂)
                (F.obj j₂) }).app
        k =
      NatTrans.app
        ({ app := fun (k : K) ↦ (c k).cone.π.app j₁, naturality := ⋯ :
            NatTrans
              (obj
                (obj (const J)
                  { obj := fun (k : K) ↦ (c k).cone.pt,
                    map := fun {k₁ k₂ : K} (f : k₁ ⟶ k₂) ↦
                      (c k₂).isLimit.lift
                        { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map f : Cone (F.flip.obj k₂) },
                    map_id := ⋯, map_comp := ⋯ : Functor.{v₂, v, u₂, u} K C })
                j₁)
              (F.obj j₁) } ≫
          F.map g)
        k
⊢ map
        (obj (const J)
          { obj := fun (k : K) ↦ (c k).cone.pt,
            map := fun {k₁ k₂ : K} (f : k₁ ⟶ k₂) ↦
              (c k₂).isLimit.lift { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map f : Cone (F.flip.obj k₂) },
            map_id := ⋯, map_comp := ⋯ : Functor.{v₂, v, u₂, u} K C })
        g ≫
      { app := fun (k : K) ↦ (c k).cone.π.app j₂, naturality := ⋯ :
        NatTrans
          (obj
            (obj (const J)
              { obj := fun (k : K) ↦ (c k).cone.pt,
                map := fun {k₁ k₂ : K} (f : k₁ ⟶ k₂) ↦
                  (c k₂).isLimit.lift
                    { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map f : Cone (F.flip.obj k₂) },
                map_id := ⋯, map_comp := ⋯ : Functor.{v₂, v, u₂, u} K C })
            j₂)
          (F.obj j₂) } =
    { app := fun (k : K) ↦ (c k).cone.π.app j₁, naturality := ⋯ :
        NatTrans
          (obj
            (obj (const J)
              { obj := fun (k : K) ↦ (c k).cone.pt,
                map := fun {k₁ k₂ : K} (f : k₁ ⟶ k₂) ↦
                  (c k₂).isLimit.lift
                    { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map f : Cone (F.flip.obj k₂) },
                map_id := ⋯, map_comp := ⋯ : Functor.{v₂, v, u₂, u} K C })
            j₁)
          (F.obj j₁) } ≫
      F.map g

Tactic:
ext k