chore: bump std to leanprover/lean4#429 (#8990)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

Mathlib/Data/List/Perm.lean

@@ -229,14 +229,9 @@ lemma subperm_iff : l₁ <+~ l₂ ↔ ∃ l, l ~ l₂ ∧ l₁ <+ l := by
   obtain ⟨l', h₂⟩ := h₂.exists_perm_append
   exact ⟨l₁ ++ l', (h₂.trans (h₁.append_right _)).symm, (prefix_append _ _).sublist⟩
 
--- This is now in `Std`, but apparently misnamed as `List.subperm_singleton_iff`.
-lemma singleton_subperm_iff : [a] <+~ l ↔ a ∈ l :=
-  ⟨fun ⟨s, hla, h⟩ ↦ by rwa [perm_singleton.1 hla, singleton_sublist] at h,
-    fun h ↦ ⟨[a], perm_rfl, singleton_sublist.2 h⟩⟩
 #align list.subperm_singleton_iff List.singleton_subperm_iff
 
--- The prime could be removed if `List.subperm_singleton_iff` is renamed in Std.
-@[simp] lemma subperm_singleton_iff' : l <+~ [a] ↔ l = [] ∨ l = [a] := by
+@[simp] lemma subperm_singleton_iff : l <+~ [a] ↔ l = [] ∨ l = [a] := by
   constructor
   · rw [subperm_iff]
     rintro ⟨s, hla, h⟩

Mathlib/Data/Multiset/Basic.lean

@@ -621,7 +621,7 @@ theorem singleton_le {a : α} {s : Multiset α} : {a} ≤ s ↔ a ∈ s :=
 
 @[simp] lemma le_singleton : s ≤ {a} ↔ s = 0 ∨ s = {a} :=
   Quot.induction_on s fun l ↦ by simp only [cons_zero, ← coe_singleton, quot_mk_to_coe'', coe_le,
-    coe_eq_zero, coe_eq_coe, perm_singleton, subperm_singleton_iff']
+    coe_eq_zero, coe_eq_coe, perm_singleton, subperm_singleton_iff]
 
 @[simp] lemma lt_singleton : s < {a} ↔ s = 0 := by
   simp only [lt_iff_le_and_ne, le_singleton, or_and_right, Ne.def, and_not_self, or_false,

lake-manifest.json

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