Def Mathlib.Tactic.GCongr.updateRel

Modification history

2025-11-13 17:14

Mathlib/Tactic/GCongr/Core.lean

feat(gcongr): use mdata instead of template (#30739) …

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