From ad7d44e201b2d53aaed6211998f3740c4fd0f838 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 10 Dec 2025 16:19:55 +1100 Subject: [PATCH 1/2] feat: `grind_pattern natCast_nonneg` --- src/Init/Grind/Ordered/Ring.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Init/Grind/Ordered/Ring.lean b/src/Init/Grind/Ordered/Ring.lean index cd01ac6ca67b..1b3ce1abc088 100644 --- a/src/Init/Grind/Ordered/Ring.lean +++ b/src/Init/Grind/Ordered/Ring.lean @@ -151,6 +151,11 @@ theorem natCast_le_natCast_of_le (a b : Nat) : a ≤ b → (a : R) ≤ (b : R) : simp [Semiring.natCast_add, Semiring.natCast_one] exact OrderedAdd.add_le_left_iff _ |>.mp ih +theorem natCast_nonneg {a : Nat} : 0 ≤ (a : R) := by + simpa [Semiring.natCast_zero] using natCast_le_natCast_of_le (R := R) _ _ (Nat.zero_le a) + +grind_pattern natCast_nonneg => (a : R) + theorem natCast_lt_natCast_of_lt (a b : Nat) : a < b → (a : R) < (b : R) := by induction a generalizing b <;> cases b <;> simp next n => From 142df231ddbc5a4a02a0a1167a92eb0c004899d7 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 11 Dec 2025 09:24:35 +1100 Subject: [PATCH 2/2] remove grind_pattern, it fires too much, we'll need to do this internally --- src/Init/Grind/Ordered/Ring.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Init/Grind/Ordered/Ring.lean b/src/Init/Grind/Ordered/Ring.lean index 1b3ce1abc088..3bea9e8d0961 100644 --- a/src/Init/Grind/Ordered/Ring.lean +++ b/src/Init/Grind/Ordered/Ring.lean @@ -154,8 +154,6 @@ theorem natCast_le_natCast_of_le (a b : Nat) : a ≤ b → (a : R) ≤ (b : R) : theorem natCast_nonneg {a : Nat} : 0 ≤ (a : R) := by simpa [Semiring.natCast_zero] using natCast_le_natCast_of_le (R := R) _ _ (Nat.zero_le a) -grind_pattern natCast_nonneg => (a : R) - theorem natCast_lt_natCast_of_lt (a b : Nat) : a < b → (a : R) < (b : R) := by induction a generalizing b <;> cases b <;> simp next n =>