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
⊢ ((mateEquiv h h)
            (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:
unfold mateEquiv

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
⊢ ({
              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