-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F G G' : Functor.{v₁, v₂, u₁, u₂} C V
η : G ⟶ G'
c c' : C
f : c ⟶ c'
⊢ Eq (α :=
    Quiver.Hom (V := Cᵒᵖ ⥤ Functor.{v₁, v₂, u₁, u₂} C V)
      (Functor.obj
        {
          obj := fun (c : C) ↦
            Functor.obj (Functor.obj (Functor.obj (Functor.whiskeringLeft₂ V) F.op) (tensorRight c ⋙ G))
              MonoidalClosed.internalHom,
          map := fun {c c' : C} (f : c ⟶ c') ↦
            NatTrans.app
              (Functor.map (Functor.obj (Functor.whiskeringLeft₂ V) F.op)
                (Functor.whiskerRight (Functor.map (Functor.flip (curriedTensor C)) f) G))
              MonoidalClosed.internalHom,
          map_id := ⋯, map_comp := ⋯ }
        c)
      (Functor.obj
        {
          obj := fun (c : C) ↦
            Functor.obj (Functor.obj (Functor.obj (Functor.whiskeringLeft₂ V) F.op) (tensorRight c ⋙ G'))
              MonoidalClosed.internalHom,
          map := fun {c c' : C} (f : c ⟶ c') ↦
            NatTrans.app
              (Functor.map (Functor.obj (Functor.whiskeringLeft₂ V) F.op)
                (Functor.whiskerRight (Functor.map (Functor.flip (curriedTensor C)) f) G'))
              MonoidalClosed.internalHom,
          map_id := ⋯, map_comp := ⋯ }
        c'))
    (Functor.map
        {
          obj := fun (c : C) ↦
            Functor.obj (Functor.obj (Functor.obj (Functor.whiskeringLeft₂ V) F.op) (tensorRight c ⋙ G))
              MonoidalClosed.internalHom,
          map := fun {c c' : C} (f : c ⟶ c') ↦
            NatTrans.app
              (Functor.map (Functor.obj (Functor.whiskeringLeft₂ V) F.op)
                (Functor.whiskerRight (Functor.map (Functor.flip (curriedTensor C)) f) G))
              MonoidalClosed.internalHom,
          map_id := ⋯, map_comp := ⋯ : C ⥤ Cᵒᵖ ⥤ Functor.{v₁, v₂, u₁, u₂} C V }
        f ≫
      NatTrans.app (Functor.map (Functor.obj (Functor.whiskeringLeft₂ V) F.op) (Functor.whiskerLeft (tensorRight c') η))
        MonoidalClosed.internalHom)
    (NatTrans.app (Functor.map (Functor.obj (Functor.whiskeringLeft₂ V) F.op) (Functor.whiskerLeft (tensorRight c) η))
        MonoidalClosed.internalHom ≫
      Functor.map
        {
          obj := fun (c : C) ↦
            Functor.obj (Functor.obj (Functor.obj (Functor.whiskeringLeft₂ V) F.op) (tensorRight c ⋙ G'))
              MonoidalClosed.internalHom,
          map := fun {c c' : C} (f : c ⟶ c') ↦
            NatTrans.app
              (Functor.map (Functor.obj (Functor.whiskeringLeft₂ V) F.op)
                (Functor.whiskerRight (Functor.map (Functor.flip (curriedTensor C)) f) G'))
              MonoidalClosed.internalHom,
          map_id := ⋯, map_comp := ⋯ : C ⥤ Cᵒᵖ ⥤ Functor.{v₁, v₂, u₁, u₂} C V }
        f)
have w : ∀ (j : Cᵒᵖ) (k : C),
  Eq (α :=
    Quiver.Hom.{v₂, u₂} (V := V)
      (Functor.obj.{v₁, v₂, u₁, u₂}
        (Functor.obj
          (Functor.obj
            {
              obj := fun (c : C) ↦
                Functor.obj (Functor.obj (Functor.obj (Functor.whiskeringLeft₂ V) F.op) (tensorRight c ⋙ G))
                  MonoidalClosed.internalHom,
              map := fun {c c' : C} (f : c ⟶ c') ↦
                NatTrans.app
                  (Functor.map (Functor.obj (Functor.whiskeringLeft₂ V) F.op)
                    (Functor.whiskerRight (Functor.map (Functor.flip (curriedTensor C)) f) G))
                  MonoidalClosed.internalHom,
              map_id := sorry, map_comp := sorry }
            c)
          j)
        k)
      (Functor.obj.{v₁, v₂, u₁, u₂}
        (Functor.obj
          (Functor.obj
            {
              obj := fun (c : C) ↦
                Functor.obj (Functor.obj (Functor.obj (Functor.whiskeringLeft₂ V) F.op) (tensorRight c ⋙ G'))
                  MonoidalClosed.internalHom,
              map := fun {c c' : C} (f : c ⟶ c') ↦
                NatTrans.app
                  (Functor.map (Functor.obj (Functor.whiskeringLeft₂ V) F.op)
                    (Functor.whiskerRight (Functor.map (Functor.flip (curriedTensor C)) f) G'))
                  MonoidalClosed.internalHom,
              map_id := sorry, map_comp := sorry }
            c')
          j)
        k))
    (NatTrans.app
        (NatTrans.app
          (Functor.map
              {
                obj := fun (c : C) ↦
                  Functor.obj (Functor.obj (Functor.obj (Functor.whiskeringLeft₂ V) F.op) (tensorRight c ⋙ G))
                    MonoidalClosed.internalHom,
                map := fun {c c' : C} (f : c ⟶ c') ↦
                  NatTrans.app
                    (Functor.map (Functor.obj (Functor.whiskeringLeft₂ V) F.op)
                      (Functor.whiskerRight (Functor.map (Functor.flip (curriedTensor C)) f) G))
                    MonoidalClosed.internalHom,
                map_id := sorry, map_comp := sorry : C ⥤ Cᵒᵖ ⥤ Functor.{v₁, v₂, u₁, u₂} C V }
              f ≫
            NatTrans.app
              (Functor.map (Functor.obj (Functor.whiskeringLeft₂ V) F.op) (Functor.whiskerLeft (tensorRight c') η))
              MonoidalClosed.internalHom)
          j)
        k :
      Quiver.Hom.{v₂, u₂} (V := V)
        (Functor.obj.{v₁, v₂, u₁, u₂}
          (Functor.obj
            (Functor.obj
              {
                obj := fun (c : C) ↦
                  Functor.obj (Functor.obj (Functor.obj (Functor.whiskeringLeft₂ V) F.op) (tensorRight c ⋙ G))
                    MonoidalClosed.internalHom,
                map := fun {c c' : C} (f : c ⟶ c') ↦
                  NatTrans.app
                    (Functor.map (Functor.obj (Functor.whiskeringLeft₂ V) F.op)
                      (Functor.whiskerRight (Functor.map (Functor.flip (curriedTensor C)) f) G))
                    MonoidalClosed.internalHom,
                map_id := sorry, map_comp := sorry }
              c)
            j)
          k)
        (Functor.obj.{v₁, v₂, u₁, u₂}
          (Functor.obj
            (Functor.obj
              {
                obj := fun (c : C) ↦
                  Functor.obj (Functor.obj (Functor.obj (Functor.whiskeringLeft₂ V) F.op) (tensorRight c ⋙ G'))
                    MonoidalClosed.internalHom,
                map := fun {c c' : C} (f : c ⟶ c') ↦
                  NatTrans.app
                    (Functor.map (Functor.obj (Functor.whiskeringLeft₂ V) F.op)
                      (Functor.whiskerRight (Functor.map (Functor.flip (curriedTensor C)) f) G'))
                    MonoidalClosed.internalHom,
                map_id := sorry, map_comp := sorry }
              c')
            j)
          k))
    (NatTrans.app
        (NatTrans.app
          (NatTrans.app
              (Functor.map (Functor.obj (Functor.whiskeringLeft₂ V) F.op) (Functor.whiskerLeft (tensorRight c) η))
              MonoidalClosed.internalHom ≫
            Functor.map
              {
                obj := fun (c : C) ↦
                  Functor.obj (Functor.obj (Functor.obj (Functor.whiskeringLeft₂ V) F.op) (tensorRight c ⋙ G'))
                    MonoidalClosed.internalHom,
                map := fun {c c' : C} (f : c ⟶ c') ↦
                  NatTrans.app
                    (Functor.map (Functor.obj (Functor.whiskeringLeft₂ V) F.op)
                      (Functor.whiskerRight (Functor.map (Functor.flip (curriedTensor C)) f) G'))
                    MonoidalClosed.internalHom,
                map_id := sorry, map_comp := sorry : C ⥤ Cᵒᵖ ⥤ Functor.{v₁, v₂, u₁, u₂} C V }
              f)
          j)
        k :
      Quiver.Hom.{v₂, u₂} (V := V)
        (Functor.obj.{v₁, v₂, u₁, u₂}
          (Functor.obj
            (Functor.obj
              {
                obj := fun (c : C) ↦
                  Functor.obj (Functor.obj (Functor.obj (Functor.whiskeringLeft₂ V) F.op) (tensorRight c ⋙ G))
                    MonoidalClosed.internalHom,
                map := fun {c c' : C} (f : c ⟶ c') ↦
                  NatTrans.app
                    (Functor.map (Functor.obj (Functor.whiskeringLeft₂ V) F.op)
                      (Functor.whiskerRight (Functor.map (Functor.flip (curriedTensor C)) f) G))
                    MonoidalClosed.internalHom,
                map_id := sorry, map_comp := sorry }
              c)
            j)
          k)
        (Functor.obj.{v₁, v₂, u₁, u₂}
          (Functor.obj
            (Functor.obj
              {
                obj := fun (c : C) ↦
                  Functor.obj (Functor.obj (Functor.obj (Functor.whiskeringLeft₂ V) F.op) (tensorRight c ⋙ G'))
                    MonoidalClosed.internalHom,
                map := fun {c c' : C} (f : c ⟶ c') ↦
                  NatTrans.app
                    (Functor.map (Functor.obj (Functor.whiskeringLeft₂ V) F.op)
                      (Functor.whiskerRight (Functor.map (Functor.flip (curriedTensor C)) f) G'))
                    MonoidalClosed.internalHom,
                map_id := sorry, map_comp := sorry }
              c')
            j)
          k))
Tactic: ext j k