fix: record funext split candidates for every parent of a lambda in `grind` This PR fixes a `grind` incompleteness where a lambda that occurs as an argument of two different functions never gets a function extensionality case split for the second one. For example, `f (fun x => k x a) = f (fun x => k x b)` with `a = b` now closes even when `fun x => k x a` also occurs in a hypothesis `g (fun x => k x a)`. Funext split candidates are indexed by the parent function and argument position, and a lambda was only recorded there when it was internalized for the first time, with the parent it first appeared in. A later occurrence under another function registered nothing, so the candidate `F = F'` for that position was never created. Lambdas are now recorded under each new parent, once per function and position. The new test `grind_subtype_mk_fact.lean` is the Mathlib `y_surjective` example that fails once the `Subtype.mk` fact is asserted before the instance that contains the second copy of the lambda is internalized. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.