diff --git a/Mathlib/Data/List/Intervals.lean b/Mathlib/Data/List/Intervals.lean
index 76357910652d1..b50fd537307e5 100644
--- a/Mathlib/Data/List/Intervals.lean
+++ b/Mathlib/Data/List/Intervals.lean
@@ -112,7 +112,7 @@ theorem inter_consecutive (n m l : ℕ) : Ico n m ∩ Ico m l = [] := by
 
 @[simp]
 theorem bagInter_consecutive (n m l : Nat) :  @List.bagInter ℕ instBEq (Ico n m) (Ico m l) = [] :=
-  (bagInter_nil_iff_inter_nil _ _).2 (inter_consecutive n m l)
+  (bagInter_nil_iff_inter_nil _ _).2 (by convert inter_consecutive n m l)
 #align list.Ico.bag_inter_consecutive List.Ico.bagInter_consecutive
 
 @[simp]
diff --git a/Mathlib/Data/List/Lattice.lean b/Mathlib/Data/List/Lattice.lean
index 87d8e1523db59..f8ea3de5aa328 100644
--- a/Mathlib/Data/List/Lattice.lean
+++ b/Mathlib/Data/List/Lattice.lean
@@ -181,7 +181,7 @@ theorem forall_mem_inter_of_forall_right (l₁ : List α) (h : ∀ x ∈ l₂, p
 
 @[simp]
 theorem inter_reverse {xs ys : List α} : xs.inter ys.reverse = xs.inter ys := by
-  simp only [List.inter, mem_reverse]
+  simp only [List.inter, elem_eq_mem, mem_reverse]
 #align list.inter_reverse List.inter_reverse
 
 end Inter
diff --git a/Mathlib/Data/List/Nodup.lean b/Mathlib/Data/List/Nodup.lean
index 2f348ccbdd75f..6393edad30c62 100644
--- a/Mathlib/Data/List/Nodup.lean
+++ b/Mathlib/Data/List/Nodup.lean
@@ -469,7 +469,7 @@ theorem Nodup.pairwise_coe [IsSymm α r] (hl : l.Nodup) :
 
 -- Porting note (#10756): new theorem
 theorem Nodup.take_eq_filter_mem [DecidableEq α] :
-    ∀ {l : List α} {n : ℕ} (_ : l.Nodup), l.take n = l.filter (· ∈ l.take n)
+    ∀ {l : List α} {n : ℕ} (_ : l.Nodup), l.take n = l.filter (l.take n).elem
   | [], n, _ => by simp
   | b::l, 0, _ => by simp
   | b::l, n+1, hl => by
diff --git a/Mathlib/Data/List/Perm.lean b/Mathlib/Data/List/Perm.lean
index 2e81ee7f752f9..dd97dc89ff67e 100644
--- a/Mathlib/Data/List/Perm.lean
+++ b/Mathlib/Data/List/Perm.lean
@@ -607,7 +607,7 @@ theorem Perm.erasep (f : α → Prop) [DecidablePred f] {l₁ l₂ : List α}
 theorem Perm.take_inter {α : Type*} [DecidableEq α] {xs ys : List α} (n : ℕ) (h : xs ~ ys)
     (h' : ys.Nodup) : xs.take n ~ ys.inter (xs.take n) := by
   simp only [List.inter]
-  exact Perm.trans (show xs.take n ~ xs.filter (· ∈ xs.take n) by
+  exact Perm.trans (show xs.take n ~ xs.filter (xs.take n).elem by
       conv_lhs => rw [Nodup.take_eq_filter_mem ((Perm.nodup_iff h).2 h')])
     (Perm.filter _ h)
 #align list.perm.take_inter List.Perm.take_inter
diff --git a/Mathlib/Data/Multiset/FinsetOps.lean b/Mathlib/Data/Multiset/FinsetOps.lean
index 6eb77e71fc3c2..157ecfe22fd11 100644
--- a/Mathlib/Data/Multiset/FinsetOps.lean
+++ b/Mathlib/Data/Multiset/FinsetOps.lean
@@ -217,8 +217,10 @@ def ndinter (s t : Multiset α) : Multiset α :=
 #align multiset.ndinter Multiset.ndinter
 
 @[simp]
-theorem coe_ndinter (l₁ l₂ : List α) : @ndinter α _ l₁ l₂ = (l₁ ∩ l₂ : List α) :=
-  rfl
+theorem coe_ndinter (l₁ l₂ : List α) : @ndinter α _ l₁ l₂ = (l₁ ∩ l₂ : List α) := by
+  simp only [ndinter, mem_coe, filter_coe, coe_eq_coe, ← elem_eq_mem]
+  apply Perm.refl
+
 #align multiset.coe_ndinter Multiset.coe_ndinter
 
 @[simp, nolint simpNF] -- Porting note (#10675): dsimp can not prove this
diff --git a/lake-manifest.json b/lake-manifest.json
index aa0032dc1ae30..3311107301adf 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "67c40f89be2c17c6f4b0b6056d2de8591c0f92d3",
+   "rev": "d4161291e2a4c1c92d710bf670570aa79bf0d6ef",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",