Commit 2026-03-01 06:36 99520ad2

View on Github →

feat(Tactic): add #defeq_abuse tactic combinator (#35750) 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:
https://github.com/leanprover/lean4/pull/12698 — structured TraceResult field on TraceData
https://github.com/leanprover/lean4/pull/12699 — Meta.synthInstance.apply trace class See https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/backward.2EisDefEq.2ErespectTransparency 🤖 Prepared with Claude Code