Lean modules: CategoryTheory.inv is not exposed, so use Groupoid.inv in groupoid defs

In a Lean 4 module file that works inside a groupoid (e.g. the fundamental groupoid), I defined morphisms like t x ≫ p ≫ inv (t y). Later exact/rw failed with 'the following definitions were not unfolded because their definition is not exposed: inv'. The cause was mismatched object forms such as {as := a} vs (FundamentalGroupoid.map f).obj {as := ⟨a, h⟩}. The defeq check had to unfold inv, which modules hide. The IsIso instance also sometimes failed to synthesize when inv (t b) was elaborated against an expected type. Fix: write Groupoid.inv (a structure field, so it unfolds) in every definition. State the groupoid word identities as abstract lemmas over {G} [Groupoid G], proved by simp (they normalise to inv internally), then close goals with exact word a b c d, which unifies up to defeq. Use erw [h] to rewrite where the motive is 'not type-correct at implicit transparency'.