refactor: eliminate simp +instances uses related to iterators/ranges/slices#12304

datokrat wants to merge 10 commits intosimp_no_instleanprover/lean4:simp_no_instfrom

paul/simp_no_instleanprover/lean4:paul/simp_no_instCopy head branch name to clipboard