Lean full subgroupoids: prove retraction naturality only where objects agree by rfl

Formalizing Brown's van Kampen for Π(X, A): I modeled Π(Y, A) as InducedCategory (FundamentalGroupoid Y) (fun a : A ↦ ⟨a.1⟩), whose homs are a 1-field structure (.hom, InducedCategory.homMk), and a retraction Π(Y) ⥤ Π(Y, A) by conjugating with chosen paths. A general naturality lemma map f ⋙ S.functor = R.functor ⋙ PiA.map f with propositional S.β (f y) = f (R.β y) was a dead end: rw/change kept failing with 'not type-correct at implicit transparency' because of (map f).obj ⟨x⟩ vs ⟨f x⟩, and inv even lost its IsIso instance inside change. What worked was proving it only for subspace inclusions, where the retraction data on W is defined from the data on X (β' y = ⟨β y.1, _⟩, c' y = toSub (c y.1)), so the objects agree definitionally. Then refine CategoryTheory.Functor.ext (fun _ ↦ rfl) (fun _ _ p ↦ ?_); erw [eqToHom_refl, eqToHom_refl, Category.id_comp, Category.comp_id]; ext; simp only [Retr.functor, PiA.map, InducedCategory.homMk_hom, Functor.map_comp, Functor.map_inv]; rfl. Also, when a functor between full subcategories has a MapsTo argument like (fun _ h ↦ h), wrap it in an abbrev with the sets given explicitly. Otherwise the target set can elaborate as Membership.mem A, and calc then fails with 'Trans Eq Eq'. For a dite-defined Sigma choice pick x : Σ b, Path b x, rw [pick, ite_eq_right h0, dite_eq_left hx] works under .2 t, where split_ifs does not.