[#15215] fix: use pi_congr instead of forall_congr, deprecate the latter

[downstream-lean4]

This is the adaptation PR for leanprover/lean4#15215.

[downstream-lean4]

Build report for downstream: follow upstream PR

Stayed green

Repo	Critical	Build	Test	Lint
aesop	✅	✅ in 17s	✅ in 4s	⏭️
batteries	✅	✅ in 12s	✅ in 4s	✅ in 2s
import-graph	✅	✅ in 3s	✅ in 4s	⏭️
lean4-cli	✅	✅ in 3s	✅ in 0s	⏭️
mathlib4	✅	✅ in 1037s	✅ in 334s	✅ in 96s
plausible	✅	✅ in 3s	✅ in 2s	⏭️
ProofWidgets4	✅	✅ in 5s	✅ in 1s	⏭️
quote4	✅	✅ in 6s	✅ in 1s	⏭️
reference-manual	✅	✅ in 76s	⏭️	⏭️
BibtexQuery		✅ in 3s	⏭️	⏭️
comparator		✅ in 3s	⏭️	⏭️
cslib		✅ in 32s	✅ in 9s	✅ in 3s
doc-gen4		✅ in 16s	⏭️	⏭️
illuminate		✅ in 8s	✅ in 11s	⏭️
lean4-unicode-basic		✅ in 4s	⏭️	⏭️
lean4export		✅ in 3s	✅ in 8s	⏭️
LeanSearchClient		✅ in 2s	✅ in 0s	⏭️
leansqlite		✅ in 9s	✅ in 20s	⏭️
nerodia		✅ in 5s	✅ in 21s	⏭️
repl		✅ in 4s	✅ in 61s	⏭️
verso		✅ in 127s	✅ in 175s	⏭️
verso-slides		✅ in 21s	✅ in 9s	⏭️
verso-web-components		✅ in 8s	⏭️	⏭️

View run

[sgraf812]

!bench mathlib4

[leanprover-radar]

Benchmark results for f121e0b against b9ce333 are in. There are significant results. @sgraf812

• 🟥 build//instructions: +125.1G (+0.09%)

Small changes (1✅, 42🟥)

• 🟥 build/module/Aesop.Nanos//instructions: +26.3M (+2.15%)
• 🟥 build/module/Aesop.RuleTac.Apply//instructions: +46.6M (+2.12%)
• 🟥 build/module/Aesop.RuleTac.Cases//instructions: +65.2M (+2.52%)
• 🟥 build/module/Aesop.RuleTac.Preprocess//instructions: +32.7M (+2.44%)
• 🟥 build/module/Aesop.Script.Util//instructions: +19.1M (+1.14%)
• 🟥 build/module/Aesop.Util.Unfold//instructions: +26.4M (+1.12%)
• 🟥 build/module/Batteries.Classes.RatCast//instructions: +20.8M (+2.11%)
• 🟥 build/module/Batteries.CodeAction//instructions: +28.8M (+2.06%)
• 🟥 build/module/Batteries.Control.ForInStep.Lemmas//instructions: +20.7M (+1.71%)
• 🟥 build/module/Batteries.Data.AssocList.Lemmas//instructions: +44.9M (+1.09%)
• 🟥 build/module/Batteries.Data.BinomialHeap//instructions: +42.2M (+3.03%)
• 🟥 build/module/Batteries.Data.BitVec.Basic//instructions: +18.2M (+1.86%)
• 🟥 build/module/Batteries.Data.Float.Basic//instructions: +18.1M (+1.10%)
• 🟥 build/module/Batteries.Data.Float.Rat//instructions: +16.2M (+1.61%)
• 🟥 build/module/Batteries.Data.FloatArray//instructions: +26.8M (+2.59%)
• 🟥 build/module/Batteries.Data.List.Init.Lemmas//instructions: +17.6M (+1.86%)
• 🟥 build/module/Batteries.Data.MLList.IO//instructions: +21.2M (+1.94%)
• 🟥 build/module/Batteries.Data.Nat.Lemmas//instructions: +37.2M (+1.56%)
• 🟥 build/module/Batteries.Data.Range//instructions: +22.2M (+1.64%)
• 🟥 build/module/Batteries.Lean.Json//instructions: +23.0M (+2.24%)
• and 23 more