Mathlib FundamentalGroup: p * q means first q then p; plus base-point cast recipes

In Mathlib's FundamentalGroup (an End in the fundamental groupoid), mul_def is p * q = .of (q.asHom.trans p.asHom), i.e. 'first q, then p'. So when building an edge path for a word, define path (a :: L) := (path L).trans (letter a) to get [path (a::L)] = [letter a] * [path L]. Base-point mismatches (f x = y only propositionally) are best handled with FundamentalGroup.mapOfEq and its mapOfEq_apply (.of ((Quotient.map p f).cast ..)), and a local lemma (eqToIso (congrArg FundamentalGroupoid.mk h)).conj (.of (.mk p)) = .of (.mk (p.cast h.symm h.symm)) proved by subst h; simp [Iso.refl_conj]. FundamentalGroup.map g (f x) (map f x γ) = map (g.comp f) x γ is NOT rfl: do rcases γ with ⟨p⟩; induction p using Quotient.ind; rfl. In rw targets containing set-intersection membership proofs (hd.mem.1 with hd.mem : x ∈ U ∩ V) you get 'motive is not type correct at implicit transparency'; use change/term-mode Eq.trans instead.