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