Theorem Mathlib.Tactic.GCongr.lt_imp_lt

Modification history

2025-06-13 14:34
Mathlib/Tactic/GCongr.lean
chore(grewrite): import `gcongr` and `grewrite` in `Tactic.Common` (#25773) …
Deleted Mathlib.Tactic.GCongr.lt_imp_ltView on Github →
2025-06-11 22:43
Mathlib/Tactic/GCongr.lean
feat: a `grw` tactic for rewriting using inequalities (#8167)
Modified Mathlib.Tactic.GCongr.lt_imp_ltView on Github →
2025-06-10 22:11
Mathlib/Tactic/GCongr.lean
feat: let `gcongr` deal with implications (#25534) …
Added Mathlib.Tactic.GCongr.lt_imp_ltView on Github →