Commit 2024-07-16 14:28 2f6e35a7

View on Github →

chore(Data/Bool): merge Init.Data.Bool.* into Data.Bool.Basic (#14769)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/BoxIntegral/Basic.lean

Modified Mathlib/Data/Bool/Basic.lean

added theorem Bool.and_eq_false_eq_eq_false_or_eq_false

added theorem Bool.and_eq_true_eq_eq_true_and_eq_true

added theorem Bool.bool_eq_false

added theorem Bool.bool_iff_false

added theorem Bool.coe_false

added theorem Bool.coe_sort_false

added theorem Bool.coe_sort_true

added theorem Bool.coe_true

added theorem Bool.coe_xor_iff

added theorem Bool.decide_congr

added theorem Bool.decide_false

added theorem Bool.decide_false_iff

added theorem Bool.decide_iff

added theorem Bool.decide_true

added theorem Bool.eq_false_eq_not_eq_true

added theorem Bool.eq_false_of_not_eq_true

added theorem Bool.eq_true_eq_not_eq_false

added theorem Bool.eq_true_of_not_eq_false

added theorem Bool.false_eq_true_eq_False

added theorem Bool.not_eq_false_eq_eq_true

added theorem Bool.not_eq_true_eq_eq_false

added theorem Bool.of_decide_false

added theorem Bool.of_decide_true

added theorem Bool.or_eq_false_eq_eq_false_and_eq_false

added theorem Bool.or_eq_true_eq_eq_true_or_eq_true

added theorem Bool.true_eq_false_eq_False

Deleted Mathlib/Init/Data/Bool/Basic.lean

Deleted Mathlib/Init/Data/Bool/Lemmas.lean

deleted theorem Bool.and_eq_false_eq_eq_false_or_eq_false

deleted theorem Bool.and_eq_true_eq_eq_true_and_eq_true

deleted theorem Bool.bool_eq_false

deleted theorem Bool.bool_iff_false

deleted theorem Bool.coe_false

deleted theorem Bool.coe_sort_false

deleted theorem Bool.coe_sort_true

deleted theorem Bool.coe_true

deleted theorem Bool.coe_xor_iff

deleted theorem Bool.decide_congr

deleted theorem Bool.decide_false

deleted theorem Bool.decide_false_iff

deleted theorem Bool.decide_iff

deleted theorem Bool.decide_true

deleted theorem Bool.eq_false_eq_not_eq_true

deleted theorem Bool.eq_false_of_not_eq_true

deleted theorem Bool.eq_true_eq_not_eq_false

deleted theorem Bool.eq_true_of_not_eq_false

deleted theorem Bool.false_eq_true_eq_False

deleted theorem Bool.not_eq_false_eq_eq_true

deleted theorem Bool.not_eq_true_eq_eq_false

deleted theorem Bool.of_decide_false

deleted theorem Bool.of_decide_true

deleted theorem Bool.or_eq_false_eq_eq_false_and_eq_false

deleted theorem Bool.or_eq_true_eq_eq_true_or_eq_true

deleted theorem Bool.true_eq_false_eq_False

Modified Mathlib/Logic/Equiv/Basic.lean

Modified Mathlib/Logic/Equiv/Defs.lean

Modified Mathlib/Order/Monotone/Basic.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling.lean

Modified scripts/noshake.json