Commit 2026-05-14 12:20 a148c498

View on Github →

fix(Data/Bool/Basic): fix parentheses of !a = b (#38539) Fix three lemmas which have a subterm of the form !a = b, which elaborates to (!(decide (a = b))) = true, where (!a) = b was probably intended. These were introduced in #534.

Estimated changes

Modified Mathlib/Data/Bool/Basic.lean

modified theorem Bool.eq_false_of_not_eq_true'

modified theorem Bool.eq_true_of_not_eq_false'

modified theorem Bool.not_eq_iff