Update src/Init/Data/Bool.lean

leanprover · Feb 23, 2024 · d2466bd · d2466bd
1 parent a8dba5d
commit d2466bd
Showing 1 changed file with 4 additions and 4 deletions.
diff --git 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