mathlib3

919aad21 - refactor(topology/path_connected): make `path` extend `C(I, X)` (#9133)