Theorem Mathlib.Tactic.GCongr.imp_mono

Modification history

2026-09-13 13:07
Mathlib/Tactic/GCongr.lean
chore(Tactic/GCongr): deprecate `Tactic/GCongr/CoreAttrs` (#43594) …
Modified Mathlib.Tactic.GCongr.imp_monoView on Github →
2026-05-05 08:39
Mathlib/Tactic/GCongr/CoreAttrs.lean
feat(GCongr): `applyRflOrId` (#38556) …
Added Mathlib.Tactic.GCongr.imp_monoView on Github →