Def Mathlib.Tactic.GCongr.GCongrM.run

Modification history

2026-04-21 11:43

Mathlib/Tactic/GCongr/Core.lean

feat(gcongr): support `rintro` patterns (#36314) …

Modified Mathlib.Tactic.GCongr.GCongrM.run View on Github →

2026-02-27 14:06

Mathlib/Tactic/GCongr/Core.lean

chore: refactor `Lean.MVarId.gcongr` to use a monad (#35478) …

Added Mathlib.Tactic.GCongr.GCongrM.run View on Github →