Lean4
/-- Transport an exact pairing across an isomorphism in the second argument. -/
def exactPairingCongrRight {X Y Y' : C} [ExactPairing X Y'] (i : Y ≅ Y') : ExactPairing X Y
where
evaluation' := i.hom ▷ X ≫ ε_ _ _
coevaluation' := η_ _ _ ≫ X ◁ i.inv
evaluation_coevaluation' := by
calc
_ = η_ X Y' ▷ X ⊗≫ X ◁ (i.inv ≫ i.hom) ▷ X ≫ X ◁ ε_ X Y' := by monoidal
_ = η_ X Y' ▷ X ⊗≫ X ◁ ε_ X Y' := by rw [Iso.inv_hom_id]; monoidal
_ = _ := by
rw [evaluation_coevaluation'']
simp
coevaluation_evaluation' :=
calc
_ = Y ◁ η_ X Y' ⊗≫ (Y ◁ (X ◁ i.inv) ≫ i.hom ▷ (X ⊗ Y)) ⊗≫ ε_ X Y' ▷ Y := by monoidal
_ = 𝟙 _ ⊗≫ (Y ◁ η_ X Y' ≫ i.hom ▷ (X ⊗ Y')) ⊗≫ ((Y' ⊗ X) ◁ i.inv ≫ ε_ X Y' ▷ Y) ⊗≫ 𝟙 _ := by
rw [whisker_exchange]; monoidal
_ = 𝟙 _ ⊗≫ i.hom ⊗≫ (Y' ◁ η_ X Y' ⊗≫ ε_ X Y' ▷ Y') ⊗≫ i.inv ⊗≫ 𝟙 _ := by rw [whisker_exchange, whisker_exchange];
monoidal
_ = 𝟙 _ ⊗≫ (i.hom ≫ i.inv) ⊗≫ 𝟙 _ := by rw [coevaluation_evaluation'']; monoidal
_ = (ρ_ Y).hom ≫ (λ_ Y).inv := by
rw [Iso.hom_inv_id]
monoidal
