[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
h : L ⊣ F
A : C
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) L
inst✝¹ : Full F
inst✝ : Faithful F
B : D
⊢ IsIso (NatTrans.app (frobeniusMorphism F h A) B)
[PROOFSTEP]
dsimp [frobeniusMorphism]
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
h : L ⊣ F
A : C
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) L
inst✝¹ : Full F
inst✝ : Faithful F
B : D
⊢ IsIso (prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B)))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A B : C
⊢ prod.map (𝟙 (F.obj A)) (NatTrans.app (expComparison F A) B) ≫ NatTrans.app (exp.ev (F.obj A)) (F.obj B) =
    inv (prodComparison F A (A ⟹ B)) ≫ F.map (NatTrans.app (exp.ev A) B)
[PROOFSTEP]
convert transferNatTrans_counit _ _ (prodComparisonNatIso F A).inv B using 2
[GOAL]
case h.e'_3.h.h.e'_6.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A B : C
e_1✝ :
  (F.obj A ⨯ (exp A ⋙ F).obj B ⟶ (𝟭 D).obj (F.obj B)) =
    ((prod.functor.obj (F.obj A)).obj ((exp A ⋙ F).obj B) ⟶ (𝟭 D).obj (F.obj B))
e_3✝ : (F.obj A ⨯ F.obj (A ⟹ B)) = (F ⋙ prod.functor.obj (F.obj A)).obj (A ⟹ B)
e_4✝ : F.obj (A ⨯ A ⟹ B) = (prod.functor.obj A ⋙ F).obj (A ⟹ B)
⊢ inv (prodComparison F A (A ⟹ B)) = NatTrans.app (prodComparisonNatIso F A).inv (A ⟹ B)
[PROOFSTEP]
apply IsIso.inv_eq_of_hom_inv_id
[GOAL]
case h.e'_3.h.h.e'_6.h.hom_inv_id
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A B : C
e_1✝ :
  (F.obj A ⨯ (exp A ⋙ F).obj B ⟶ (𝟭 D).obj (F.obj B)) =
    ((prod.functor.obj (F.obj A)).obj ((exp A ⋙ F).obj B) ⟶ (𝟭 D).obj (F.obj B))
e_3✝ : (F.obj A ⨯ F.obj (A ⟹ B)) = (F ⋙ prod.functor.obj (F.obj A)).obj (A ⟹ B)
e_4✝ : F.obj (A ⨯ A ⟹ B) = (prod.functor.obj A ⋙ F).obj (A ⟹ B)
⊢ prodComparison F A (A ⟹ B) ≫ NatTrans.app (prodComparisonNatIso F A).inv (A ⟹ B) = 𝟙 (F.obj (A ⨯ A ⟹ B))
[PROOFSTEP]
simp only [Limits.prodComparisonNatIso_inv, asIso_inv, NatIso.isIso_inv_app, IsIso.hom_inv_id]
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A B : C
⊢ F.map (NatTrans.app (exp.coev A) B) ≫ NatTrans.app (expComparison F A) (A ⨯ B) =
    NatTrans.app (exp.coev (F.obj A)) (F.obj B) ≫ (exp (F.obj A)).map (inv (prodComparison F A B))
[PROOFSTEP]
convert unit_transferNatTrans _ _ (prodComparisonNatIso F A).inv B using 3
[GOAL]
case h.e'_3.h.h.e'_7.h.h.e'_8.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A B : C
e_1✝ :
  (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj (A ⨯ B)) =
    (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj ((prod.functor.obj A).obj B))
e_4✝ :
  (prod.functor.obj (F.obj A) ⋙ exp (F.obj A)).obj (F.obj B) =
    (prod.functor.obj (F.obj A) ⋙ exp (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_5✝ : (F.obj A ⟹ F.obj (A ⨯ B)) = (F.obj A ⟹ (prod.functor.obj A ⋙ F).obj ((𝟭 C).obj B))
e_6✝ : (prod.functor.obj (F.obj A)).obj (F.obj B) = (prod.functor.obj (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_7✝ : F.obj (A ⨯ B) = (prod.functor.obj A ⋙ F).obj ((𝟭 C).obj B)
⊢ inv (prodComparison F A B) = NatTrans.app (prodComparisonNatIso F A).inv ((𝟭 C).obj B)
[PROOFSTEP]
apply IsIso.inv_eq_of_hom_inv_id
[GOAL]
case h.e'_3.h.h.e'_7.h.h.e'_8.h.hom_inv_id
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A B : C
e_1✝ :
  (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj (A ⨯ B)) =
    (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj ((prod.functor.obj A).obj B))
e_4✝ :
  (prod.functor.obj (F.obj A) ⋙ exp (F.obj A)).obj (F.obj B) =
    (prod.functor.obj (F.obj A) ⋙ exp (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_5✝ : (F.obj A ⟹ F.obj (A ⨯ B)) = (F.obj A ⟹ (prod.functor.obj A ⋙ F).obj ((𝟭 C).obj B))
e_6✝ : (prod.functor.obj (F.obj A)).obj (F.obj B) = (prod.functor.obj (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_7✝ : F.obj (A ⨯ B) = (prod.functor.obj A ⋙ F).obj ((𝟭 C).obj B)
⊢ prodComparison F A B ≫ NatTrans.app (prodComparisonNatIso F A).inv ((𝟭 C).obj B) = 𝟙 (F.obj (A ⨯ B))
[PROOFSTEP]
dsimp
[GOAL]
case h.e'_3.h.h.e'_7.h.h.e'_8.h.hom_inv_id
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A B : C
e_1✝ :
  (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj (A ⨯ B)) =
    (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj ((prod.functor.obj A).obj B))
e_4✝ :
  (prod.functor.obj (F.obj A) ⋙ exp (F.obj A)).obj (F.obj B) =
    (prod.functor.obj (F.obj A) ⋙ exp (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_5✝ : (F.obj A ⟹ F.obj (A ⨯ B)) = (F.obj A ⟹ (prod.functor.obj A ⋙ F).obj ((𝟭 C).obj B))
e_6✝ : (prod.functor.obj (F.obj A)).obj (F.obj B) = (prod.functor.obj (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_7✝ : F.obj (A ⨯ B) = (prod.functor.obj A ⋙ F).obj ((𝟭 C).obj B)
⊢ prodComparison F A B ≫ NatTrans.app (inv (NatTrans.mk fun B => prodComparison F A B)) B = 𝟙 (F.obj (A ⨯ B))
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A B : C
⊢ CartesianClosed.uncurry (NatTrans.app (expComparison F A) B) =
    inv (prodComparison F A (A ⟹ B)) ≫ F.map (NatTrans.app (exp.ev A) B)
[PROOFSTEP]
rw [uncurry_eq, expComparison_ev]
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A A' : C
f : A' ⟶ A
⊢ expComparison F A ≫ whiskerLeft F (pre (F.map f)) = whiskerRight (pre f) F ≫ expComparison F A'
[PROOFSTEP]
ext B
[GOAL]
case w.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A A' : C
f : A' ⟶ A
B : C
⊢ NatTrans.app (expComparison F A ≫ whiskerLeft F (pre (F.map f))) B =
    NatTrans.app (whiskerRight (pre f) F ≫ expComparison F A') B
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A A' : C
f : A' ⟶ A
B : C
⊢ NatTrans.app (expComparison F A) B ≫ NatTrans.app (pre (F.map f)) (F.obj B) =
    F.map (NatTrans.app (pre f) B) ≫ NatTrans.app (expComparison F A') B
[PROOFSTEP]
apply uncurry_injective
[GOAL]
case w.h.a
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A A' : C
f : A' ⟶ A
B : C
⊢ CartesianClosed.uncurry (NatTrans.app (expComparison F A) B ≫ NatTrans.app (pre (F.map f)) (F.obj B)) =
    CartesianClosed.uncurry (F.map (NatTrans.app (pre f) B) ≫ NatTrans.app (expComparison F A') B)
[PROOFSTEP]
rw [uncurry_natural_left, uncurry_natural_left, uncurry_expComparison, uncurry_pre, prod.map_swap_assoc, ← F.map_id,
  expComparison_ev, ← F.map_id, ← prodComparison_inv_natural_assoc, ← prodComparison_inv_natural_assoc, ← F.map_comp, ←
  F.map_comp, prod_map_pre_app_comp_ev]
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
⊢ ↑(transferNatTransSelf (Adjunction.comp h (exp.adjunction A)) (Adjunction.comp (exp.adjunction (F.obj A)) h))
      (frobeniusMorphism F h A) =
    expComparison F A
[PROOFSTEP]
rw [← Equiv.eq_symm_apply]
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
⊢ frobeniusMorphism F h A =
    ↑(transferNatTransSelf (Adjunction.comp h (exp.adjunction A)) (Adjunction.comp (exp.adjunction (F.obj A)) h)).symm
      (expComparison F A)
[PROOFSTEP]
ext B : 2
[GOAL]
case w.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ NatTrans.app (frobeniusMorphism F h A) B =
    NatTrans.app
      (↑(transferNatTransSelf (Adjunction.comp h (exp.adjunction A))
              (Adjunction.comp (exp.adjunction (F.obj A)) h)).symm
        (expComparison F A))
      B
[PROOFSTEP]
dsimp [frobeniusMorphism, transferNatTransSelf, transferNatTrans, Adjunction.comp]
[GOAL]
case w.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B)) =
    𝟙 (L.obj (F.obj A ⨯ B)) ≫
      (L.map
            (prod.map (𝟙 (F.obj A))
              ((NatTrans.app h.unit B ≫
                  F.map (NatTrans.app (exp.adjunction A).unit (L.obj B)) ≫ 𝟙 (F.obj (A ⟹ A ⨯ L.obj B))) ≫
                𝟙 (F.obj (A ⟹ A ⨯ L.obj B)) ≫
                  NatTrans.app (expComparison F A) (A ⨯ L.obj B) ≫ 𝟙 (F.obj A ⟹ F.obj (A ⨯ L.obj B)))) ≫
          𝟙 (L.obj (F.obj A ⨯ F.obj A ⟹ F.obj (A ⨯ L.obj B))) ≫
            L.map (NatTrans.app (exp.adjunction (F.obj A)).counit (F.obj (A ⨯ L.obj B))) ≫
              NatTrans.app h.counit (A ⨯ L.obj B)) ≫
        𝟙 (A ⨯ L.obj B)
[PROOFSTEP]
simp only [id_comp, comp_id]
[GOAL]
case w.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B)) =
    L.map
        (prod.map (𝟙 (F.obj A))
          ((NatTrans.app h.unit B ≫ F.map (NatTrans.app (exp.adjunction A).unit (L.obj B))) ≫
            NatTrans.app (expComparison F A) (A ⨯ L.obj B))) ≫
      L.map (NatTrans.app (exp.adjunction (F.obj A)).counit (F.obj (A ⨯ L.obj B))) ≫ NatTrans.app h.counit (A ⨯ L.obj B)
[PROOFSTEP]
rw [← L.map_comp_assoc, prod.map_id_comp, assoc]
  -- Porting note: need to use `erw` here.
    -- https://github.com/leanprover-community/mathlib4/issues/5164
[GOAL]
case w.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B)) =
    L.map
        (prod.map (𝟙 (F.obj A)) (NatTrans.app h.unit B ≫ F.map (NatTrans.app (exp.adjunction A).unit (L.obj B))) ≫
          prod.map (𝟙 (F.obj A)) (NatTrans.app (expComparison F A) (A ⨯ L.obj B)) ≫
            NatTrans.app (exp.adjunction (F.obj A)).counit (F.obj (A ⨯ L.obj B))) ≫
      NatTrans.app h.counit (A ⨯ L.obj B)
[PROOFSTEP]
erw [expComparison_ev]
[GOAL]
case w.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B)) =
    L.map
        (prod.map (𝟙 (F.obj A)) (NatTrans.app h.unit B ≫ F.map (NatTrans.app (exp.adjunction A).unit (L.obj B))) ≫
          inv (prodComparison F A (A ⟹ A ⨯ L.obj B)) ≫ F.map (NatTrans.app (exp.ev A) (A ⨯ L.obj B))) ≫
      NatTrans.app h.counit (A ⨯ L.obj B)
[PROOFSTEP]
rw [prod.map_id_comp, assoc, ← F.map_id, ← prodComparison_inv_natural_assoc, ← F.map_comp]
  -- Porting note: need to use `erw` here.
    -- https://github.com/leanprover-community/mathlib4/issues/5164
[GOAL]
case w.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B)) =
    L.map
        (prod.map (F.map (𝟙 A)) (NatTrans.app h.unit B) ≫
          inv (prodComparison F A (L.obj B)) ≫
            F.map
              (prod.map (𝟙 A) (NatTrans.app (exp.adjunction A).unit (L.obj B)) ≫
                NatTrans.app (exp.ev A) (A ⨯ L.obj B))) ≫
      NatTrans.app h.counit (A ⨯ L.obj B)
[PROOFSTEP]
erw [exp.ev_coev]
[GOAL]
case w.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B)) =
    L.map
        (prod.map (F.map (𝟙 A)) (NatTrans.app h.unit B) ≫
          inv (prodComparison F A (L.obj B)) ≫ F.map (𝟙 (A ⨯ L.obj B))) ≫
      NatTrans.app h.counit (A ⨯ L.obj B)
[PROOFSTEP]
rw [F.map_id (A ⨯ L.obj B), comp_id]
[GOAL]
case w.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B)) =
    L.map (prod.map (F.map (𝟙 A)) (NatTrans.app h.unit B) ≫ inv (prodComparison F A (L.obj B))) ≫
      NatTrans.app h.counit (A ⨯ L.obj B)
[PROOFSTEP]
ext
[GOAL]
case w.h.h₁
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ (prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B))) ≫ prod.fst =
    (L.map (prod.map (F.map (𝟙 A)) (NatTrans.app h.unit B) ≫ inv (prodComparison F A (L.obj B))) ≫
        NatTrans.app h.counit (A ⨯ L.obj B)) ≫
      prod.fst
[PROOFSTEP]
rw [assoc, assoc, ← h.counit_naturality, ← L.map_comp_assoc, assoc, inv_prodComparison_map_fst]
[GOAL]
case w.h.h₁
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B)) ≫ prod.fst =
    L.map (prod.map (F.map (𝟙 A)) (NatTrans.app h.unit B) ≫ prod.fst) ≫ NatTrans.app h.counit A
[PROOFSTEP]
simp
[GOAL]
case w.h.h₂
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ (prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B))) ≫ prod.snd =
    (L.map (prod.map (F.map (𝟙 A)) (NatTrans.app h.unit B) ≫ inv (prodComparison F A (L.obj B))) ≫
        NatTrans.app h.counit (A ⨯ L.obj B)) ≫
      prod.snd
[PROOFSTEP]
rw [assoc, assoc, ← h.counit_naturality, ← L.map_comp_assoc, assoc, inv_prodComparison_map_snd]
[GOAL]
case w.h.h₂
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B)) ≫ prod.snd =
    L.map (prod.map (F.map (𝟙 A)) (NatTrans.app h.unit B) ≫ prod.snd) ≫ NatTrans.app h.counit (L.obj B)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
i : IsIso (expComparison F A)
⊢ IsIso (frobeniusMorphism F h A)
[PROOFSTEP]
rw [← frobeniusMorphism_mate F h] at i 
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
i :
  IsIso
    (↑(transferNatTransSelf (Adjunction.comp h (exp.adjunction A)) (Adjunction.comp (exp.adjunction (F.obj A)) h))
      (frobeniusMorphism F h A))
⊢ IsIso (frobeniusMorphism F h A)
[PROOFSTEP]
exact @transferNatTransSelf_of_iso _ _ _ _ _ _ _ _ _ _ _ i
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
i : IsIso (frobeniusMorphism F h A)
⊢ IsIso (expComparison F A)
[PROOFSTEP]
rw [← frobeniusMorphism_mate F h]
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
i : IsIso (frobeniusMorphism F h A)
⊢ IsIso
    (↑(transferNatTransSelf (Adjunction.comp h (exp.adjunction A)) (Adjunction.comp (exp.adjunction (F.obj A)) h))
      (frobeniusMorphism F h A))
[PROOFSTEP]
infer_instance
