Commit 2026-05-27 10:15 e745713e

feat: overlapping instances linter (#38126) This PR implements the overlapping instances linter, with better performance than the previous attempt. The overlapping instances linter warns on data-carrying overlaps between instances in the local context of a declaration, as well as on redundant instances of Prop classes (i.e. those which can be synthesized from another instance in the context). An annoyance is the need for withSetBoolOptionIn. This is a private declaration in the unusedInstancesInType linter, with a link to leanprover/lean4#13133, which has been merged. When that commit lands in mathlib, we should move to withSetOptionIn. See #35095 and #33677 for previous iterations of this linter. See #14731 for an old attempt at a weaker form of this linter.