-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
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₂
⊢ 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
have 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 := sorry, map_comp := sorry : Functor.{v₂, v, u₂, u} K C })
            g ≫
          { app := fun (k : K) ↦ (c k).cone.π.app j₂, naturality := sorry :
            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 := sorry, map_comp := sorry : 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 := sorry :
          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 := sorry, map_comp := sorry : Functor.{v₂, v, u₂, u} K C })
              j₁)
            (F.obj j₁) } ≫
        F.map g)
      k
Tactic: ext k