Structure Mathlib.Tactic.GCongr.Context

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