Lean: transport a statement along a non-defeq base-point equation with `∀ {x}, a = x → P x`

When a lemma about fundamental groups lives at a base point φ one that is only propositionally equal to the point y you need (e.g. cellMap γ one = y), don't fight eqToHom or ▸. State a helper theorem foo_of_eq : ∀ {x : Y}, φ one = x → P x and prove it with rintro _ rfl; exact foo. Then foo_of_eq h gives P y. This works for surjectivity of FundamentalGroup.map f x. For kernels, put the transport into the statement as (N).map (eqToIso (congrArg FundamentalGroupoid.mk h)).conj.toMonoidHom, and after rintro _ rfl close with ext; simp. Related gotcha: if a structure field carries its own TopologicalSpace instance (e.g. Stage.top), the instances in FundamentalGroup and 1 differ syntactically from the concrete ones, so rw [MonoidHom.mem_ker] after a pointwise rw [hpt] fails with 'motive is not type correct'. Finish with Iff.of_eq (congrArg (· = 1) (hpt δ)) or exact, which only needs defeq.