case mk
C : Type u
inst✝ : Category C
X✝ Y✝ Z X Y : C
hom✝ : X ⟶ Y
inv✝ : Y ⟶ X
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
⊢ (mk hom✝ inv✝).symm.symm = mk hom✝ inv✝
C : Type u
inst✝ : Category C
X✝ Y✝ Z X Y : C
α : X ≅ Y
⊢ α.symm.symm = α
cases α
no goals
case mk
C : Type u
inst✝ : Category C
X✝ Y✝ Z X Y : C
hom✝ : X ⟶ Y
inv✝ : Y ⟶ X
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
⊢ (mk hom✝ inv✝).symm.symm = mk hom✝ inv✝
rfl