Def Mathlib.Tactic.DefEqAbuse.reportDefEqAbuse

Modification history

2026-03-01 06:36

Mathlib/Tactic/DefEqAbuse.lean

feat(Tactic): add `#defeq_abuse` tactic combinator (#35750) …

Added Mathlib.Tactic.DefEqAbuse.reportDefEqAbuse View on Github →