From d2466bd56a37eb6ded430a0b52771608f8a37801 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Fri, 23 Feb 2024 11:43:53 +1100 Subject: [PATCH] Update src/Init/Data/Bool.lean --- src/Init/Data/Bool.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean index cb26fa789d1e..e77952c70521 100644 --- a/src/Init/Data/Bool.lean +++ b/src/Init/Data/Bool.lean @@ -223,10 +223,10 @@ theorem toNat_le_one (c:Bool) : c.toNat ≤ 1 := by theorem toNat_lt (b : Bool) : b.toNat < 2 := Nat.lt_succ_of_le (toNat_le_one _) -@[simp] theorem decide_toNat_eq_zero (b : Bool) : decide (b.toNat = 0) = !b := by - cases b <;> rfl -@[simp] theorem decide_toNat_eq_one (b : Bool) : decide (b.toNat = 1) = b := by - cases b <;> rfl +@[simp] theorem toNat_eq_zero (b : Bool) : b.toNat = 0 ↔ b = false := by + cases b <;> simp +@[simp] theorem toNat_eq_one (b : Bool) : b.toNat = 1 ↔ b = true := by + cases b <;> simp end Bool