-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic (goal)
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))
⊢ 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)))
have 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))
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]