fix: use pi_congr instead of forall_congr, deprecate the latter

[sgraf812]

This PR generalizes the conv and simp tactics to apply pi_congr instead of forall_congr. The test case for #7507 has examples that work now, but only worked at universe v=0 before.

Since there are no more remaining uses of forall_congr, it is now deprecated.

Closes #7507. Continues #14516, whose base branch no longer exists.

[downstream-lean4]

The adaptation PR for this PR is leanprover/downstream-lean4#85.

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for ba545a5 against e12fac8 are in. No significant results found. @sgraf812

• 🟥 build//instructions: +320.9M (+0.00%)

Small changes (5🟥)

• 🟥 build/module/Init.Data.Iterators.Combinators.Monadic.ULift//instructions: +3.2M (+0.22%)
• 🟥 build/module/Init.Data.Iterators.Internal.LawfulMonadLiftFunction//instructions: +4.0M (+0.34%)
• 🟥 build/module/Init.Data.Nat.Lcm//instructions: +6.2M (+0.39%)
• 🟥 build/module/Init.Data.String.Lemmas.Pattern.Pred//instructions: +27.7M (+0.52%)
• 🟥 build/module/Lean.Elab.Tactic.Conv.Congr//instructions: +23.9M (+0.38%)

[sgraf812]

Note for review: this patch makes it possible for simp to rewrite in more situations, so it traverses more terms in mathlib for rewriting opportunities and regresses slightly. I think it's the right call nonetheless; on the adaptation branch I discovered a simp antipattern that way (blanket eq_zero [...] (lhs : α) : lhs = 0 as a simp lemma) that we or mathlib might want to incorporate into a simp linter at some point: leanprover-community/mathlib4#42053.