Internal imports for the Hopf-problem modules

Retain the support imports marked for downstream use by Mathlib, together with the shared tactics. The original Prelude remains available through the project entry points.