-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
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
L : Functor.{v, v, u', u} D C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  Eq (α := ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
    (natTrans
      ((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)))
        ((mateEquiv h h :
            (a : TwoSquare (tensorLeft (F.obj A)) L L (tensorLeft A)) →
              TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))))
    ((conjugateEquiv (h.comp (ihom.adjunction A)) (Adjunction.comp (ihom.adjunction (F.obj A)) h) :
        (a : tensorLeft (F.obj A) ⋙ L ⟶ L ⋙ tensorLeft A) → ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
      (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A))))
B : C
e_w :
  Eq (α := tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B) ⟶ F.obj (tensorObj.{v, u} (𝒞 := inst) A B))
    (h.unit.app (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj B)) ≫
      F.map (prodComparison L (F.obj A) (F.obj B)) ≫
        F.map (h.counit.app A ▷ L.obj (F.obj B)) ≫ F.map (A ◁ h.counit.app B))
    (inv (prodComparison F A B))
⊢ Eq (α := (F ⋙ tensorLeft (F.obj A)).obj B ⟶ (tensorLeft A ⋙ F).obj B)
    (NatTrans.app
      (natTrans
        (({
              toFun := fun (α : TwoSquare (tensorLeft (F.obj A)) L L (tensorLeft A)) ↦
                TwoSquare.mk F (tensorLeft A) (tensorLeft (F.obj A)) F
                  ((F ⋙ tensorLeft (F.obj A)).rightUnitor.inv ≫
                    (F ⋙ tensorLeft (F.obj A)).whiskerLeft h.unit ≫
                      (F.associator (tensorLeft (F.obj A)) (L ⋙ F)).hom ≫
                        F.whiskerLeft (Iso.inv (Functor.associator (tensorLeft (F.obj A)) L F)) ≫
                          F.whiskerLeft (Functor.whiskerRight α.natTrans F) ≫
                            F.whiskerLeft (L.associator (tensorLeft A) F).hom ≫
                              (F.associator L (tensorLeft A ⋙ F)).inv ≫
                                Functor.whiskerRight h.counit (tensorLeft A ⋙ F) ≫ (tensorLeft A ⋙ F).leftUnitor.hom),
              invFun := fun (β : TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F) ↦
                TwoSquare.mk (tensorLeft (F.obj A)) L L (tensorLeft A)
                  ((tensorLeft (F.obj A) ⋙ L).leftUnitor.inv ≫
                    Functor.whiskerRight h.unit (tensorLeft (F.obj A) ⋙ L) ≫
                      ((L ⋙ F).associator (tensorLeft (F.obj A)) L).inv ≫
                        Functor.whiskerRight (L.associator F (tensorLeft (F.obj A))).hom L ≫
                          Functor.whiskerRight (L.whiskerLeft β.natTrans) L ≫
                            Functor.whiskerRight (L.associator (tensorLeft A) F).inv L ≫
                              ((L ⋙ tensorLeft A).associator F L).hom ≫
                                (L ⋙ tensorLeft A).whiskerLeft h.counit ≫ (L ⋙ tensorLeft A).rightUnitor.hom),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : TwoSquare (tensorLeft (F.obj A)) L L (tensorLeft A)) →
              TwoSquare F (tensorLeft A) (tensorLeft (F.obj A)) F)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft (Functor.map (curriedTensor C) (h.counit.app A)))))
      B)
    (NatTrans.app (natTrans (Iso.inv (prodComparisonNatIso F A))) B)

Tactic:
simp only [Functor.comp_obj, curriedTensor_obj_obj, Equiv.coe_fn_mk, Functor.whiskerRight_comp,
    Functor.whiskerLeft_comp, Category.assoc, NatTrans.comp_app, Functor.id_obj,
    Functor.rightUnitor_inv_app, Functor.whiskerLeft_app, Functor.associator_hom_app,
    Functor.associator_inv_app, Functor.whiskerRight_app, prodComparisonNatTrans_app,
    curriedTensor_map_app, Functor.comp_map, curriedTensor_obj_map, Functor.leftUnitor_hom_app,
    Category.comp_id, Category.id_comp, prodComparisonNatIso_inv, NatIso.isIso_inv_app]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.associator_hom_app, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Functor.associator_inv_app, CategoryTheory.Functor.whiskerLeft_comp, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategory.curriedTensor_obj_map, CategoryTheory.CartesianMonoidalCategory.prodComparisonNatIso_inv, CategoryTheory.MonoidalCategory.curriedTensor_obj_obj, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.whiskerRight_app, Equiv.coe_fn_mk, CategoryTheory.MonoidalCategory.curriedTensor_map_app, CategoryTheory.Functor.whiskerRight_comp, CategoryTheory.NatIso.isIso_inv_app, CategoryTheory.NatTrans.comp_app, CategoryTheory.Functor.rightUnitor_inv_app, CategoryTheory.Functor.leftUnitor_hom_app, CategoryTheory.Functor.comp_map, CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans_app, CategoryTheory.Category.id_comp