-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : MonoidalClosed.{v₁, u₁} C
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : Functor.{v₂, v₁, u₂, u₁} J C
f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃
j : J
k₁ k₂ : Under.{v₂, u₂} j
φ : k₁ ⟶ k₂
rw :
  Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
    (curry (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ f.app k₁.right) ≫
      Functor.map (ihom (F₁.obj k₁.right)) (F₃.map (Under.Hom.right φ)))
    (F₂.map k₂.hom ≫
      CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₂.right)) (F₃.obj k₂.right))
        (curry (f.app k₂.right)) (NatTrans.app (pre (F₁.map (Under.Hom.right φ))) (F₃.obj k₂.right)))
rw₁ :
  Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
    (curry (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ f.app k₁.right) ≫
      Functor.map (ihom (F₁.obj k₁.right)) (F₃.map (Under.Hom.right φ)))
    (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₂.right)) (F₃.obj k₂.right))
      (curry (F₁.obj k₂.right ◁ F₂.map k₂.hom ≫ f.app k₂.right))
      (NatTrans.app (pre (F₁.map (Under.Hom.right φ))) (F₃.obj k₂.right)))
rw₂ :
  Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
    (curry ((F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ f.app k₁.right) ≫ F₃.map (Under.Hom.right φ)))
    (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₂.right)) (F₃.obj k₂.right))
      (curry (F₁.obj k₂.right ◁ F₂.map k₂.hom ≫ f.app k₂.right))
      (NatTrans.app (pre (F₁.map (Under.Hom.right φ))) (F₃.obj k₂.right)))
rw₃ :
  Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
    (curry ((F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ f.app k₁.right) ≫ F₃.map (Under.Hom.right φ)))
    (curry (F₁.map (Under.Hom.right φ) ▷ F₂.obj j ≫ F₁.obj k₂.right ◁ F₂.map k₂.hom ≫ f.app k₂.right))
rw₄ :
  Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
    (curry (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ f.app k₁.right ≫ F₃.map (Under.Hom.right φ)))
    (curry (F₁.map (Under.Hom.right φ) ▷ F₂.obj j ≫ F₁.obj k₂.right ◁ F₂.map k₂.hom ≫ f.app k₂.right))
rw₅ :
  Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
    (curry
      (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫
        (tensorObj (𝒞 := Functor.category) F₁ F₂).map (Under.Hom.right φ) ≫ f.app k₂.right))
    (curry (F₁.map (Under.Hom.right φ) ▷ F₂.obj j ≫ F₁.obj k₂.right ◁ F₂.map k₂.hom ≫ f.app k₂.right))
rw₆ :
  Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
    (curry
      (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ (F₁.map (Under.Hom.right φ) ⊗ₘ F₂.map (Under.Hom.right φ)) ≫ f.app k₂.right))
    (curry (F₁.map (Under.Hom.right φ) ▷ F₂.obj j ≫ F₁.obj k₂.right ◁ F₂.map k₂.hom ≫ f.app k₂.right))
rw₇ :
  Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
    (curry
      (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫
        F₁.map (Under.Hom.right φ) ▷ F₂.obj k₁.right ≫ F₁.obj k₂.right ◁ F₂.map (Under.Hom.right φ) ≫ f.app k₂.right))
    (curry (F₁.map (Under.Hom.right φ) ▷ F₂.obj j ≫ F₁.obj k₂.right ◁ F₂.map k₂.hom ≫ f.app k₂.right))
rw₈ :
  Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
    (curry
      (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫
        F₁.map (Under.Hom.right φ) ▷ F₂.obj k₁.right ≫ F₁.obj k₂.right ◁ F₂.map (Under.Hom.right φ) ≫ f.app k₂.right))
    (curry
      (F₁.map (Under.Hom.right φ) ▷ F₂.obj j ≫ F₁.obj k₂.right ◁ F₂.map (k₁.hom ≫ Under.Hom.right φ) ≫ f.app k₂.right))
rw₉ :
  Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
    (curry
      (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫
        F₁.map (Under.Hom.right φ) ▷ F₂.obj k₁.right ≫ F₁.obj k₂.right ◁ F₂.map (Under.Hom.right φ) ≫ f.app k₂.right))
    (curry
      (F₁.map (Under.Hom.right φ) ▷ F₂.obj j ≫
        F₁.obj k₂.right ◁ (F₂.map k₁.hom ≫ F₂.map (Under.Hom.right φ)) ≫ f.app k₂.right))
rw₁₀ :
  Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
    (curry
      (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫
        F₁.map (Under.Hom.right φ) ▷ F₂.obj k₁.right ≫ F₁.obj k₂.right ◁ F₂.map (Under.Hom.right φ) ≫ f.app k₂.right))
    (curry
      (F₁.map (Under.Hom.right φ) ▷ F₂.obj j ≫
        F₁.obj k₂.right ◁ F₂.map k₁.hom ≫ F₁.obj k₂.right ◁ F₂.map (Under.Hom.right φ) ≫ f.app k₂.right))
rw₁₁ rw₁₂ :
  Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
    (curry
      (F₁.map (Under.Hom.right φ) ▷ F₂.obj j ≫
        F₁.obj k₂.right ◁ F₂.map k₁.hom ≫ F₁.obj k₂.right ◁ F₂.map (Under.Hom.right φ) ≫ f.app k₂.right))
    (curry
      (F₁.map (Under.Hom.right φ) ▷ F₂.obj j ≫
        F₁.obj k₂.right ◁ F₂.map k₁.hom ≫ F₁.obj k₂.right ◁ F₂.map (Under.Hom.right φ) ≫ f.app k₂.right))
⊢ Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
    (F₂.map k₁.hom ≫ curry (f.app k₁.right) ≫ Functor.map (ihom (F₁.obj k₁.right)) (F₃.map (Under.Hom.right φ)))
    (F₂.map k₂.hom ≫
      CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₂.right)) (F₃.obj k₂.right))
        (curry (f.app k₂.right)) (NatTrans.app (pre (F₁.map (Under.Hom.right φ))) (F₃.obj k₂.right)))

Tactic:
rw [← curry_natural_left_assoc, ← curry_natural_left_assoc,
            ← curry_natural_right, curry_pre_app, Category.assoc,
            ← f.naturality φ.right, Monoidal.tensorObj_map, tensorHom_def_assoc,
            ← Under.w φ, Functor.map_comp, MonoidalCategory.whiskerLeft_comp_assoc,
            whisker_exchange_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalClosed.curry_pre_app, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalClosed.curry_natural_left_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.NatTrans.naturality, CategoryTheory.Under.Hom.right, CategoryTheory.Functor.map_comp, CategoryTheory.MonoidalCategory.tensorHom_def_assoc, CategoryTheory.Monoidal.tensorObj_map, CategoryTheory.MonoidalClosed.curry_natural_right, CategoryTheory.Under.w