chore: bump std (#2156)

Mathlib/Data/Bool/Basic.lean

@@ -74,10 +74,7 @@ theorem decide_or (p q : Prop) [Decidable p] [Decidable q] : decide (p ∨ q) =
   by_cases p <;> by_cases q <;> simp [*]
 #align bool.to_bool_or Bool.decide_or
 
-@[simp]
-theorem decide_eq {p q : Prop} [Decidable p] [Decidable q] : decide p = decide q ↔ (p ↔ q) :=
-  ⟨fun h ↦ (coe_decide p).symm.trans <| by simp [h], decide_congr⟩
-#align bool.to_bool_eq Bool.decide_eq
+#align bool.to_bool_eq decide_eq_decide
 
 theorem not_false' : ¬false := fun.
 #align bool.not_ff Bool.not_false'

Mathlib/Data/Option/Basic.lean

@@ -104,11 +104,6 @@ theorem bind_eq_bind {α β : Type _} {f : α → Option β} {x : Option α} : x
   rfl
 #align option.bind_eq_bind Option.bind_eq_bind
 
---Porting note: New lemma used to prove a theorem in Data.List.Basic
-theorem map_eq_bind (f : α → β) (o : Option α) :
-  Option.map f o = Option.bind o (some ∘ f) := by
-  cases o <;> rfl
-
 theorem map_coe {α β} {a : α} {f : α → β} : f <$> (a : Option α) = ↑(f a) :=
   rfl
 #align option.map_coe Option.map_coe

Mathlib/Logic/Basic.lean

@@ -661,9 +661,6 @@ theorem exists_swap {p : α → β → Prop} : (∃ x y, p x y) ↔ ∃ y x, p x
   ⟨fun ⟨x, y, h⟩ ↦ ⟨y, x, h⟩, fun ⟨y, x, h⟩ ↦ ⟨x, y, h⟩⟩
 #align exists_swap exists_swap
 
-@[simp] theorem forall_exists_index {q : (∃ x, p x) → Prop} :
-    (∀ h, q h) ↔ ∀ x (h : p x), q ⟨x, h⟩ :=
-  ⟨fun h x hpx ↦ h ⟨x, hpx⟩, fun h ⟨x, hpx⟩ ↦ h x hpx⟩
 #align forall_exists_index forall_exists_index
 
 #align exists_imp_distrib exists_imp

lake-manifest.json

@@ -10,12 +10,12 @@
   {"git":
    {"url": "https://github.com/JLimperg/aesop",
     "subDir?": null,
-    "rev": "ccff5d4ae7411c5fe741f3139950e8bddf353dea",
+    "rev": "ba61f7fec6174d8c7d2796457da5a8d0b0da44c6",
     "name": "aesop",
     "inputRev?": "master"}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "14ac0a9637e10d36e05544e84baf56e76dd6adf8",
+    "rev": "de7e2a79905a3f87cad1ad5bf57045206f9738c7",
     "name": "std",
     "inputRev?": "main"}}]}