-- Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
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'
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 := ⋯, map_comp := ⋯ }
              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 := ⋯, map_comp := ⋯ }
              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 := ⋯, 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)
            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 := ⋯, map_comp := ⋯ }
                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 := ⋯, map_comp := ⋯ }
                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 := ⋯, map_comp := ⋯ : 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 := ⋯, map_comp := ⋯ }
                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 := ⋯, map_comp := ⋯ }
                c')
              j)
            k))
⊢ 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)

Tactic:
ext j k