[Merged by Bors] - feat(Homotopy/Path): add missing lemmas#30552

urkud wants to merge 1 commit intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

urkud:pathExtend-evalAturkud/mathlib4:pathExtend-evalAtCopy head branch name to clipboard