[GOAL]
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.129, u_1} C
inst✝⁴ : Category.{?u.133, u_2} D
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory D
F : MonoidalFunctor C D
inst✝¹ : Faithful F.toFunctor
X Y : C
eval : Y ⊗ X ⟶ 𝟙_ C
coeval : 𝟙_ C ⟶ X ⊗ Y
inst✝ : ExactPairing (F.obj X) (F.obj Y)
map_eval : F.map eval = inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X) ≫ ε_ (F.obj X) (F.obj Y) ≫ F.ε
map_coeval : F.map coeval = inv F.ε ≫ η_ (F.obj X) (F.obj Y) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y
⊢ F.map ((𝟙 Y ⊗ coeval) ≫ (α_ Y X Y).inv ≫ (eval ⊗ 𝟙 Y)) = F.map ((ρ_ Y).hom ≫ (λ_ Y).inv)
[PROOFSTEP]
simp [map_eval, map_coeval, MonoidalFunctor.map_tensor]
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.129, u_1} C
inst✝⁴ : Category.{?u.133, u_2} D
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory D
F : MonoidalFunctor C D
inst✝¹ : Faithful F.toFunctor
X Y : C
eval : Y ⊗ X ⟶ 𝟙_ C
coeval : 𝟙_ C ⟶ X ⊗ Y
inst✝ : ExactPairing (F.obj X) (F.obj Y)
map_eval : F.map eval = inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X) ≫ ε_ (F.obj X) (F.obj Y) ≫ F.ε
map_coeval : F.map coeval = inv F.ε ≫ η_ (F.obj X) (F.obj Y) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y
⊢ F.map ((coeval ⊗ 𝟙 X) ≫ (α_ X Y X).hom ≫ (𝟙 X ⊗ eval)) = F.map ((λ_ X).hom ≫ (ρ_ X).inv)
[PROOFSTEP]
simp [map_eval, map_coeval, MonoidalFunctor.map_tensor]
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{?u.23115, u_1} C
inst✝⁵ : Category.{?u.23119, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝² : Full F.toFunctor
inst✝¹ : Faithful F.toFunctor
X Y : C
inst✝ : ExactPairing (F.obj X) (F.obj Y)
⊢ F.map (F.preimage (inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X) ≫ ε_ (F.obj X) (F.obj Y) ≫ F.ε)) =
    inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X) ≫ ε_ (F.obj X) (F.obj Y) ≫ F.ε
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{?u.23115, u_1} C
inst✝⁵ : Category.{?u.23119, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝² : Full F.toFunctor
inst✝¹ : Faithful F.toFunctor
X Y : C
inst✝ : ExactPairing (F.obj X) (F.obj Y)
⊢ F.map (F.preimage (inv F.ε ≫ η_ (F.obj X) (F.obj Y) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y)) =
    inv F.ε ≫ η_ (F.obj X) (F.obj Y) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.27280, u_1} C
inst✝⁴ : Category.{?u.27284, u_2} D
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory D
F : MonoidalFunctor C D
inst✝¹ : IsEquivalence F.toFunctor
X : C
inst✝ : HasLeftDual (F.obj X)
⊢ ExactPairing ((Functor.inv F.toFunctor).obj ᘁ(F.obj X)) X
[PROOFSTEP]
refine @exactPairingOfFullyFaithful _ _ _ _ _ _ F _ _ _ _ ?_
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.27280, u_1} C
inst✝⁴ : Category.{?u.27284, u_2} D
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory D
F : MonoidalFunctor C D
inst✝¹ : IsEquivalence F.toFunctor
X : C
inst✝ : HasLeftDual (F.obj X)
⊢ ExactPairing (F.obj ((Functor.inv F.toFunctor).obj ᘁ(F.obj X))) (F.obj X)
[PROOFSTEP]
refine @exactPairingCongrLeft _ _ _ _ _ _ ?_ (F.toFunctor.asEquivalence.counitIso.app _)
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.27280, u_1} C
inst✝⁴ : Category.{?u.27284, u_2} D
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory D
F : MonoidalFunctor C D
inst✝¹ : IsEquivalence F.toFunctor
X : C
inst✝ : HasLeftDual (F.obj X)
⊢ ExactPairing ((𝟭 D).obj ᘁ(F.obj X)) (F.obj X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.27280, u_1} C
inst✝⁴ : Category.{?u.27284, u_2} D
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory D
F : MonoidalFunctor C D
inst✝¹ : IsEquivalence F.toFunctor
X : C
inst✝ : HasLeftDual (F.obj X)
⊢ ExactPairing (ᘁ(F.obj X)) (F.obj X)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.30444, u_1} C
inst✝⁴ : Category.{?u.30448, u_2} D
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory D
F : MonoidalFunctor C D
inst✝¹ : IsEquivalence F.toFunctor
X : C
inst✝ : HasRightDual (F.obj X)
⊢ ExactPairing X ((Functor.inv F.toFunctor).obj (F.obj X)ᘁ)
[PROOFSTEP]
refine @exactPairingOfFullyFaithful _ _ _ _ _ _ F _ _ _ _ ?_
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.30444, u_1} C
inst✝⁴ : Category.{?u.30448, u_2} D
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory D
F : MonoidalFunctor C D
inst✝¹ : IsEquivalence F.toFunctor
X : C
inst✝ : HasRightDual (F.obj X)
⊢ ExactPairing (F.obj X) (F.obj ((Functor.inv F.toFunctor).obj (F.obj X)ᘁ))
[PROOFSTEP]
refine @exactPairingCongrRight _ _ _ _ _ _ ?_ (F.toFunctor.asEquivalence.counitIso.app _)
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.30444, u_1} C
inst✝⁴ : Category.{?u.30448, u_2} D
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory D
F : MonoidalFunctor C D
inst✝¹ : IsEquivalence F.toFunctor
X : C
inst✝ : HasRightDual (F.obj X)
⊢ ExactPairing (F.obj X) ((𝟭 D).obj (F.obj X)ᘁ)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.30444, u_1} C
inst✝⁴ : Category.{?u.30448, u_2} D
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory D
F : MonoidalFunctor C D
inst✝¹ : IsEquivalence F.toFunctor
X : C
inst✝ : HasRightDual (F.obj X)
⊢ ExactPairing (F.obj X) (F.obj X)ᘁ
[PROOFSTEP]
infer_instance
