Commit 2025-09-16 10:17 b3174e3f

View on Github →

chore: grind annotations in Data/Bool (#29453)

Estimated changes

Modified Mathlib/Data/Bool/Basic.lean

modified theorem Bool.bool_iff_false

modified theorem Bool.coe_xor_iff

modified theorem Bool.dichotomy

modified theorem Bool.eq_false_eq_not_eq_true

modified theorem Bool.eq_false_of_not_eq_true'

modified theorem Bool.eq_true_eq_not_eq_false

modified theorem Bool.eq_true_of_not_eq_false'

modified theorem Bool.false_eq_true_eq_False

modified theorem Bool.not_eq_false_eq_eq_true

modified theorem Bool.not_eq_true_eq_eq_false

added theorem Bool.ofNat_add_one

modified theorem Bool.ofNat_toNat

added theorem Bool.ofNat_zero

modified theorem Bool.or_inr

modified theorem Bool.toNat_beq_zero

modified theorem Bool.true_eq_false_eq_False

Modified Mathlib/Data/Bool/Count.lean

Modified Mathlib/Data/Bool/Set.lean

modified theorem Bool.compl_singleton

modified theorem Bool.range_eq

modified theorem Bool.univ_eq