Def Mathlib.Tactic.Erw?.extractRewriteHypEq

Modification history

2025-08-04 12:20

Mathlib/Tactic/ErwQuestion.lean

feat: `erw?` supports all arguments that `erw` does (#27751) …

Added Mathlib.Tactic.Erw?.extractRewriteHypEq View on Github →