Def Mathlib.Tactic.GCongr.getTransLemma?

Modification history

2025-07-31 09:17

Mathlib/Tactic/GCongr/Core.lean

feat(gcongr): also use more general lemmas, closing extra goals with rfl (#26907) …

Deleted Mathlib.Tactic.GCongr.getTransLemma?View on Github →

2025-06-10 22:11

Mathlib/Tactic/GCongr/Core.lean

feat: let `gcongr` deal with implications (#25534) …

Added Mathlib.Tactic.GCongr.getTransLemma?View on Github →