simp at this
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : X ⟶ X
this : 𝟙 X ≫ g = e ≫ g ↔ 𝟙 X = e
⊢ g = e ≫ g ↔ 𝟙 X = e
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : X ⟶ X
this : g = e ≫ g ↔ 𝟙 X = e
⊢ g = e ≫ g ↔ 𝟙 X = e