Def Lean.MVarId.gcongrForward

Modification history

2025-11-13 17:14
Mathlib/Tactic/GCongr/Core.lean
feat(gcongr): use mdata instead of template (#30739) …
Modified Lean.MVarId.gcongrForwardView on Github →
2023-06-05 08:37
Mathlib/Tactic/GCongr/Core.lean
feat: tactic `gcongr` for "relational congruence" (#3965) …
Added Lean.MVarId.gcongrForwardView on Github →