-- 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'
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))
have w : Eq (α :=
  Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj (unop j))) (G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) k c)) ⟶
    Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj (unop j))) (G'.obj (tensorObj.{v₁, u₁} (𝒞 := inst) k c')))
  (Functor.map (ihom (F.obj (unop j))) (G.map (k ◁ f)) ≫
    Functor.map (ihom (F.obj (unop j))) (η.app (tensorObj.{v₁, u₁} (𝒞 := inst) k c')))
  (Functor.map (ihom (F.obj (unop j))) (η.app (tensorObj.{v₁, u₁} (𝒞 := inst) k c)) ≫
    Functor.map (ihom (F.obj (unop j))) (G'.map (k ◁ f)))
Tactic: dsimp