-- Mathlib/CategoryTheory/Closed/Functor.lean
theorem frobeniusMorphism_mate (h : L ⊣ F) (A : C) :
    conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h)
        (frobeniusMorphism F h A).natTrans = (expComparison F A).natTrans

Proof state:
case e_w.h.h.inv_hom_id
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  ((mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A)))
        ((mateEquiv h h)
          (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L ((curriedTensor C).map (h.counit.app A))))).natTrans =
    (conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h))
      (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L ((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)) ≫
        prodComparison F (L.obj (F.obj A)) (L.obj (F.obj B)) ≫
          F.map (h.counit.app A) ▷ F.obj (L.obj (F.obj B)) ≫ F.obj A ◁ F.map (h.counit.app B) =
    𝟙 (F.obj A ⊗ F.obj B)

Tactic:
slice_lhs 2 3 => rw [← prodComparison_comp]

Result:
case e_w.h.h.inv_hom_id
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  ((mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A)))
        ((mateEquiv h h)
          (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L ((curriedTensor C).map (h.counit.app A))))).natTrans =
    (conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h))
      (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L ((curriedTensor C).map (h.counit.app A)))
B : C
⊢ h.unit.app (F.obj A ⊗ F.obj B) ≫
      (prodComparison (L ⋙ F) (F.obj A) (F.obj B) ≫ F.map (h.counit.app A) ▷ F.obj (L.obj (F.obj B))) ≫
        F.obj A ◁ F.map (h.counit.app B) =
    𝟙 (F.obj A ⊗ F.obj B)

Proof state:
case e_w.h.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  ((mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A)))
        ((mateEquiv h h)
          (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L ((curriedTensor C).map (h.counit.app A))))).natTrans =
    (conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h))
      (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L ((curriedTensor C).map (h.counit.app A)))
B : C
⊢ ({
              toFun := fun α =>
                TwoSquare.mk F (tensorLeft A) (tensorLeft (F.obj A)) F
                  (whiskerLeft (F ⋙ tensorLeft (F.obj A)) h.unit ≫
                    whiskerRight (whiskerLeft F α.natTrans) F ≫ whiskerRight h.counit (tensorLeft A ⋙ F)),
              invFun := fun β =>
                TwoSquare.mk (tensorLeft (F.obj A)) L L (tensorLeft A)
                  (whiskerRight h.unit (tensorLeft (F.obj A) ⋙ L) ≫
                    whiskerRight (whiskerLeft L β.natTrans) L ≫ whiskerLeft (L ⋙ tensorLeft A) h.counit),
              left_inv := ⋯, right_inv := ⋯ }
            (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L ((curriedTensor C).map (h.counit.app A)))).natTrans.app
      B =
    (natTrans (prodComparisonNatIso F A).inv).app B

Tactic:
simp only [Functor.comp_obj, tensorLeft_obj, Functor.id_obj, Equiv.coe_fn_mk, whiskerLeft_comp,
  whiskerLeft_twice, whiskerRight_comp, assoc, NatTrans.comp_app, whiskerLeft_app,
  curriedTensor_obj_obj, whiskerRight_app, prodComparisonNatTrans_app, curriedTensor_map_app,
  Functor.comp_map, tensorLeft_map, prodComparisonNatIso_inv, asIso_inv, NatIso.isIso_inv_app]

Result:
case e_w.h.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  ((mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A)))
        ((mateEquiv h h)
          (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L ((curriedTensor C).map (h.counit.app A))))).natTrans =
    (conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h))
      (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L ((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)

Proof state:
case e_w.h.h.inv_hom_id
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  ((mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A)))
        ((mateEquiv h h)
          (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L ((curriedTensor C).map (h.counit.app A))))).natTrans =
    (conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h))
      (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L ((curriedTensor C).map (h.counit.app A)))
B : C
ηlemma :
  h.unit.app (F.obj A ⊗ F.obj B) ≫
      lift ((L ⋙ F).map (fst (F.obj A) (F.obj B))) ((L ⋙ F).map (snd (F.obj A) (F.obj B))) =
    h.unit.app (F.obj A) ⊗ h.unit.app (F.obj B)
⊢ h.unit.app (F.obj A ⊗ F.obj B) ≫
      lift ((L ⋙ F).map (fst (F.obj A) (F.obj B))) ((L ⋙ F).map (snd (F.obj A) (F.obj B))) ≫
        F.map (h.counit.app A) ▷ F.obj (L.obj (F.obj B)) ≫ F.obj A ◁ F.map (h.counit.app B) =
    𝟙 (F.obj A ⊗ F.obj B)

Tactic:
slice_lhs 1 2 => rw [ηlemma]

Result:
case e_w.h.h.inv_hom_id
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  ((mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A)))
        ((mateEquiv h h)
          (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L ((curriedTensor C).map (h.counit.app A))))).natTrans =
    (conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h))
      (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L ((curriedTensor C).map (h.counit.app A)))
B : C
ηlemma :
  h.unit.app (F.obj A ⊗ F.obj B) ≫
      lift ((L ⋙ F).map (fst (F.obj A) (F.obj B))) ((L ⋙ F).map (snd (F.obj A) (F.obj B))) =
    h.unit.app (F.obj A) ⊗ h.unit.app (F.obj B)
⊢ ((h.unit.app (F.obj A) ⊗ h.unit.app (F.obj B)) ≫ F.map (h.counit.app A) ▷ F.obj (L.obj (F.obj B))) ≫
      F.obj A ◁ F.map (h.counit.app B) =
    𝟙 (F.obj A ⊗ F.obj B)