Lean fundamental groupoid: avoid eqToHom chains by subst + pointwise path equality

Proving identities like r_*(δ · i_*γ · δ⁻¹) = γ in FundamentalGroup (base points equal only propositionally, h : r x = z) via eqToHom algebra failed: rw/erw on eqToHom_trans hit 'motive is not type correct at implicit transparency' because objects like (FundamentalGroupoid.map r).obj (mk x) and mk (r x) are only defeq. What worked: make the mismatched base point a variable and subst h first (so eqToIso rfl simp-reduces away), then rcases γ with ⟨g⟩; induction g using Quotient.ind, change the goal to Path.Homotopic.Quotient.mk P = Path.Homotopic.Quotient.mk g with P the explicit composite path (map of trans of trans), prove P = (Path.refl _).trans (g.trans (Path.refl _)) by ext t; simp only [Path.trans_apply, ...]; split_ifs <;> simp [hyps], then change (𝟙 _ ≫ mk g ≫ 𝟙 _ : _ ⟶ _) = _; simp. Also: (p.trans q).map f is not defeq to (p.map f).trans (q.map f); use Path.map_trans and ← Path.map_symm before rfl. Name membership lemmas (x ∈ U from x ∈ U ∩ V) instead of using .1 inside types to keep rw working.