case hom_inv_id
C : Type u
inst✝ : Category C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ 𝟙 X ≫ 𝟙 X = 𝟙 X
C : Type u
inst✝ : Category C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ inv (𝟙 X) = 𝟙 X
apply inv_eq_of_hom_inv_id
no goals
case hom_inv_id
C : Type u
inst✝ : Category C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ 𝟙 X ≫ 𝟙 X = 𝟙 X
simp