[Merged by Bors] - feat: drop completeness assumption in the definition of setToFun, expand API#39615

sgouezel wants to merge 7 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

sgouezel:SG_noCompletesgouezel/mathlib4:SG_noCompleteCopy head branch name to clipboard