Structure Mathlib.Tactic.GRewrite.Config

Modification history

2025-06-11 22:43

Mathlib/Tactic/GRewrite/Core.lean

feat: a `grw` tactic for rewriting using inequalities (#8167)

Added Mathlib.Tactic.GRewrite.Config View on Github →