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 => g ⁻¹ ≫ x) (g ≫ h) = (fun x => g ⁻¹ ≫ x) (g ≫ h')
⊢ h = h'
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 : h = h'
⊢ h = h'