[Merged by Bors] - feat(Order/Cover): characterise covering in Pi types#22929

b-mehta wants to merge 4 commits intomasterleanprover-community/mathlib4:masterfrom

cover-pileanprover-community/mathlib4:cover-piCopy head branch name to clipboard