chore: bump Std

Mathlib/Algebra/Group/UniqueProds.lean

@@ -533,6 +533,7 @@ theorem _root_.MulEquiv.twoUniqueProds_iff (f : G ≃* H) : TwoUniqueProds G ↔
     simp_rw [mem_product, mem_image, ← filter_nonempty_iff] at h1 h2
     replace h1 := uniqueMul_of_twoUniqueMul ?_ h1.1 h1.2
     replace h2 := uniqueMul_of_twoUniqueMul ?_ h2.1 h2.2
+
     · obtain ⟨a1, ha1, b1, hb1, hu1⟩ := h1
       obtain ⟨a2, ha2, b2, hb2, hu2⟩ := h2
       rw [mem_filter] at ha1 hb1 ha2 hb2
@@ -542,9 +543,10 @@ theorem _root_.MulEquiv.twoUniqueProds_iff (f : G ≃* H) : TwoUniqueProds G ↔
         UniqueMul.of_image_filter (Pi.evalMulHom G i) ha2.2 hb2.2 hi2 hu2⟩
       contrapose! hne; rw [Prod.mk.inj_iff] at hne ⊢
       rw [← ha1.2, ← hb1.2, ← ha2.2, ← hb2.2, hne.1, hne.2]; exact ⟨rfl, rfl⟩
-    all_goals
-      rcases hc with hc | hc; · exact ihA _ (hc.2 _)
-      by_cases hA : A.filter (· i = _) = A; rw [hA]
+    all_goals rcases hc with hc | hc; · exact ihA _ (hc.2 _)
+    · by_cases hA : A.filter (· i = p2.1) = A; rw [hA]
+      exacts [ihB _ (hc.2 _), ihA _ ((A.filter_subset _).ssubset_of_ne hA)]
+    · by_cases hA : A.filter (· i = p1.1) = A; rw [hA]
       exacts [ihB _ (hc.2 _), ihA _ ((A.filter_subset _).ssubset_of_ne hA)]
 
 open ULift in

Mathlib/Data/Int/Bitwise.lean

@@ -193,22 +193,22 @@ theorem bit1_ne_zero (m : ℤ) : bit1 m ≠ 0 := by simpa only [bit0_zero] using
 end deprecated
 
 @[simp]
-theorem testBit_zero (b) : ∀ n, testBit (bit b n) 0 = b
-  | (n : ℕ) => by rw [bit_coe_nat]; apply Nat.testBit_zero
+theorem testBit_bit_zero (b) : ∀ n, testBit (bit b n) 0 = b
+  | (n : ℕ) => by rw [bit_coe_nat]; apply Nat.testBit_bit_zero
   | -[n+1] => by
-    rw [bit_negSucc]; dsimp [testBit]; rw [Nat.testBit_zero]; clear testBit_zero;
+    rw [bit_negSucc]; dsimp [testBit]; rw [Nat.testBit_bit_zero]; clear testBit_bit_zero;
         cases b <;>
       rfl
-#align int.test_bit_zero Int.testBit_zero
+#align int.test_bit_zero Int.testBit_bit_zero
 
 @[simp]
-theorem testBit_succ (m b) : ∀ n, testBit (bit b n) (Nat.succ m) = testBit n m
-  | (n : ℕ) => by rw [bit_coe_nat]; apply Nat.testBit_succ
+theorem testBit_bit_succ (m b) : ∀ n, testBit (bit b n) (Nat.succ m) = testBit n m
+  | (n : ℕ) => by rw [bit_coe_nat]; apply Nat.testBit_bit_succ
   | -[n+1] => by
     dsimp only [testBit]
     simp only [bit_negSucc]
-    cases b <;> simp only [Bool.not_false, Bool.not_true, Nat.testBit_succ]
-#align int.test_bit_succ Int.testBit_succ
+    cases b <;> simp only [Bool.not_false, Bool.not_true, Nat.testBit_bit_succ]
+#align int.test_bit_succ Int.testBit_bit_succ
 
 -- Porting note: TODO
 -- /- ./././Mathport/Syntax/Translate/Expr.lean:333:4: warning: unsupported (TODO): `[tacs] -/

Mathlib/Data/Nat/Bitwise.lean

@@ -199,7 +199,7 @@ theorem zero_of_testBit_eq_false {n : ℕ} (h : ∀ i, testBit n i = false) : n
   induction' n using Nat.binaryRec with b n hn
   · rfl
   · have : b = false := by simpa using h 0
-    rw [this, bit_false, bit0_val, hn fun i => by rw [← h (i + 1), testBit_succ], mul_zero]
+    rw [this, bit_false, bit0_val, hn fun i => by rw [← h (i + 1), testBit_bit_succ], mul_zero]
 #align nat.zero_of_test_bit_eq_ff Nat.zero_of_testBit_eq_false
 
 theorem testBit_eq_false_of_lt {n i} (h : n < 2 ^ i) : n.testBit i = false := by
@@ -214,7 +214,7 @@ theorem testBit_eq_inth (n i : ℕ) : n.testBit i = n.bits.getI i := by
       bodd_eq_bits_head, List.getI_zero_eq_headI]
     cases List.headI (bits n) <;> rfl
   conv_lhs => rw [← bit_decomp n]
-  rw [testBit_succ, ih n.div2, div2_bits_eq_tail]
+  rw [testBit_bit_succ, ih n.div2, div2_bits_eq_tail]
   cases n.bits <;> simp
 #align nat.test_bit_eq_inth Nat.testBit_eq_inth
 
@@ -229,13 +229,13 @@ theorem exists_most_significant_bit {n : ℕ} (h : n ≠ 0) :
     rw [show b = true by
         revert h
         cases b <;> simp]
-    refine' ⟨0, ⟨by rw [testBit_zero], fun j hj => _⟩⟩
+    refine' ⟨0, ⟨by rw [testBit_bit_zero], fun j hj => _⟩⟩
     obtain ⟨j', rfl⟩ := exists_eq_succ_of_ne_zero (ne_of_gt hj)
-    rw [testBit_succ, zero_testBit]
+    rw [testBit_bit_succ, zero_testBit]
   · obtain ⟨k, ⟨hk, hk'⟩⟩ := hn h'
-    refine' ⟨k + 1, ⟨by rw [testBit_succ, hk], fun j hj => _⟩⟩
+    refine' ⟨k + 1, ⟨by rw [testBit_bit_succ, hk], fun j hj => _⟩⟩
     obtain ⟨j', rfl⟩ := exists_eq_succ_of_ne_zero (show j ≠ 0 by intro x; subst x; simp at hj)
-    exact (testBit_succ _ _ _).trans (hk' _ (lt_of_succ_lt_succ hj))
+    exact (testBit_bit_succ _ _ _).trans (hk' _ (lt_of_succ_lt_succ hj))
 #align nat.exists_most_significant_bit Nat.exists_most_significant_bit
 
 theorem lt_of_testBit {n m : ℕ} (i : ℕ) (hn : testBit n i = false) (hm : testBit m i = true)
@@ -248,16 +248,16 @@ theorem lt_of_testBit {n m : ℕ} (i : ℕ) (hn : testBit n i = false) (hm : tes
   · exact False.elim (Bool.false_ne_true ((zero_testBit i).symm.trans hm))
   by_cases hi : i = 0
   · subst hi
-    simp only [testBit_zero] at hn hm
+    simp only [testBit_bit_zero] at hn hm
     have : n = m :=
       eq_of_testBit_eq fun i => by convert hnm (i + 1) (Nat.zero_lt_succ _) using 1
-      <;> rw [testBit_succ]
+      <;> rw [testBit_bit_succ]
     rw [hn, hm, this, bit_false, bit_true, bit0_val, bit1_val]
     exact lt_add_one _
   · obtain ⟨i', rfl⟩ := exists_eq_succ_of_ne_zero hi
-    simp only [testBit_succ] at hn hm
-    have :=
-      hn' _ hn hm fun j hj => by convert hnm j.succ (succ_lt_succ hj) using 1 <;> rw [testBit_succ]
+    simp only [testBit_bit_succ] at hn hm
+    have := hn' _ hn hm fun j hj => by
+      convert hnm j.succ (succ_lt_succ hj) using 1 <;> rw [testBit_bit_succ]
     have this' : 2 * n < 2 * m := Nat.mul_lt_mul' (le_refl _) this two_pos
     cases b <;> cases b'
     <;> simp only [bit_false, bit_true, bit0_val n, bit1_val n, bit0_val m, bit1_val m]
@@ -483,7 +483,7 @@ theorem bitwise_lt {f x y n} (hx : x < 2 ^ n) (hy : y < 2 ^ n) :
       cases n <;> simp_all
 
 lemma shiftLeft_lt {x n m : ℕ} (h : x < 2 ^ n) : x <<< m < 2 ^ (n + m) := by
-  simp only [pow_add, shiftLeft_eq, mul_lt_mul_right (two_pow_pos _), h]
+  simp only [pow_add, shiftLeft_eq, mul_lt_mul_right (Nat.two_pow_pos _), h]
 
 /-- Note that the LHS is the expression used within `Std.BitVec.append`, hence the name. -/
 lemma append_lt {x y n m} (hx : x < 2 ^ n) (hy : y < 2 ^ m) : y <<< n ||| x < 2 ^ (n + m) := by

Mathlib/Data/Nat/Pow.lean

@@ -74,8 +74,6 @@ theorem one_lt_pow (n m : ℕ) (h₀ : n ≠ 0) (h₁ : 1 < m) : 1 < m ^ n := by
   exact Nat.pow_lt_pow_left h₁ h₀
 #align nat.one_lt_pow Nat.one_lt_pow
 
-theorem two_pow_pos (n : ℕ) : 0 < 2^n := Nat.pos_pow_of_pos _ (by decide)
-
 theorem two_pow_succ (n : ℕ) : 2^(n + 1) = 2^n + 2^n := by simp [pow_succ, mul_two]
 
 theorem one_lt_pow' (n m : ℕ) : 1 < (m + 2) ^ (n + 1) :=

Mathlib/Data/Num/Lemmas.lean

@@ -977,11 +977,11 @@ theorem castNum_testBit (m n) : testBit m n = Nat.testBit m n := by
     induction' n with n IH generalizing m <;> cases' m with m m
         <;> dsimp only [PosNum.testBit, Nat.zero_eq]
     · rfl
-    · rw [PosNum.cast_bit1, ← Nat.bit_true, Nat.testBit_zero]
-    · rw [PosNum.cast_bit0, ← Nat.bit_false, Nat.testBit_zero]
-    · rw [PosNum.cast_one', ← bit1_zero, ← Nat.bit_true, Nat.testBit_succ, Nat.zero_testBit]
-    · rw [PosNum.cast_bit1, ← Nat.bit_true, Nat.testBit_succ, IH]
-    · rw [PosNum.cast_bit0, ← Nat.bit_false, Nat.testBit_succ, IH]
+    · rw [PosNum.cast_bit1, ← Nat.bit_true, Nat.testBit_bit_zero]
+    · rw [PosNum.cast_bit0, ← Nat.bit_false, Nat.testBit_bit_zero]
+    · rw [PosNum.cast_one', ← bit1_zero, ← Nat.bit_true, Nat.testBit_bit_succ, Nat.zero_testBit]
+    · rw [PosNum.cast_bit1, ← Nat.bit_true, Nat.testBit_bit_succ, IH]
+    · rw [PosNum.cast_bit0, ← Nat.bit_false, Nat.testBit_bit_succ, IH]
 #align num.test_bit_to_nat Num.castNum_testBit
 
 end Num

Mathlib/Init/Data/Nat/Bitwise.lean

@@ -291,7 +291,7 @@
   fun _ _ _ hk => by simp only [← shiftLeft'_false, shiftLeft'_sub false _ hk]
 
 @[simp]
-theorem testBit_zero (b n) : testBit (bit b n) 0 = b := by
+theorem testBit_bit_zero (b n) : testBit (bit b n) 0 = b := by
   rw [testBit, bit]
   cases b
   · simp [bit0, ← Nat.mul_two]
@@ -307,7 +307,7 @@
   | 1 => rfl
   | n + 2 => by simpa using bodd_eq_and_one_ne_zero n
 
-theorem testBit_succ (m b n) : testBit (bit b n) (succ m) = testBit n m := by
+theorem testBit_bit_succ (m b n) : testBit (bit b n) (succ m) = testBit n m := by
   have : bodd (((bit b n) >>> 1) >>> m) = bodd (n >>> m) := by
     simp only [shiftRight_eq_div_pow]
     simp [← div2_val, div2_bit]

Mathlib/Init/Logic.lean

@@ -632,7 +632,7 @@ end Binary
 #align decidable.not_imp_not Decidable.not_imp_not
 #align decidable.not_or_of_imp Decidable.not_or_of_imp
 #align decidable.imp_iff_not_or Decidable.imp_iff_not_or
-#align decidable.not_imp Decidable.not_imp
+#align decidable.not_imp Decidable.not_imp_iff_and_not
 #align decidable.peirce Decidable.peirce
 #align peirce' peirce'
 #align decidable.not_iff_not Decidable.not_iff_not

Mathlib/Logic/Basic.lean

@@ -439,7 +439,7 @@ theorem imp_or {a b c : Prop} : a → b ∨ c ↔ (a → b) ∨ (a → c) := Dec
 theorem imp_or' : a → b ∨ c ↔ (a → b) ∨ (a → c) := Decidable.imp_or'
 #align imp_or_distrib' imp_or'ₓ -- universes
 
-theorem not_imp : ¬(a → b) ↔ a ∧ ¬b := Decidable.not_imp
+theorem not_imp : ¬(a → b) ↔ a ∧ ¬b := Decidable.not_imp_iff_and_not
 #align not_imp not_imp
 
 theorem peirce (a b : Prop) : ((a → b) → a) → a := Decidable.peirce _ _
@@ -474,12 +474,12 @@ theorem not_and_not_right : ¬(a ∧ ¬b) ↔ a → b := Decidable.not_and_not_r
 
 /-! ### De Morgan's laws -/
 
-#align decidable.not_and_distrib Decidable.not_and
-#align decidable.not_and_distrib' Decidable.not_and'
+#align decidable.not_and_distrib Decidable.not_and_iff_or_not_not
+#align decidable.not_and_distrib' Decidable.not_and_iff_or_not_not
 
 /-- One of **de Morgan's laws**: the negation of a conjunction is logically equivalent to the
 disjunction of the negations. -/
-theorem not_and_or : ¬(a ∧ b) ↔ ¬a ∨ ¬b := Decidable.not_and
+theorem not_and_or : ¬(a ∧ b) ↔ ¬a ∨ ¬b := Decidable.not_and_iff_or_not_not
 #align not_and_distrib not_and_or
 
 #align not_or_distrib not_or

Mathlib/Order/Chain.lean

@@ -183,7 +183,7 @@ theorem IsChain.succ (hs : IsChain r s) : IsChain r (SuccChain r s) :=
 
 theorem IsChain.superChain_succChain (hs₁ : IsChain r s) (hs₂ : ¬IsMaxChain r s) :
     SuperChain r s (SuccChain r s) := by
-  simp only [IsMaxChain, not_and, not_forall, exists_prop, exists_and_left] at hs₂
+  simp only [IsMaxChain, _root_.not_and, not_forall, exists_prop, exists_and_left] at hs₂
   obtain ⟨t, ht, hst⟩ := hs₂ hs₁
   exact succChain_spec ⟨t, hs₁, ht, ssubset_iff_subset_ne.2 hst⟩
 #align is_chain.super_chain_succ_chain IsChain.superChain_succChain

Mathlib/Order/Filter/Basic.lean

@@ -2038,7 +2038,7 @@ theorem eventually_comap : (∀ᶠ a in comap f l, p a) ↔ ∀ᶠ b in l, ∀ a
 
 @[simp]
 theorem frequently_comap : (∃ᶠ a in comap f l, p a) ↔ ∃ᶠ b in l, ∃ a, f a = b ∧ p a := by
-  simp only [Filter.Frequently, eventually_comap, not_exists, not_and]
+  simp only [Filter.Frequently, eventually_comap, not_exists, _root_.not_and]
 #align filter.frequently_comap Filter.frequently_comap
 
 theorem mem_comap_iff_compl : s ∈ comap f l ↔ (f '' sᶜ)ᶜ ∈ l := by

Mathlib/Tactic/Tauto.lean

@@ -37,7 +37,7 @@ def distribNotOnceAt (hypFVar : Expr) (g : MVarId) : MetaM AssertAfterResult :=
   | ~q(¬ (($a : Prop) ∧ $b)) => do
     let h' : Q(¬($a ∧ $b)) := h.toExpr
     let _inst ← synthInstanceQ (q(Decidable $b) : Q(Type))
-    replace q(Decidable.not_and'.mp $h')
+    replace q(Decidable.not_and_iff_or_not_not'.mp $h')
   | ~q(¬ (($a : Prop) ∨ $b)) => do
     let h' : Q(¬($a ∨ $b)) := h.toExpr
     replace q(not_or.mp $h')
@@ -52,7 +52,7 @@ def distribNotOnceAt (hypFVar : Expr) (g : MVarId) : MetaM AssertAfterResult :=
   | ~q(¬ ((($a : Prop)) → $b)) => do
     let h' : Q(¬($a → $b)) := h.toExpr
     let _inst ← synthInstanceQ (q(Decidable $a) : Q(Type))
-    replace q(Decidable.not_imp.mp $h')
+    replace q(Decidable.not_imp_iff_and_not.mp $h')
   | ~q(¬ (($a : Prop) ↔ $b)) => do
     let h' : Q(¬($a ↔ $b)) := h.toExpr
     let _inst ← synthInstanceQ (q(Decidable $b) : Q(Type))

Mathlib/Topology/NoetherianSpace.lean

@@ -251,7 +251,7 @@ theorem NoetherianSpace.exists_open_ne_empty_le_irreducibleComponent [Noetherian
     rintro a -
     by_cases h : a ∈ U
     · exact ⟨U, Set.mem_insert _ _, h⟩
-    · rw [Set.mem_diff, Decidable.not_and, not_not, Set.mem_iUnion] at h
+    · rw [Set.mem_diff, Decidable.not_and_iff_or_not_not, not_not, Set.mem_iUnion] at h
       rcases h with (h|⟨i, hi⟩)
       · refine ⟨irreducibleComponent a, Or.inr ?_, mem_irreducibleComponent⟩
         simp only [Set.mem_diff, Set.mem_singleton_iff]

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "6132dd32b49f17b1d300aba3fb15966e8f489432",
+   "rev": "bdf1213ce28eb4ba30a9a13c8195dcb5095c6d3f",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",