case w
C : Type u
inst✝ : Category C
X Y Z : C
α : X ≅ Y
⊢ (refl X ≪≫ α).hom = α.hom
C : Type u
inst✝ : Category C
X Y Z : C
α : X ≅ Y
⊢ refl X ≪≫ α = α
ext
no goals
case w
C : Type u
inst✝ : Category C
X Y Z : C
α : X ≅ Y
⊢ (refl X ≪≫ α).hom = α.hom
apply Category.id_comp