Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
L : D ⥤ C
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)))
        ((mateEquiv h h)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A))))).natTrans =
    (conjugateEquiv (h.comp (ihom.adjunction A)) ((ihom.adjunction (F.obj A)).comp h))
      (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A)))
B : C
⊢ ({
              toFun := fun α ↦
                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 ((tensorLeft (F.obj A)).associator L F).inv ≫
                          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.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 := ⋯ }
            (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A)))).natTrans.app
      B =
    (natTrans (prodComparisonNatIso F A).inv).app 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]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
L : D ⥤ C
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)))
        ((mateEquiv h h)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A))))).natTrans =
    (conjugateEquiv (h.comp (ihom.adjunction A)) ((ihom.adjunction (F.obj A)).comp h))
      (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A)))
B : C
⊢ h.unit.app (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)