simp at this
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
hyp : g ≫ h = g' ≫ h
this : (fun x => x ≫ h ⁻¹ ) (g ≫ h) = (fun x => x ≫ h ⁻¹ ) (g' ≫ h)
⊢ g = g'
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
hyp : g ≫ h = g' ≫ h
this : g = g'
⊢ g = g'