[Merged by Bors] - feat(Tactic): add #defeq_abuse tactic combinator

[kim-em]

This PR adds #defeq_abuse in, a tactic/command combinator for diagnosing backward.isDefEq.respectTransparency failures. It runs the given tactic or command with the option both true and false, and when the strict setting fails, walks the trace tree to identify the specific isDefEq checks that are root causes.

Reusable trace-tree analysis utilities are extracted into Mathlib.Lean.MessageData.Trace:

• TraceResult / traceResultOf — structured access to the ✅/❌/💥 status encoding
• foldTraceNodes — generic fold over MessageData trace trees
• stripTraceResultPrefix / dedupByString — helpers for trace content comparison

Companion lean4 PRs that will simplify this further:

• feat: add structured TraceResult to TraceData leanprover/lean4#12698 — structured TraceResult field on TraceData
• feat: add Meta.synthInstance.apply trace class leanprover/lean4#12699 — Meta.synthInstance.apply trace class

See https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/backward.2EisDefEq.2ErespectTransparency

🤖 Prepared with Claude Code

[github-actions]

PR summary d300915bf1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
There are 6696 files with changed transitive imports taking up over 297229 characters: this is too many to display!
You can run scripts/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

+ A
+ B
+ Gr'
+ MyAction
+ MyPred
+ MySub₂
+ MySub₂.toAddSubgroup
+ Num'
+ Sm'
+ TraceResult
+ VisitStep
+ Zo'
+ analyzeTraces
+ b
+ dedupByString
+ extractInstName
+ instance : Gr' Int
+ instance : Membership ℕ (MyPred ℕ) where mem s a := s a
+ instance : Singleton ℕ (MyPred ℕ) where singleton a x := x = a
+ instance : Zo' Int
+ instance {G : Type} [AddCommGroup G] : CoeSort (MySub₂ G) Type
+ instance {n} : Num' Int n
+ instance {α} [Zo' α] : Num' α 0
+ instance {α} [h : Gr' α] : Sm' α := { h with }
+ myOp
+ myPredBoundedOrder
+ myPredCompleteLattice
+ myPredDistribLattice
+ myPred_disjoint_singleton_right
+ mySub₂AddCommGroup
+ mySub₂AddCommMonoid
+ mySub₂MyAction
+ myTestFun
+ onlyOnDefEqNodes
+ reportDefEqAbuse
+ stripTraceResultPrefix
+ testCoersion
+ testVirtualParent
+ testVirtualParentFixed
+ test_zo_cmd_abuse
+ traceResultOf
+ visitWithAndAscendM
+ visitWithM
+ zo_eq_iff
++ instance {V : Type} [AddCommGroup V] [Module ℝ V] {l : Submodule ℝ V} :

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
11957	1	backward.isDefEq

Current commit 93584a9453
Reference commit d300915bf1

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[SnirBroshi]

Since this is specific to respectTransparency and not all defeq abuse, is it possible to rename the new tactic, in order to reserve #defeq_abuse for checking for defeq abuses everywhere?

Perhaps #defeq_abuse_implicits, since that setting is specifically about defeqs in implicit arguments?
Or #defeq_abuse +onlyImplicits in.

[thorimur]

For maintainers without context: this PR contributes a diagnostic tool from Kim & their Claude to assist with managing the breaking changes associated with backwards.isDefeq.respectTransparency.

I recommend reading the recent messages in the thread on Zulip for context, but in short:

This is not intended as a feature so much as an adaptation tool for immediate use. So, it’s being held to different standards—but with clear disclaimers to users about this difference-in-standards in the module docstrings and hovers (see the review PR #35843 if it has not been merged into this branch yet), so that it does get confused for a stable user-facing tool.

That difference makes this maintainer delegate quite unusual for a number of reasons:

• the code has not been fully reviewed to work as expected
• the code is not yet sufficiently maintainable
• I myself have contributed a significant refactor to try to take one step towards making it more readable, but this has not been reviewed by someone else

Though, to balance this out for the circumstances, I have:

• made sure there are disclaimers visible which make clear that this is subject to change and should not be relied on in any fashion
• read through it and checked that it is safe to run at a basic level (it does not wipe your hard drive or obviously crash lean)
• reviewed the documentation in the module with public declarations (Lean.MessageData.Trace) and ensured that most declarations are private

Given that it fulfills different obligations than an ordinary meta PR, has time-sensitive value (i.e. it is most useful immediately, while this breakage is still affecting Mathlib), and is flagged to users as experimental/subject to change (and therefore does not make the same promises about behavior or maintainability as ordinary meta code), I think—pending merging #35843 into this branch—that it's reasonable to:



maintainer delegate?

[github-actions]

🚀 Pull request has been placed on the maintainer queue by thorimur.

[thorimur]

Also, please remember to update the PR description and title before merging :)

[Vierkantor]

A cursory glance and this looks good, once the changes of #35843 are merged.

bors d+

[mathlib-bors]

✌️ kim-em can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job