Structure Mathlib.Tactic.GCongr.State

Modification history

2026-02-27 14:06

Mathlib/Tactic/GCongr/Core.lean

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

Added Mathlib.Tactic.GCongr.State View on Github →