fix: occurence check in `mkInjectiveTheoremTypeCore?`

[arthur-adjedj]

Closes #3386

Currently, when generating the signature of an injectivity lemma for a certain constructor c : forall xs, Foo a_1 ... a_n, mkInjectiveTheoremTypeCore? will differentiate between variables which are bound to stay the same between the two equal values (i.e inductive indices), and non-fixed ones. To do that, the function currently checks whether a variable x ∈ xs appears in the final co-domain Foo a_1 ... a_n of the constructor. This condition isn't enough however. As shown in the linked issue, the codomain may also depend on variables which appears in the type of free vars contained in Foo a_1 ... a_n, but not in the term itself. This PR fixes the issue by also checking the types of any free variable occuring in the final codomain, so as to ensure injectivity lemmas are well-typed.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-3398 has successfully built against this PR. (2024-02-19 14:56:16) View Log
• ✅ Mathlib branch lean-pr-testing-3398 has successfully built against this PR. (2024-02-19 15:38:43) View Log
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 605cecdde33e2ae84dec5653af4d8f9bc2649b17 --onto 62cdb51ed5b9d8487877d5a4adbcd4659d81fc6a. (2024-04-24 20:33:27)

[arthur-adjedj]

awaiting-review

[kim-em]

!bench

[leanprover-bot]

Here are the benchmark results for commit 70a0ce4f2aa3f823c35c903df43c50b6a192e60e. There were no significant changes against commit 605cecdde33e2ae84dec5653af4d8f9bc2649b17.