rw [comp_id, comp_id] at this
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
this : (𝟙 X) ⁻¹ ≫ 𝟙 X ≫ 𝟙 X = 𝟙 X
⊢ (𝟙 X) ⁻¹ = 𝟙 X
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
this : (𝟙 X) ⁻¹ = 𝟙 X
⊢ (𝟙 X) ⁻¹ = 𝟙 X