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