have := left_cancel g (𝟙 _) e
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : Y ⟶ Y
⊢ g = g ≫ e ↔ 𝟙 Y = e
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : Y ⟶ Y
this : g ≫ 𝟙 Y = g ≫ e ↔ 𝟙 Y = e
⊢ g = g ≫ e ↔ 𝟙 Y = e