Commit 2026-02-27 14:06 243a7e8e
View on Github →chore: refactor Lean.MVarId.gcongr to use a monad (#35478)
This PR refactors the implementation of the gcongr tactic to use its own monad. This will make it easier to refactor/maintain/read the code.