I'm playing around with the definition of a Lie groupoid following Eckhard Meinrenken's notes. I read the thing for the first time in my life like an hour ago, so assume that I don't know anything about the topic.
One of the very first things he leaves as an exercise after the definition is that inverses are unique. More precisely, if $\mathcal{G} \rightrightarrows M$ and we have $g,h,h' \in \mathcal{G}$ with $g\circ h, g\circ h', h \circ g$ and $h'\circ g$ all in $M$, with ${\sf s}(h) = {\sf s}(h') = {\sf t}(g)$ and ${\sf t}(h) = {\sf t}(h') = {\sf s}(g)$, then necessarily $h=h'$. Mimicking what happens for groups, I cooked up a:
Proof. \begin{align} h &= {\sf t}(h) \circ h = {\sf t}(h') \circ h = {\sf t}(h'\circ g) \circ h \\ &= (h'\circ g)\circ h = h' \circ (g\circ h) = h' \circ {\sf s}(g\circ h) \\ &= h' \circ {\sf s}(h) = h' \circ {\sf s}(h') = h'.\end{align} And I didn't even use all the assumptions. Neat. So we're finally allowed to write $h = g^{-1}$, so ${\sf s}(g^{-1}) = {\sf t}(g)$, ${\sf t}(g^{-1}) = {\sf s}(g)$, and $g\circ g^{-1} = {\sf t}(g)$ and $g^{-1} \circ g = {\sf s}(g)$.
Now comes my question. One would expect that a cancellation law should follow from existence of inverses like this, unless the uniqueness of a unit is essential for this. Namely, if $g_1\circ h = g_2 \circ h$ for $g_1,g_2,h \in \mathcal{G}$ (automatically implying that ${\sf s}(g_1) = {\sf s}(g_2) = {\sf s}(h)$ as well as ${\sf t}(g_1) = {\sf t}(g_2)$), then $g_1 = g_2$. So: $$g_1 \circ h = g_2 \circ h \implies (g_1\circ h)\circ h^{-1} = (g_2\circ h)\circ h^{-1} \implies g_1 \circ (h\circ h^{-1}) = g_2 \circ (h \circ h^{-1}) \implies g_1 \circ {\sf t}(h) = g_2 \circ {\sf t}(h).$$
I do not immediately see how to get rid of this pesky ${\sf t}(h)$. Is the result I'm trying to prove in general false and the above is the best we can get? Are extra assumptions necessary?
The target of $h$ is the source of both $g_1$ and $g_2$. Actually, if you don't make mistakes, you can just ignore any $s (\bullet)$ or $t (\bullet)$ appearing in a composition chain, just as you can ignore identity elements in a group.