Merge master into nightly-testing

Mathlib/Analysis/BoxIntegral/Basic.lean

@@ -819,8 +819,8 @@ theorem HasIntegral.of_le_Henstock_of_forall_isLittleO (hl : l ≤ Henstock) (B
       ∃ δ > 0, ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x δ → x ∈ Box.Icc J →
         (l.bDistortion → J.distortion ≤ c) → dist (vol J (f x)) (g J) ≤ ε * B J) :
     HasIntegral I l f vol (g I) :=
-  have A : l.bHenstock := hl.2.1.resolve_left (by decide)
-  HasIntegral.of_bRiemann_eq_false_of_forall_isLittleO (hl.1.resolve_right (by decide)) B hB0 _ s hs
+  have A : l.bHenstock := Bool.eq_true_of_true_le hl.2.1
+  HasIntegral.of_bRiemann_eq_false_of_forall_isLittleO (Bool.eq_false_of_le_false hl.1) B hB0 _ s hs
     (fun _ => A) H₁ <| by simpa only [A, true_imp_iff] using H₂
 set_option linter.uppercaseLean3 false in
 #align box_integral.has_integral_of_le_Henstock_of_forall_is_o BoxIntegral.HasIntegral.of_le_Henstock_of_forall_isLittleO

Mathlib/Data/Bool/Basic.lean

@@ -145,12 +145,8 @@ theorem eq_true_of_ne_false : ∀ {a : Bool}, a ≠ false → a = true := by dec
 theorem eq_false_of_ne_true : ∀ {a : Bool}, a ≠ true → a = false := by decide
 #align bool.eq_ff_of_ne_tt Bool.eq_false_of_ne_true
 
-theorem or_comm : ∀ a b, (a || b) = (b || a) := by decide
 #align bool.bor_comm Bool.or_comm
-
 #align bool.bor_assoc Bool.or_assoc
-
-theorem or_left_comm : ∀ a b c, (a || (b || c)) = (b || (a || c)) := by decide
 #align bool.bor_left_comm Bool.or_left_comm
 
 theorem or_inl {a b : Bool} (H : a) : a || b := by simp [H]
@@ -159,12 +155,8 @@ theorem or_inl {a b : Bool} (H : a) : a || b := by simp [H]
 theorem or_inr {a b : Bool} (H : b) : a || b := by cases a <;> simp [H]
 #align bool.bor_inr Bool.or_inr
 
-theorem and_comm : ∀ a b, (a && b) = (b && a) := by decide
 #align bool.band_comm Bool.and_comm
-
 #align bool.band_assoc Bool.and_assoc
-
-theorem and_left_comm : ∀ a b c, (a && (b && c)) = (b && (a && c)) := by decide
 #align bool.band_left_comm Bool.and_left_comm
 
 theorem and_elim_left : ∀ {a b : Bool}, a && b → a := by decide
@@ -176,22 +168,10 @@ theorem and_intro : ∀ {a b : Bool}, a → b → a && b := by decide
 theorem and_elim_right : ∀ {a b : Bool}, a && b → b := by decide
 #align bool.band_elim_right Bool.and_elim_right
 
-theorem and_or_distrib_left (a b c : Bool) : (a && (b || c)) = (a && b || a && c) := by
-  cases a <;> simp
 #align bool.band_bor_distrib_left Bool.and_or_distrib_left
-
-theorem and_or_distrib_right (a b c : Bool) : ((a || b) && c) = (a && c || b && c) := by
-  cases a <;> cases b <;> cases c <;> simp
 #align bool.band_bor_distrib_right Bool.and_or_distrib_right
-
-theorem or_and_distrib_left (a b c : Bool) : (a || b && c) = ((a || b) && (a || c)) := by
-  cases a <;> simp
 #align bool.bor_band_distrib_left Bool.or_and_distrib_left
-
-theorem or_and_distrib_right (a b c : Bool) : (a && b || c) = ((a || c) && (b || c)) := by
-  cases a <;> cases b <;> cases c <;> simp
 #align bool.bor_band_distrib_right Bool.or_and_distrib_right
-
 #align bool.bnot_ff Bool.not_false
 #align bool.bnot_tt Bool.not_true
 
@@ -241,107 +221,66 @@ theorem eq_false_of_not_eq_true' {a : Bool} : !a = true → a = false := by
   cases a <;> decide
 #align bool.eq_ff_of_bnot_eq_tt Bool.eq_false_of_not_eq_true'
 
-@[simp]
-theorem and_not_self : ∀ x, (x && !x) = false := by decide
+-- TODO: undo the rename in leanprover/std4#183?
+alias and_not_self := and_not_self_right
 #align bool.band_bnot_self Bool.and_not_self
 
-@[simp]
-theorem not_and_self : ∀ x, (!x && x) = false := by decide
+-- TODO: undo the rename in leanprover/std4#183?
+alias not_and_self := and_not_self_left
 #align bool.bnot_band_self Bool.not_and_self
 
-@[simp]
-theorem or_not_self : ∀ x, (x || !x) = true := by decide
+-- TODO: undo the rename in leanprover/std4#183?
+alias or_not_self := or_not_self_right
 #align bool.bor_bnot_self Bool.or_not_self
 
-@[simp]
-theorem not_or_self : ∀ x, (!x || x) = true := by decide
+-- TODO: undo the rename in leanprover/std4#183?
+alias not_or_self := or_not_self_left
 #align bool.bnot_bor_self Bool.not_or_self
 
 theorem bne_eq_xor : bne = xor := by funext a b; revert a b; decide
 
-theorem xor_comm : ∀ a b, xor a b = xor b a := by decide
 #align bool.bxor_comm Bool.xor_comm
 
-@[simp]
-theorem xor_assoc : ∀ a b c, xor (xor a b) c = xor a (xor b c) := by decide
+attribute [simp] xor_assoc
 #align bool.bxor_assoc Bool.xor_assoc
 
-theorem xor_left_comm : ∀ a b c, xor a (xor b c) = xor b (xor a c) := by decide
 #align bool.bxor_left_comm Bool.xor_left_comm
-
-@[simp]
-theorem xor_not_left : ∀ a, xor (!a) a = true := by decide
 #align bool.bxor_bnot_left Bool.xor_not_left
-
-@[simp]
-theorem xor_not_right : ∀ a, xor a (!a) = true := by decide
 #align bool.bxor_bnot_right Bool.xor_not_right
 
-@[simp]
-theorem xor_not_not : ∀ a b, xor (!a) (!b) = xor a b := by decide
+attribute [simp] xor_not_not
 #align bool.bxor_bnot_bnot Bool.xor_not_not
 
-@[simp]
-theorem xor_false_left : ∀ a, xor false a = a := by decide
 #align bool.bxor_ff_left Bool.xor_false_left
-
-@[simp]
-theorem xor_false_right : ∀ a, xor a false = a := by decide
 #align bool.bxor_ff_right Bool.xor_false_right
-
-theorem and_xor_distrib_left (a b c : Bool) : (a && xor b c) = xor (a && b) (a && c) := by
-  cases a <;> simp
 #align bool.band_bxor_distrib_left Bool.and_xor_distrib_left
-
-theorem and_xor_distrib_right (a b c : Bool) : (xor a b && c) = xor (a && c) (b && c) := by
-  cases a <;> cases b <;> cases c <;> simp
 #align bool.band_bxor_distrib_right Bool.and_xor_distrib_right
 
 theorem xor_iff_ne : ∀ {x y : Bool}, xor x y = true ↔ x ≠ y := by decide
 #align bool.bxor_iff_ne Bool.xor_iff_ne
 
 /-! ### De Morgan's laws for booleans-/
 
-@[simp]
-theorem not_and : ∀ a b : Bool, (!(a && b)) = (!a || !b) := by decide
+attribute [simp] not_and
 #align bool.bnot_band Bool.not_and
 
-@[simp]
-theorem not_or : ∀ a b : Bool, (!(a || b)) = (!a && !b) := by decide
+attribute [simp] not_or
 #align bool.bnot_bor Bool.not_or
 
-theorem not_inj : ∀ {a b : Bool}, (!a) = !b → a = b := by decide
 #align bool.bnot_inj Bool.not_inj
 
--- Porting note: having to unfold here is not pretty.
--- There is a discussion on zulip about this at
--- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/LinearOrder.20in.20mathlib3.2F4/near/308228493
 instance linearOrder : LinearOrder Bool where
-  le := fun a b ↦ a = false ∨ b = true
-  le_refl := by unfold LE.le; decide
-  le_trans := by unfold LE.le; decide
-  le_antisymm := by unfold LE.le Preorder.toLE; decide
-  le_total := by unfold LE.le Preorder.toLE PartialOrder.toPreorder; decide
-  decidableLE := by unfold LE.le Preorder.toLE PartialOrder.toPreorder; exact inferInstance
-  decidableEq := inferInstance
-  max := or
-  max_def := λ a b => by cases a <;> cases b <;> decide
-  min := and
-  min_def := λ a b => by cases a <;> cases b <;> decide
+  le_refl := Bool.le_refl
+  le_trans _ _ _ := Bool.le_trans
+  le_antisymm _ _ := Bool.le_antisymm
+  le_total := Bool.le_total
+  decidableLE := inferInstance
+  lt_iff_le_not_le _ _ := Bool.lt_iff_le_not_le
 #align bool.linear_order Bool.linearOrder
 
-@[simp] theorem max_eq_or : max = or := rfl
-
-@[simp] theorem min_eq_and : min = and := rfl
+attribute [simp] Bool.max_eq_or Bool.min_eq_and
 
-@[simp]
-theorem false_le {x : Bool} : false ≤ x :=
-  Or.intro_left _ rfl
 #align bool.ff_le Bool.false_le
-
-@[simp]
-theorem le_true {x : Bool} : x ≤ true :=
-  Or.intro_right _ rfl
 #align bool.le_tt Bool.le_true
 
 theorem lt_iff : ∀ {x y : Bool}, x < y ↔ x = false ∧ y = true := by decide
@@ -386,17 +325,15 @@ def ofNat (n : Nat) : Bool :=
 theorem ofNat_le_ofNat {n m : Nat} (h : n ≤ m) : ofNat n ≤ ofNat m := by
   simp only [ofNat, ne_eq, _root_.decide_not]
   cases Nat.decEq n 0 with
-  | isTrue hn => rw [decide_eq_true hn]; exact false_le
+  | isTrue hn => rw [decide_eq_true hn]; exact Bool.false_le _
   | isFalse hn =>
     cases Nat.decEq m 0 with
-    | isFalse hm => rw [decide_eq_false hm]; exact le_true
+    | isFalse hm => rw [decide_eq_false hm]; exact Bool.le_true _
     | isTrue hm => subst hm; have h := le_antisymm h (Nat.zero_le n); contradiction
 #align bool.of_nat_le_of_nat Bool.ofNat_le_ofNat
 
 theorem toNat_le_toNat {b₀ b₁ : Bool} (h : b₀ ≤ b₁) : toNat b₀ ≤ toNat b₁ := by
-  cases h with
-  | inl h => subst h; exact Nat.zero_le _
-  | inr h => subst h; cases b₀ <;> simp
+  cases b₀ <;> cases b₁ <;> simp_all
 #align bool.to_nat_le_to_nat Bool.toNat_le_toNat
 
 theorem ofNat_toNat (b : Bool) : ofNat (toNat b) = b := by

Mathlib/Init/Data/Bool/Basic.lean

@@ -4,24 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Mathlib.Mathport.Rename
+import Std.Data.Bool
 
 /-!
 # Boolean operations
 
-In Lean 3 this file also contained the definitions of `cond`, `bor`, `band` and `bnot`,
-the boolean functions. These are in Lean 4 core (as `cond`, `or`, `and` and `not`), but
-apparently `xor` didn't make the cut.
-
+In Lean 3 this file contained the definitions of `cond`, `bor`, `band` and `bnot`,
+the boolean functions. These are now in Lean 4 core or Std (as `cond`, `or`, `and`, `not`, `xor`).
 -/
 
 #align bor or
 #align band and
 #align bnot not
-
-/-- Boolean XOR -/
-@[inline]
-def xor : Bool → Bool → Bool
-  | true, false => true
-  | false, true => true
-  | _, _ => false
 #align bxor xor

Mathlib/Init/Data/Bool/Lemmas.lean

@@ -47,19 +47,18 @@ namespace Bool
 theorem cond_self.{u} {α : Type u} (b : Bool) (a : α) : cond b a a = a := by cases b <;> rfl
 #align cond_a_a Bool.cond_self
 
-@[simp]
-theorem xor_self (b : Bool) : xor b b = false := by cases b <;> simp
+attribute [simp] xor_self
 #align bxor_self Bool.xor_self
 
-@[simp]
-theorem xor_true (b : Bool) : xor b true = not b := by cases b <;> simp
+-- TODO: undo the rename in leanprover/std4#183?
+alias xor_true := xor_true_right
 #align bxor_tt Bool.xor_true
 
 theorem xor_false (b : Bool) : xor b false = b := by cases b <;> simp
 #align bxor_ff Bool.xor_false
 
-@[simp]
-theorem true_xor (b : Bool) : xor true b = not b := by cases b <;> simp
+-- TODO: undo the rename in leanprover/std4#183?
+alias true_xor := xor_true_left
 #align tt_bxor Bool.true_xor
 
 theorem false_xor (b : Bool) : xor false b = b := by cases b <;> simp
@@ -167,7 +166,6 @@ theorem coe_or_iff (a b : Bool) : a || b ↔ a ∨ b := by simp
 theorem coe_and_iff (a b : Bool) : a && b ↔ a ∧ b := by simp
 #align band_coe_iff Bool.coe_and_iff
 
-@[simp]
 theorem coe_xor_iff (a b : Bool) : xor a b ↔ Xor' (a = true) (b = true) := by
   cases a <;> cases b <;> exact by decide
 #align bxor_coe_iff Bool.coe_xor_iff

Mathlib/Init/Data/Nat/Bitwise.lean

@@ -73,10 +73,7 @@ theorem bodd_succ (n : ℕ) : bodd (succ n) = not (bodd n) := by
 
 @[simp]
 theorem bodd_add (m n : ℕ) : bodd (m + n) = bxor (bodd m) (bodd n) := by
-  induction' n with n IH
-  · simp
-  · simp [add_succ, IH]
-    cases bodd m <;> cases bodd n <;> rfl
+  induction n <;> simp_all [add_succ]
 #align nat.bodd_add Nat.bodd_add
 
 @[simp]

Mathlib/Order/BoundedOrder.lean

@@ -942,9 +942,9 @@ open Bool
 
 instance Bool.boundedOrder : BoundedOrder Bool where
   top := true
-  le_top _ := le_true
+  le_top := Bool.le_true
   bot := false
-  bot_le _ := false_le
+  bot_le := Bool.false_le
 
 @[simp]
 theorem top_eq_true : ⊤ = true :=

lake-manifest.json

@@ -40,5 +40,13 @@
     "opts": {},
     "name": "proofwidgets",
     "inputRev?": "v0.0.21",
+    "inherited": false}},
+  {"git":
+   {"url": "https://github.com/leanprover/std4",
+    "subDir?": null,
+    "rev": "0da0e81a141cd26364f8799fb31ae7866ec43fb7",
+    "opts": {},
+    "name": "std",
+    "inputRev?": "main",
     "inherited": false}}],
  "name": "mathlib"}