-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Functor (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A A' : C
f : A' ⟶ A
vcomp1 :
  Eq (α := TwoSquare (ihom A) F F (ihom (F.obj A')))
    ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A')) :
          (a : TwoSquare F (tensorLeft A) (tensorLeft (F.obj A')) F) → TwoSquare (ihom A) F F (ihom (F.obj A')))
        (TwoSquare.whiskerRight (Iso.inv (prodComparisonNatIso F A)) (Functor.map (curriedTensor D) (F.map f))) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
    (TwoSquare.whiskerBottom (B := ihom (F.obj A))
        ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)) :
            (a : TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F) → TwoSquare (ihom A) F F (ihom (F.obj A)))
          (Iso.inv (prodComparisonNatIso F A)))
        ((conjugateEquiv (ihom.adjunction (F.obj A)) (ihom.adjunction (F.obj A')) :
            (a : tensorLeft (F.obj A') ⟶ tensorLeft (F.obj A)) → ihom (F.obj A) ⟶ ihom (F.obj A'))
          (Functor.map (curriedTensor D) (F.map f))) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
vcomp2 :
  Eq (α := TwoSquare (ihom A) F F (ihom (F.obj A')))
    ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A')) :
          (a : TwoSquare F (tensorLeft A) (tensorLeft (F.obj A')) F) → TwoSquare (ihom A) F F (ihom (F.obj A')))
        (TwoSquare.whiskerLeft (Iso.inv (prodComparisonNatIso F A')) (Functor.map (curriedTensor C) f)) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
    (TwoSquare.whiskerTop (T' := ihom A')
        ((mateEquiv (ihom.adjunction A') (ihom.adjunction (F.obj A')) :
            (a : TwoSquare F (tensorLeft A') (tensorLeft (F.obj A')) F) → TwoSquare (ihom A') F F (ihom (F.obj A')))
          (Iso.inv (prodComparisonNatIso F A')))
        ((conjugateEquiv (ihom.adjunction A) (ihom.adjunction A') :
            (a : tensorLeft A' ⟶ tensorLeft A) → ihom A ⟶ ihom A')
          (Functor.map (curriedTensor C) f)) :
      TwoSquare (ihom A) F F (ihom (F.obj A')))
B : C
⊢ Eq (α := (F ⋙ tensorLeft (F.obj A')).obj B ⟶ (tensorLeft A ⋙ F).obj B)
    (NatTrans.app
      (F.whiskerLeft (Functor.map (curriedTensor D) (F.map f)) ≫ natTrans (Iso.inv (prodComparisonNatIso F A))) B)
    (NatTrans.app
      (natTrans (Iso.inv (prodComparisonNatIso F A')) ≫ Functor.whiskerRight (Functor.map (curriedTensor C) f) F) B)
have h : Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A' B) ⟶ F.obj (tensorObj.{v, u} (𝒞 := inst) A B))
  (CategoryStruct.comp (Y := tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A') (F.obj B)) (prodComparison F A' B)
    (F.map f ▷ F.obj B ≫ inv (prodComparison F A B)))
  (F.map (f ▷ B))
Tactic: simp only [Functor.comp_obj, curriedTensor_obj_obj, prodComparisonNatIso_inv,
    NatTrans.comp_app, Functor.whiskerLeft_app, curriedTensor_map_app, NatIso.isIso_inv_app,
    Functor.whiskerRight_app, IsIso.eq_inv_comp, prodComparisonNatTrans_app]