feat: don't reduce proofs in is_def_eq_core

[arthur-adjedj]

This PR ensures is_def_eq_proof_irrel runs before reducing any potential proofs in is_def_eq_core rather than after. This is already the order in which things run in the elaborator, so no need for any changes there.

Related to #14977

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-15103 has successfully built against this PR. (2026-09-10 11:32:54) View Log
• ✅ Mathlib branch lean-pr-testing-15103 has successfully built against this PR. (2026-09-10 15:21:51) View Log

[arthur-adjedj]

!bench

[arthur-adjedj]

!bench mathlib

[leanprover-radar]

Benchmark results for 4f29e98 against fe53f21 are in. There are significant results. @arthur-adjedj

• 🟥 build//instructions: +9.1G (+0.08%)

Medium changes (2🟥)

• 🟥 vcgen/AdcChain/250/kernel//wall-clock: +3ms (+12.85%)
• 🟥 vcgen/AdcChain/500/kernel//wall-clock: +7ms (+13.21%)

Small changes (1✅, 32🟥)

• 🟥 build/module/Init.Data.Array.BinSearch//instructions: +49.4M (+0.86%)
• 🟥 build/module/Init.Data.Array.Extract//instructions: +257.8M (+0.78%)
• 🟥 build/module/Init.Data.Array.QSort.Basic//instructions: +37.9M (+0.39%)
• 🟥 build/module/Init.Data.BitVec.Bitblast//instructions: +291.3M (+0.60%)
• 🟥 build/module/Init.Data.Char.Ordinal//instructions: +80.1M (+1.42%)
• 🟥 build/module/Init.Data.Dyadic.Basic//instructions: +82.7M (+0.63%)
• 🟥 build/module/Init.Data.List.Nat.Count//instructions: +25.9M (+0.69%)
• 🟥 build/module/Init.Data.List.Nat.Perm//instructions: +13.0M (+0.57%)
• 🟥 build/module/Init.Data.List.Nat.Sublist//instructions: +28.8M (+0.63%)
• 🟥 build/module/Init.Data.List.Nat.TakeDrop//instructions: +47.2M (+0.46%)
• 🟥 build/module/Init.Data.List.Sort.Basic//instructions: +13.7M (+0.56%)
• 🟥 build/module/Init.Data.List.Sort.Impl//instructions: +73.0M (+0.68%)
• 🟥 build/module/Init.Data.Nat.Fold//instructions: +34.2M (+0.42%)
• 🟥 build/module/Init.Data.Range.Basic//instructions: +18.6M (+0.57%)
• 🟥 build/module/Init.Data.Range.Lemmas//instructions: +33.2M (+0.75%)
• 🟥 build/module/Init.Data.String.Lemmas.Pattern.Memcmp//instructions: +17.8M (+0.77%)
• 🟥 build/module/Init.Data.String.Lemmas.Pattern.String.ForwardSearcher//instructions: +109.9M (+0.63%)
• ✅ build/module/Init.Data.Vector.Range//instructions: -19.7M (-0.55%)
• 🟥 build/module/Init.Grind.Module.Envelope//instructions: +43.6M (+0.69%)
• 🟥 build/module/Init.Grind.Ring.Envelope//instructions: +57.3M (+0.66%)
• and 13 more

[leanprover-radar]

Benchmark results for leanprover-community/mathlib4-nightly-testing@d7ce512 against leanprover-community/mathlib4-nightly-testing@2025d0b are in. No significant results found. @arthur-adjedj

• 🟥 build//instructions: +92.6G (+0.07%)

Small changes (1✅, 1🟥)

• 🟥 build/module/Batteries.Data.Vector.Basic//instructions: +41.8M (+0.57%)
• ✅ build/module/Mathlib.Algebra.Algebra.Operations//instructions: -2.0G (-4.25%)