[Merged by Bors] - chore(Data/Bool): merge Init.Data.Bool.* into Data.Bool.Basic

Mathlib.lean

@@ -2705,8 +2705,6 @@ import Mathlib.Init.Classical
 import Mathlib.Init.Control.Combinators
 import Mathlib.Init.Control.Lawful
 import Mathlib.Init.Core
-import Mathlib.Init.Data.Bool.Basic
-import Mathlib.Init.Data.Bool.Lemmas
 import Mathlib.Init.Data.Buffer.Parser
 import Mathlib.Init.Data.Fin.Basic
 import Mathlib.Init.Data.Int.Basic

Mathlib/Analysis/BoxIntegral/Basic.lean

@@ -7,7 +7,7 @@ import Mathlib.Analysis.BoxIntegral.Partition.Filter
 import Mathlib.Analysis.BoxIntegral.Partition.Measure
 import Mathlib.Analysis.Oscillation
 import Mathlib.Topology.UniformSpace.Compact
-import Mathlib.Init.Data.Bool.Lemmas
+import Mathlib.Data.Bool.Basic
 
 #align_import analysis.box_integral.basic from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982"
 

Mathlib/Data/Bool/Basic.lean

@@ -21,6 +21,123 @@ bool, boolean, Bool, De Morgan
 
 namespace Bool
 
+#align bor or
+#align band and
+#align bnot not
+#align bxor xor
+
+section
+
+/-!
+This section contains lemmas about booleans which were present in core Lean 3.
+The remainder of this file contains lemmas about booleans from mathlib 3.
+-/
+
+theorem true_eq_false_eq_False : ¬true = false := by decide
+#align tt_eq_ff_eq_false Bool.true_eq_false_eq_False
+
+theorem false_eq_true_eq_False : ¬false = true := by decide
+#align ff_eq_tt_eq_false Bool.false_eq_true_eq_False
+
+theorem eq_false_eq_not_eq_true (b : Bool) : (¬b = true) = (b = false) := by simp
+#align eq_ff_eq_not_eq_tt Bool.eq_false_eq_not_eq_true
+
+theorem eq_true_eq_not_eq_false (b : Bool) : (¬b = false) = (b = true) := by simp
+#align eq_tt_eq_not_eq_ft Bool.eq_true_eq_not_eq_false
+
+theorem eq_false_of_not_eq_true {b : Bool} : ¬b = true → b = false :=
+  Eq.mp (eq_false_eq_not_eq_true b)
+#align eq_ff_of_not_eq_tt Bool.eq_false_of_not_eq_true
+
+theorem eq_true_of_not_eq_false {b : Bool} : ¬b = false → b = true :=
+  Eq.mp (eq_true_eq_not_eq_false b)
+#align eq_tt_of_not_eq_ff Bool.eq_true_of_not_eq_false
+
+theorem and_eq_true_eq_eq_true_and_eq_true (a b : Bool) :
+    ((a && b) = true) = (a = true ∧ b = true) := by simp
+#align band_eq_true_eq_eq_tt_and_eq_tt Bool.and_eq_true_eq_eq_true_and_eq_true
+
+theorem or_eq_true_eq_eq_true_or_eq_true (a b : Bool) :
+    ((a || b) = true) = (a = true ∨ b = true) := by simp
+#align bor_eq_true_eq_eq_tt_or_eq_tt Bool.or_eq_true_eq_eq_true_or_eq_true
+
+theorem not_eq_true_eq_eq_false (a : Bool) : (not a = true) = (a = false) := by cases a <;> simp
+#align bnot_eq_true_eq_eq_ff Bool.not_eq_true_eq_eq_false
+
+#adaptation_note /-- this is no longer a simp lemma,
+  as after nightly-2024-03-05 the LHS simplifies. -/
+theorem and_eq_false_eq_eq_false_or_eq_false (a b : Bool) :
+    ((a && b) = false) = (a = false ∨ b = false) := by
+  cases a <;> cases b <;> simp
+#align band_eq_false_eq_eq_ff_or_eq_ff Bool.and_eq_false_eq_eq_false_or_eq_false
+
+theorem or_eq_false_eq_eq_false_and_eq_false (a b : Bool) :
+    ((a || b) = false) = (a = false ∧ b = false) := by
+  cases a <;> cases b <;> simp
+#align bor_eq_false_eq_eq_ff_and_eq_ff Bool.or_eq_false_eq_eq_false_and_eq_false
+
+theorem not_eq_false_eq_eq_true (a : Bool) : (not a = false) = (a = true) := by cases a <;> simp
+#align bnot_eq_ff_eq_eq_tt Bool.not_eq_false_eq_eq_true
+
+theorem coe_false : ↑false = False := by simp
+#align coe_ff Bool.coe_false
+
+theorem coe_true : ↑true = True := by simp
+#align coe_tt Bool.coe_true
+
+theorem coe_sort_false : (false : Prop) = False := by simp
+#align coe_sort_ff Bool.coe_sort_false
+
+theorem coe_sort_true : (true : Prop) = True := by simp
+#align coe_sort_tt Bool.coe_sort_true
+
+theorem decide_iff (p : Prop) [d : Decidable p] : decide p = true ↔ p := by simp
+#align to_bool_iff Bool.decide_iff
+
+theorem decide_true {p : Prop} [Decidable p] : p → decide p :=
+  (decide_iff p).2
+#align to_bool_true Bool.decide_true
+#align to_bool_tt Bool.decide_true
+
+theorem of_decide_true {p : Prop} [Decidable p] : decide p → p :=
+  (decide_iff p).1
+#align of_to_bool_true Bool.of_decide_true
+
+theorem bool_iff_false {b : Bool} : ¬b ↔ b = false := by cases b <;> decide
+#align bool_iff_false Bool.bool_iff_false
+
+theorem bool_eq_false {b : Bool} : ¬b → b = false :=
+  bool_iff_false.1
+#align bool_eq_false Bool.bool_eq_false
+
+theorem decide_false_iff (p : Prop) {_ : Decidable p} : decide p = false ↔ ¬p :=
+  bool_iff_false.symm.trans (not_congr (decide_iff _))
+#align to_bool_ff_iff Bool.decide_false_iff
+
+theorem decide_false {p : Prop} [Decidable p] : ¬p → decide p = false :=
+  (decide_false_iff p).2
+#align to_bool_ff Bool.decide_false
+
+theorem of_decide_false {p : Prop} [Decidable p] : decide p = false → ¬p :=
+  (decide_false_iff p).1
+#align of_to_bool_ff Bool.of_decide_false
+
+theorem decide_congr {p q : Prop} [Decidable p] [Decidable q] (h : p ↔ q) : decide p = decide q :=
+  decide_eq_decide.mpr h
+#align to_bool_congr Bool.decide_congr
+
+@[deprecated (since := "2024-06-07")] alias coe_or_iff := or_eq_true_iff
+#align bor_coe_iff Bool.or_eq_true_iff
+
+@[deprecated (since := "2024-06-07")] alias coe_and_iff := and_eq_true_iff
+#align band_coe_iff Bool.and_eq_true_iff
+
+theorem coe_xor_iff (a b : Bool) : xor a b ↔ Xor' (a = true) (b = true) := by
+  cases a <;> cases b <;> decide
+#align bxor_coe_iff Bool.coe_xor_iff
+
+end
+
 @[deprecated (since := "2024-06-07")] alias decide_True := decide_true_eq_true
 #align bool.to_bool_true decide_true_eq_true
 

Mathlib/Logic/Equiv/Basic.lean

@@ -12,6 +12,7 @@ import Mathlib.Data.Sum.Basic
 import Mathlib.Init.Data.Sigma.Basic
 import Mathlib.Logic.Equiv.Defs
 import Mathlib.Logic.Function.Conjugate
+import Mathlib.Tactic.Coe
 import Mathlib.Tactic.Lift
 import Mathlib.Tactic.Convert
 import Mathlib.Tactic.Contrapose

Mathlib/Logic/Equiv/Defs.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura, Mario Carneiro
 -/
 import Mathlib.Data.FunLike.Equiv
 import Mathlib.Data.Quot
-import Mathlib.Init.Data.Bool.Lemmas
+import Mathlib.Data.Bool.Basic
 import Mathlib.Logic.Unique
 import Mathlib.Tactic.Substs
 import Mathlib.Tactic.Conv

Mathlib/Order/Monotone/Basic.lean

@@ -8,6 +8,7 @@ import Mathlib.Init.Data.Int.Order
 import Mathlib.Order.Compare
 import Mathlib.Order.Max
 import Mathlib.Order.RelClasses
+import Mathlib.Tactic.Coe
 import Mathlib.Tactic.Choose
 
 #align_import order.monotone.basic from "leanprover-community/mathlib"@"554bb38de8ded0dafe93b7f18f0bfee6ef77dc5d"

Mathlib/Topology/Category/Profinite/Nobeling.lean

@@ -7,7 +7,7 @@ import Mathlib.Algebra.Category.ModuleCat.Free
 import Mathlib.Topology.Category.Profinite.CofilteredLimit
 import Mathlib.Topology.Category.Profinite.Product
 import Mathlib.Topology.LocallyConstant.Algebra
-import Mathlib.Init.Data.Bool.Lemmas
+import Mathlib.Data.Bool.Basic
 
 /-!
 

scripts/noshake.json

@@ -289,7 +289,7 @@
   "Mathlib.NumberTheory.ArithmeticFunction": ["Mathlib.Tactic.ArithMult"],
   "Mathlib.MeasureTheory.MeasurableSpace.Defs": ["Mathlib.Tactic.FunProp.Attr"],
   "Mathlib.Logic.Nontrivial.Defs": ["Mathlib.Init.Logic"],
-  "Mathlib.Logic.Equiv.Defs": ["Mathlib.Init.Data.Bool.Lemmas"],
+  "Mathlib.Logic.Equiv.Defs": ["Mathlib.Data.Bool.Basic"],
   "Mathlib.LinearAlgebra.Matrix.Transvection": ["Mathlib.Data.Matrix.DMatrix"],
   "Mathlib.LinearAlgebra.Basic": ["Mathlib.Algebra.BigOperators.Group.Finset"],
   "Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional": ["Mathlib.Init.Core"],
@@ -303,7 +303,6 @@
   "Mathlib.Init.Data.Nat.GCD": ["Batteries.Data.Nat.Gcd"],
   "Mathlib.Init.Data.List.Basic": ["Batteries.Data.List.Basic"],
   "Mathlib.Init.Data.Int.Basic": ["Batteries.Data.Int.Order"],
-  "Mathlib.Init.Data.Bool.Lemmas": ["Mathlib.Tactic.AdaptationNote"],
   "Mathlib.GroupTheory.MonoidLocalization": ["Mathlib.Init.Data.Prod"],
   "Mathlib.Geometry.Manifold.Sheaf.Smooth":
   ["Mathlib.CategoryTheory.Sites.Whiskering"],