chore: make RBNode.mem_insert more robust

[kim-em]

This proof has three different hypotheses named h, and in a upcoming version of leanprover/lean4#2793 something is going to change in how they shadow each other.

This is a fix that works before and after. For now I'll be pointing leanprover-community/mathlib4#8076 at this branch.

@digama0 this proof has some other scary features (e.g. nonterminal simp) which we should fix at some point.

[digama0]

Can you say more about how the shadowing will change? That sounds a bit scary. (Can you point me to a branch that fails without this change?)

Regarding nonterminal simp, I don't avoid it here as heavily as in mathlib, because the simp set is small(er) and stable(r), and proofs tend to involve more domain-specific notions (like the RBSet functions in this case) for which the simp set is known exactly. I think the jury is still out regarding whether this is a good idea or whether we need to be as defensive as mathlib wrt the simp set.

[kim-em]

@digama0, try the Std branch lean-pr-testing-2793. It has no changes except to use the toolchain from leanprover/lean4#2793.

[digama0]

It seems the issue is that the rw [find?_eq_zoom] at h line does not delete the original h, and the reason for this is that it results in h: root? (zoom (cmp v) t ?inr.p).fst = some v' where ?inr.p could possibly depend on the original h. The mvar is unified away in the next rewrite, but it should have been inferred from the optParam in find?_eq_zoom, and rw [find?_eq_zoom (p := .root)] at h fixes the issue. In other words, this is another manifestation of the issue you reported: leanprover/lean4#2793 (comment)

[kim-em]

Ah, great, thank you.

I'm happy in that case to either close this or merge, as you see fit!

[digama0]

Let's leave it open until we find out how leanprover/lean4#2793 (comment) will be resolved.

[fgdorais]

The original upstream PR was subsumed by lean4#4596. Does this mean this PR is obsolete?