Def Mathlib.Tactic.finishElabGRewrite

Modification history

2026-06-07 02:12
Mathlib/Tactic/GRewrite/Elab.lean
feat(GRewrite): new `grw` implementation (#38318) …
Deleted Mathlib.Tactic.finishElabGRewriteView on Github →
2026-04-29 09:12
Mathlib/Tactic/GRewrite/Elab.lean
chore(GRewrite): copy how `rw` elaborates (#38558) …
Added Mathlib.Tactic.finishElabGRewriteView on Github →