Def Mathlib.Tactic.GRewrite.dischargeMain

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.dischargeMainView on Github →