Def Mathlib.Tactic.Erw?.extractRewriteEq

Modification history

2025-02-11 15:35
Mathlib/Tactic/ErwQuestion.lean
feat: `erw?`, a tool to explain why `erw` is necessary (#21643) …
Added Mathlib.Tactic.Erw?.extractRewriteEqView on Github →