case w
C : Type u₁
inst✝¹ : Category C
inst✝ : MonoidalCategory C
X Y : C
p : ExactPairing X Y
⊢ (rightDualIso p p).hom = (Iso.refl Y).hom
C : Type u₁
inst✝¹ : Category C
inst✝ : MonoidalCategory C
X Y : C
p : ExactPairing X Y
⊢ rightDualIso p p = Iso.refl Y
ext
no goals
case w
C : Type u₁
inst✝¹ : Category C
inst✝ : MonoidalCategory C
X Y : C
p : ExactPairing X Y
⊢ (rightDualIso p p).hom = (Iso.refl Y).hom
simp only [rightDualIso, Iso.refl_hom, @rightAdjointMate_id _ _ _ _ ⟨Y⟩]