From 8399e6ed4f6a7111b1d0f80e6c042aa402386637 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Wed, 8 Jul 2026 11:05:33 -0400 Subject: [PATCH 1/2] =?UTF-8?q?feat(GRewrite):=20also=20support=20strict?= =?UTF-8?q?=20rewriting=20in=20`=E2=89=A5`/`>`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/Order/Basic.lean | 3 +++ MathlibTest/Tactic/GRewrite.lean | 3 +++ 2 files changed, 6 insertions(+) diff --git a/Mathlib/Order/Basic.lean b/Mathlib/Order/Basic.lean index cff09b9564d8aa..65b1ffe5e9eaca 100644 --- a/Mathlib/Order/Basic.lean +++ b/Mathlib/Order/Basic.lean @@ -191,6 +191,9 @@ theorem gt_imp_gt_of_le_of_le (h₁ : a ≤ c) (h₂ : d ≤ b) : a > b → c > attribute [gcongr strict] lt_of_lt_of_le lt_of_lt_of_le' +@[to_dual (attr := gcongr strict) ge_imp_gt_of_lt'] +theorem ge_imp_gt_of_lt (h : a < b) : a ≥ c → b > c := lt_of_lt_of_le' h + namespace Mathlib.Tactic.GCongr open Lean Meta diff --git a/MathlibTest/Tactic/GRewrite.lean b/MathlibTest/Tactic/GRewrite.lean index 62a69dee5f6a3f..61262fcdc3d11c 100644 --- a/MathlibTest/Tactic/GRewrite.lean +++ b/MathlibTest/Tactic/GRewrite.lean @@ -477,6 +477,9 @@ example (h₁ : a ≤ b) (h₂ : b < c) : a < c := by example (h₁ : a ≤ b) (h₂ : b < c) : a < c := by by_contra!; grw [← h₂, ← h₁] at this; contrapose! this; rfl +example (h₁ : a < b) (h₂ : b ≤ c) : c > a := by + grw [h₁, h₂] + -- Strict inequalities can also be used as non-strict ones: example (h₁ : a < b) (h₂ : b < c) : a ≤ c := by grw [h₁, h₂] From 01c2a28e28c499d6f906df178fadea1b52eb9127 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Wed, 8 Jul 2026 11:06:23 -0400 Subject: [PATCH 2/2] . --- MathlibTest/Tactic/GRewrite.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/MathlibTest/Tactic/GRewrite.lean b/MathlibTest/Tactic/GRewrite.lean index 61262fcdc3d11c..06d0bbc0dad641 100644 --- a/MathlibTest/Tactic/GRewrite.lean +++ b/MathlibTest/Tactic/GRewrite.lean @@ -480,6 +480,9 @@ example (h₁ : a ≤ b) (h₂ : b < c) : a < c := by example (h₁ : a < b) (h₂ : b ≤ c) : c > a := by grw [h₁, h₂] +example (h₁ : a < b) (h₂ : b ≤ c) : c > a := by + grw [← h₂, ← h₁] + -- Strict inequalities can also be used as non-strict ones: example (h₁ : a < b) (h₂ : b < c) : a ≤ c := by grw [h₁, h₂]