From ef71f0beabddd0dd272ea55e294d1f2535408195 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 28 Sep 2024 14:55:15 +1000 Subject: [PATCH] chore: restore @[simp] to upstreamed Nat.lt_off_iff (#5503) This was upstreamed from Mathlib in #5478, but leaving off the `@[simp]` attribute, thereby breaking Mathlib. (We could of course add the simp attribute back in Mathlib, but wherever it lives it should have been in place at the time we merged -- this way I have to add it temporarily in Mathlib and then remove it again once it is redundant.) --- src/Init/Data/Nat/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index 93a17538ff..bbfe76ceda 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -634,7 +634,7 @@ theorem lt_succ_of_lt (h : a < b) : a < succ b := le_succ_of_le h theorem lt_add_one_of_lt (h : a < b) : a < b + 1 := le_succ_of_le h -theorem lt_one_iff : n < 1 ↔ n = 0 := Nat.lt_succ_iff.trans <| by rw [le_zero_eq] +@[simp] theorem lt_one_iff : n < 1 ↔ n = 0 := Nat.lt_succ_iff.trans <| by rw [le_zero_eq] theorem succ_pred_eq_of_ne_zero : ∀ {n}, n ≠ 0 → succ (pred n) = n | _+1, _ => rfl