[Merged by Bors] - chore(LongestPole): private an import to reduce the rebuild pole#39609

b-mehta wants to merge 6 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

b-mehta:test-poleb-mehta/mathlib4:test-poleCopy head branch name to clipboard