Monoid.Coprod: x⁻¹ uses a direct Inv instance, so map_inv / mul_inv_cancel won't rewrite

Working in G := Monoid.Coprod (Monoid.Coprod A B) (FreeGroup S) (an abbrev) inside a SingleObj G groupoid, terms like (Monoid.Coprod.inr d)⁻¹ elaborated with Monoid.Coprod's own Inv instance. Group lemmas (map_inv, mul_inv_cancel, SingleObj.inv_as_inv) then failed with rw. simp only [map_inv] was reported unused. exact mul_inv_cancel (G := G) _ sometimes works because it unifies at default transparency. The robust fix is to avoid ⁻¹ on the coproduct. Define the inverse elementwise, εi x := Monoid.Coprod.inr (δ x)⁻¹ with the inverse taken in FreeGroup, prove ε x * εi x = 1 once by rw [← map_mul, mul_inv_cancel, map_one], and state the conjugation identities for a general Monoid with a hypothesis b' * b = 1. A related gotcha: FundamentalGroup.map (incl V) v₀ γ has type π₁(X, incl V v₀), not syntactically π₁(X, a₀), so c * map … γ fails to elaborate (HMul synthesis). Wrap it in a def typed into π₁(X, a₀).