From 1235ec289a65216b5edd90e72c68f6cfb15f498e Mon Sep 17 00:00:00 2001
From: leanprover-community-bot <leanprover.community@gmail.com>
Date: Tue, 31 Oct 2023 06:42:02 +0000
Subject: [PATCH] bump to nightly-2023-10-31-06

mathlib commit https://github.com/leanprover-community/mathlib/commit/65a1391a0106c9204fe45bc73a039f056558cb83
---
 Archive/All.lean                             |  2 +-
 Counterexamples/All.lean                     |  2 +-
 Mathbin/Algebra/BigOperators/Basic.lean      | 26 ++++++--
 Mathbin/Algebra/BigOperators/Order.lean      |  4 +-
 Mathbin/All.lean                             |  2 +-
 Mathbin/Data/Finset/Card.lean                |  7 ++-
 Mathbin/Data/Finset/Image.lean               | 22 ++++++-
 Mathbin/Data/List/Basic.lean                 | 37 ++++++++++-
 Mathbin/Data/List/Count.lean                 | 12 +++-
 Mathbin/Data/List/Perm.lean                  |  4 +-
 Mathbin/Data/Multiset/Basic.lean             | 64 +++++++++++++++-----
 Mathbin/Data/Multiset/Lattice.lean           |  3 +-
 Mathbin/Data/Set/Finite.lean                 |  4 +-
 Mathbin/NumberTheory/KummerDedekind.lean     |  4 +-
 Mathbin/Topology/MetricSpace/Metrizable.lean |  8 +--
 README.md                                    |  2 +-
 lake-manifest.json                           | 40 ++++++------
 lakefile.lean                                |  4 +-
 upstream-rev                                 |  2 +-
 19 files changed, 186 insertions(+), 63 deletions(-)

diff --git a/Archive/All.lean b/Archive/All.lean
index 0c34db5b64..3715824253 100644
--- a/Archive/All.lean
+++ b/Archive/All.lean
@@ -53,5 +53,5 @@ import Wiedijk100Theorems.PerfectNumbers
 import Wiedijk100Theorems.SolutionOfCubic
 import Wiedijk100Theorems.SumOfPrimeReciprocalsDiverges
 
-#align_import all from "leanprover-community/mathlib"@"3365b20c2ffa7c35e47e5209b89ba9abdddf3ffe"
+#align_import all from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"
 
diff --git a/Counterexamples/All.lean b/Counterexamples/All.lean
index 713aa75120..3650e14940 100644
--- a/Counterexamples/All.lean
+++ b/Counterexamples/All.lean
@@ -13,5 +13,5 @@ import SeminormLatticeNotDistrib
 import SorgenfreyLine
 import ZeroDivisorsInAddMonoidAlgebras
 
-#align_import all from "leanprover-community/mathlib"@"3365b20c2ffa7c35e47e5209b89ba9abdddf3ffe"
+#align_import all from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"
 
diff --git a/Mathbin/Algebra/BigOperators/Basic.lean b/Mathbin/Algebra/BigOperators/Basic.lean
index 651431f87c..eaeca35970 100644
--- a/Mathbin/Algebra/BigOperators/Basic.lean
+++ b/Mathbin/Algebra/BigOperators/Basic.lean
@@ -14,7 +14,7 @@ import Data.Finset.Sigma
 import Data.Multiset.Powerset
 import Data.Set.Pairwise.Basic
 
-#align_import algebra.big_operators.basic from "leanprover-community/mathlib"@"fa2309577c7009ea243cffdf990cd6c84f0ad497"
+#align_import algebra.big_operators.basic from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"
 
 /-!
 # Big operators
@@ -129,6 +129,12 @@ theorem prod_eq_multiset_prod [CommMonoid β] (s : Finset α) (f : α → β) :
 #align finset.sum_eq_multiset_sum Finset.sum_eq_multiset_sum
 -/
 
+@[simp, to_additive]
+theorem prod_map_val [CommMonoid β] (s : Finset α) (f : α → β) : (s.1.map f).Prod = ∏ a in s, f a :=
+  rfl
+#align finset.prod_map_val Finset.prod_map_val
+#align finset.sum_map_val Finset.sum_map_val
+
 #print Finset.prod_eq_fold /-
 @[to_additive]
 theorem prod_eq_fold [CommMonoid β] (s : Finset α) (f : α → β) :
@@ -1998,12 +2004,22 @@ theorem sum_const_nat {m : ℕ} {f : α → ℕ} (h₁ : ∀ x ∈ s, f x = m) :
 #align finset.sum_const_nat Finset.sum_const_nat
 -/
 
+theorem nat_cast_card_filter [AddCommMonoidWithOne β] (p) [DecidablePred p] (s : Finset α) :
+    ((filter p s).card : β) = ∑ a in s, if p a then 1 else 0 := by
+  simp only [add_zero, sum_const, nsmul_eq_mul, eq_self_iff_true, sum_const_zero, sum_ite,
+    nsmul_one]
+#align finset.nat_cast_card_filter Finset.nat_cast_card_filter
+
+theorem card_filter (p) [DecidablePred p] (s : Finset α) :
+    (filter p s).card = ∑ a in s, ite (p a) 1 0 :=
+  nat_cast_card_filter _ _
+#align finset.card_filter Finset.card_filter
+
 #print Finset.sum_boole /-
 @[simp]
-theorem sum_boole {s : Finset α} {p : α → Prop} [NonAssocSemiring β] {hp : DecidablePred p} :
-    (∑ x in s, if p x then (1 : β) else (0 : β)) = (s.filterₓ p).card := by
-  simp only [add_zero, mul_one, Finset.sum_const, nsmul_eq_mul, eq_self_iff_true,
-    Finset.sum_const_zero, Finset.sum_ite]
+theorem sum_boole {s : Finset α} {p : α → Prop} [AddCommMonoidWithOne β] {hp : DecidablePred p} :
+    (∑ x in s, if p x then 1 else 0 : β) = (s.filterₓ p).card :=
+  (nat_cast_card_filter _ _).symm
 #align finset.sum_boole Finset.sum_boole
 -/
 
diff --git a/Mathbin/Algebra/BigOperators/Order.lean b/Mathbin/Algebra/BigOperators/Order.lean
index a9054e7420..9d1d1f64c2 100644
--- a/Mathbin/Algebra/BigOperators/Order.lean
+++ b/Mathbin/Algebra/BigOperators/Order.lean
@@ -8,7 +8,7 @@ import Algebra.Order.Ring.WithTop
 import Algebra.BigOperators.Basic
 import Data.Fintype.Card
 
-#align_import algebra.big_operators.order from "leanprover-community/mathlib"@"824f9ae93a4f5174d2ea948e2d75843dd83447bb"
+#align_import algebra.big_operators.order from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"
 
 /-!
 # Results about big operators with values in an ordered algebraic structure.
@@ -230,7 +230,7 @@ theorem prod_le_pow_card (s : Finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s
   by
   refine' (Multiset.prod_le_pow_card (s.val.map f) n _).trans _
   · simpa using h
-  · simpa
+  · simp
 #align finset.prod_le_pow_card Finset.prod_le_pow_card
 #align finset.sum_le_card_nsmul Finset.sum_le_card_nsmul
 -/
diff --git a/Mathbin/All.lean b/Mathbin/All.lean
index c5e332a543..a2d1be0f60 100644
--- a/Mathbin/All.lean
+++ b/Mathbin/All.lean
@@ -3219,5 +3219,5 @@ import Topology.VectorBundle.Basic
 import Topology.VectorBundle.Constructions
 import Topology.VectorBundle.Hom
 
-#align_import all from "leanprover-community/mathlib"@"3365b20c2ffa7c35e47e5209b89ba9abdddf3ffe"
+#align_import all from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"
 
diff --git a/Mathbin/Data/Finset/Card.lean b/Mathbin/Data/Finset/Card.lean
index 51a8b550c2..17a5bf9eaa 100644
--- a/Mathbin/Data/Finset/Card.lean
+++ b/Mathbin/Data/Finset/Card.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad
 import Data.Finset.Image
 import Tactic.ByContra
 
-#align_import data.finset.card from "leanprover-community/mathlib"@"3365b20c2ffa7c35e47e5209b89ba9abdddf3ffe"
+#align_import data.finset.card from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"
 
 /-!
 # Cardinality of a finite set
@@ -55,6 +55,11 @@ theorem card_def (s : Finset α) : s.card = s.1.card :=
 #align finset.card_def Finset.card_def
 -/
 
+@[simp]
+theorem card_val (s : Finset α) : s.1.card = s.card :=
+  rfl
+#align finset.card_val Finset.card_val
+
 #print Finset.card_mk /-
 @[simp]
 theorem card_mk {m nodup} : (⟨m, nodup⟩ : Finset α).card = m.card :=
diff --git a/Mathbin/Data/Finset/Image.lean b/Mathbin/Data/Finset/Image.lean
index 1c431cb7fc..f85d0ad62b 100644
--- a/Mathbin/Data/Finset/Image.lean
+++ b/Mathbin/Data/Finset/Image.lean
@@ -8,7 +8,7 @@ import Data.Fin.Basic
 import Data.Finset.Basic
 import Data.Int.Order.Basic
 
-#align_import data.finset.image from "leanprover-community/mathlib"@"b685f506164f8d17a6404048bc4d696739c5d976"
+#align_import data.finset.image from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"
 
 /-! # Image and map operations on finite sets
 
@@ -225,6 +225,26 @@ theorem filter_map {p : β → Prop} [DecidablePred p] :
 #align finset.filter_map Finset.filter_map
 -/
 
+theorem map_filter' (p : α → Prop) [DecidablePred p] (f : α ↪ β) (s : Finset α)
+    [DecidablePred fun b => ∃ a, p a ∧ f a = b] :
+    (s.filterₓ p).map f = (s.map f).filterₓ fun b => ∃ a, p a ∧ f a = b := by
+  simp [(· ∘ ·), filter_map, f.injective.eq_iff]
+#align finset.map_filter' Finset.map_filter'
+
+theorem filter_attach' [DecidableEq α] (s : Finset α) (p : s → Prop) [DecidablePred p] :
+    s.attach.filterₓ p =
+      (s.filterₓ fun x => ∃ h, p ⟨x, h⟩).attach.map
+        ⟨Subtype.map id <| filter_subset _ _, Subtype.map_injective _ injective_id⟩ :=
+  eq_of_veq <| Multiset.filter_attach' _ _
+#align finset.filter_attach' Finset.filter_attach'
+
+@[simp]
+theorem filter_attach (p : α → Prop) [DecidablePred p] (s : Finset α) :
+    (s.attach.filterₓ fun x => p ↑x) =
+      (s.filterₓ p).attach.map ((Embedding.refl _).subtypeMap mem_of_mem_filter) :=
+  eq_of_veq <| Multiset.filter_attach _ _
+#align finset.filter_attach Finset.filter_attach
+
 #print Finset.map_filter /-
 theorem map_filter {f : α ≃ β} {p : α → Prop} [DecidablePred p] :
     (s.filterₓ p).map f.toEmbedding = (s.map f.toEmbedding).filterₓ (p ∘ f.symm) := by
diff --git a/Mathbin/Data/List/Basic.lean b/Mathbin/Data/List/Basic.lean
index 9c1b988b62..6128ee73ae 100644
--- a/Mathbin/Data/List/Basic.lean
+++ b/Mathbin/Data/List/Basic.lean
@@ -5,7 +5,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 -/
 import Data.Nat.Order.Basic
 
-#align_import data.list.basic from "leanprover-community/mathlib"@"9da1b3534b65d9661eb8f42443598a92bbb49211"
+#align_import data.list.basic from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"
 
 /-!
 # Basic properties of lists
@@ -4287,6 +4287,11 @@ def attach (l : List α) : List { x // x ∈ l } :=
 #align list.attach List.attach
 -/
 
+@[simp]
+theorem attach_nil : ([] : List α).attach = [] :=
+  rfl
+#align list.attach_nil List.attach_nil
+
 #print List.sizeOf_lt_sizeOf_of_mem /-
 theorem sizeOf_lt_sizeOf_of_mem [SizeOf α] {x : α} {l : List α} (hx : x ∈ l) :
     SizeOf.sizeOf x < SizeOf.sizeOf l :=
@@ -5082,6 +5087,32 @@ theorem map_filter (f : β → α) (l : List β) : filter p (map f l) = map f (f
 #align list.map_filter List.map_filter
 -/
 
+theorem map_filter' {f : α → β} (hf : Injective f) (l : List α)
+    [DecidablePred fun b => ∃ a, p a ∧ f a = b] :
+    (l.filterₓ p).map f = (l.map f).filterₓ fun b => ∃ a, p a ∧ f a = b := by
+  simp [(· ∘ ·), map_filter, hf.eq_iff]
+#align list.map_filter' List.map_filter'
+
+theorem filter_attach' (l : List α) (p : { a // a ∈ l } → Prop) [DecidableEq α] [DecidablePred p] :
+    l.attach.filterₓ p =
+      (l.filterₓ fun x => ∃ h, p ⟨x, h⟩).attach.map
+        (Subtype.map id fun x hx =>
+          let ⟨h, _⟩ := of_mem_filter hx
+          h) :=
+  by
+  classical
+  refine' map_injective_iff.2 Subtype.coe_injective _
+  simp [(· ∘ ·), map_filter' _ Subtype.coe_injective]
+#align list.filter_attach' List.filterₓ_attach'
+
+@[simp]
+theorem filter_attach (l : List α) (p : α → Prop) [DecidablePred p] :
+    (l.attach.filterₓ fun x => p ↑x) =
+      (l.filterₓ p).attach.map (Subtype.map id fun _ => mem_of_mem_filter) :=
+  map_injective_iff.2 Subtype.coe_injective <| by
+    simp_rw [map_map, (· ∘ ·), Subtype.map, Subtype.coe_mk, id.def, ← map_filter, attach_map_coe]
+#align list.filter_attach List.filterₓ_attach
+
 #print List.filter_filter /-
 @[simp]
 theorem filter_filter (q) [DecidablePred q] :
@@ -5094,6 +5125,10 @@ theorem filter_filter (q) [DecidablePred q] :
 #align list.filter_filter List.filter_filter
 -/
 
+theorem filter_comm (q) [DecidablePred q] (l : List α) :
+    filter p (filter q l) = filter q (filter p l) := by simp [and_comm']
+#align list.filter_comm List.filterₓ_comm
+
 #print List.filter_true /-
 @[simp]
 theorem filter_true {h : DecidablePred fun a : α => True} (l : List α) :
diff --git a/Mathbin/Data/List/Count.lean b/Mathbin/Data/List/Count.lean
index 2bf1445eaf..7ef1a88a34 100644
--- a/Mathbin/Data/List/Count.lean
+++ b/Mathbin/Data/List/Count.lean
@@ -5,7 +5,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 -/
 import Data.List.BigOperators.Basic
 
-#align_import data.list.count from "leanprover-community/mathlib"@"47adfab39a11a072db552f47594bf8ed2cf8a722"
+#align_import data.list.count from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"
 
 /-!
 # Counting in lists
@@ -156,6 +156,11 @@ theorem countP_map (p : β → Prop) [DecidablePred p] (f : α → β) :
 #align list.countp_map List.countP_map
 -/
 
+@[simp]
+theorem countP_attach (l : List α) : (l.attach.countP fun a => p ↑a) = l.countP p := by
+  rw [← countp_map, attach_map_coe]
+#align list.countp_attach List.countP_attach
+
 variable {p q}
 
 #print List.countP_mono_left /-
@@ -377,6 +382,11 @@ theorem count_bind {α β} [DecidableEq β] (l : List α) (f : α → List β) (
 #align list.count_bind List.count_bind
 -/
 
+@[simp]
+theorem count_attach (a : { x // x ∈ l }) : l.attach.count a = l.count a :=
+  Eq.trans (countP_congr fun _ _ => Subtype.ext_iff) <| countP_attach _ _
+#align list.count_attach List.count_attach
+
 #print List.count_map_of_injective /-
 @[simp]
 theorem count_map_of_injective {α β} [DecidableEq α] [DecidableEq β] (l : List α) (f : α → β)
diff --git a/Mathbin/Data/List/Perm.lean b/Mathbin/Data/List/Perm.lean
index 41f5c589a2..40c6c8d724 100644
--- a/Mathbin/Data/List/Perm.lean
+++ b/Mathbin/Data/List/Perm.lean
@@ -8,7 +8,7 @@ import Data.List.Permutation
 import Data.List.Range
 import Data.Nat.Factorial.Basic
 
-#align_import data.list.perm from "leanprover-community/mathlib"@"f2f413b9d4be3a02840d0663dace76e8fe3da053"
+#align_import data.list.perm from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"
 
 /-!
 # List Permutations
@@ -579,7 +579,7 @@ theorem Subperm.countP_le (p : α → Prop) [DecidablePred p] {l₁ l₂ : List
 
 #print List.Perm.countP_congr /-
 theorem Perm.countP_congr (s : l₁ ~ l₂) {p p' : α → Prop} [DecidablePred p] [DecidablePred p']
-    (hp : ∀ x ∈ l₁, p x = p' x) : l₁.countP p = l₂.countP p' :=
+    (hp : ∀ x ∈ l₁, p x ↔ p' x) : l₁.countP p = l₂.countP p' :=
   by
   rw [← s.countp_eq p']
   clear s
diff --git a/Mathbin/Data/Multiset/Basic.lean b/Mathbin/Data/Multiset/Basic.lean
index b629d693ce..4ed0ff173e 100644
--- a/Mathbin/Data/Multiset/Basic.lean
+++ b/Mathbin/Data/Multiset/Basic.lean
@@ -6,7 +6,7 @@ Authors: Mario Carneiro
 import Data.Set.List
 import Data.List.Perm
 
-#align_import data.multiset.basic from "leanprover-community/mathlib"@"06a655b5fcfbda03502f9158bbf6c0f1400886f9"
+#align_import data.multiset.basic from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"
 
 /-!
 # Multisets
@@ -19,7 +19,7 @@ We define the global infix notation `::ₘ` for `multiset.cons`.
 -/
 
 
-open List Subtype Nat
+open Function List Nat Subtype
 
 variable {α : Type _} {β : Type _} {γ : Type _}
 
@@ -2739,6 +2739,10 @@ theorem filter_filter (q) [DecidablePred q] (s : Multiset α) :
 #align multiset.filter_filter Multiset.filter_filter
 -/
 
+theorem filter_comm (q) [DecidablePred q] (s : Multiset α) :
+    filter p (filter q s) = filter q (filter p s) := by simp [and_comm']
+#align multiset.filter_comm Multiset.filter_comm
+
 #print Multiset.filter_add_filter /-
 theorem filter_add_filter (q) [DecidablePred q] (s : Multiset α) :
     filter p s + filter q s = filter (fun a => p a ∨ q a) s + filter (fun a => p a ∧ q a) s :=
@@ -2758,6 +2762,12 @@ theorem map_filter (f : β → α) (s : Multiset β) : filter p (map f s) = map
 #align multiset.map_filter Multiset.map_filter
 -/
 
+theorem map_filter' {f : α → β} (hf : Injective f) (s : Multiset α)
+    [DecidablePred fun b => ∃ a, p a ∧ f a = b] :
+    (s.filterₓ p).map f = (s.map f).filterₓ fun b => ∃ a, p a ∧ f a = b := by
+  simp [(· ∘ ·), map_filter, hf.eq_iff]
+#align multiset.map_filter' Multiset.map_filter'
+
 /-! ### Simultaneously filter and map elements of a multiset -/
 
 
@@ -3032,6 +3042,22 @@ theorem countP_map (f : α → β) (s : Multiset α) (p : β → Prop) [Decidabl
 #align multiset.countp_map Multiset.countP_map
 -/
 
+@[simp]
+theorem countP_attach (s : Multiset α) : (s.attach.countP fun a => p ↑a) = s.countP p :=
+  Quotient.inductionOn s fun l =>
+    by
+    simp only [quot_mk_to_coe, coe_countp]
+    rw [quot_mk_to_coe, coe_attach, coe_countp]
+    exact List.countP_attach _ _
+#align multiset.countp_attach Multiset.countP_attach
+
+@[simp]
+theorem filter_attach (m : Multiset α) (p : α → Prop) [DecidablePred p] :
+    (m.attach.filterₓ fun x => p ↑x) =
+      (m.filterₓ p).attach.map (Subtype.map id fun _ => Multiset.mem_of_mem_filter) :=
+  Quotient.inductionOn m fun l => congr_arg coe (List.filter_attach l p)
+#align multiset.filter_attach Multiset.filter_attach
+
 variable {p}
 
 #print Multiset.countP_pos /-
@@ -3060,7 +3086,7 @@ theorem countP_pos_of_mem {s a} (h : a ∈ s) (pa : p a) : 0 < countP p s :=
 
 #print Multiset.countP_congr /-
 theorem countP_congr {s s' : Multiset α} (hs : s = s') {p p' : α → Prop} [DecidablePred p]
-    [DecidablePred p'] (hp : ∀ x ∈ s, p x = p' x) : s.countP p = s'.countP p' :=
+    [DecidablePred p'] (hp : ∀ x ∈ s, p x ↔ p' x) : s.countP p = s'.countP p' :=
   Quot.induction_on₂ s s'
     (fun l l' hs hp => by
       simp only [quot_mk_to_coe'', coe_eq_coe] at hs 
@@ -3076,7 +3102,7 @@ end
 
 section
 
-variable [DecidableEq α]
+variable [DecidableEq α] {s : Multiset α}
 
 #print Multiset.count /-
 /-- `count a s` is the multiplicity of `a` in `s`. -/
@@ -3178,6 +3204,11 @@ theorem count_nsmul (a : α) (n s) : count a (n • s) = n * count a s := by
 #align multiset.count_nsmul Multiset.count_nsmul
 -/
 
+@[simp]
+theorem count_attach (a : { x // x ∈ s }) : s.attach.count a = s.count a :=
+  Eq.trans (countP_congr rfl fun _ _ => Subtype.ext_iff) <| countP_attach _ _
+#align multiset.count_attach Multiset.count_attach
+
 #print Multiset.count_pos /-
 theorem count_pos {a : α} {s : Multiset α} : 0 < count a s ↔ a ∈ s := by simp [count, countp_pos]
 #align multiset.count_pos Multiset.count_pos
@@ -3378,16 +3409,6 @@ theorem count_map_eq_count' [DecidableEq β] (f : α → β) (s : Multiset α) (
 #align multiset.count_map_eq_count' Multiset.count_map_eq_count'
 -/
 
-#print Multiset.attach_count_eq_count_coe /-
-@[simp]
-theorem attach_count_eq_count_coe (m : Multiset α) (a) : m.attach.count a = m.count (a : α) :=
-  calc
-    m.attach.count a = (m.attach.map (coe : _ → α)).count (a : α) :=
-      (Multiset.count_map_eq_count' _ _ Subtype.coe_injective _).symm
-    _ = m.count (a : α) := congr_arg _ m.attach_map_val
-#align multiset.attach_count_eq_count_coe Multiset.attach_count_eq_count_coe
--/
-
 #print Multiset.filter_eq' /-
 theorem filter_eq' (s : Multiset α) (b : α) : s.filterₓ (· = b) = replicate (count b s) b :=
   Quotient.inductionOn s fun l => congr_arg coe <| filter_eq' l b
@@ -3745,6 +3766,21 @@ theorem map_injective {f : α → β} (hf : Function.Injective f) :
 #align multiset.map_injective Multiset.map_injective
 -/
 
+theorem filter_attach' (s : Multiset α) (p : { a // a ∈ s } → Prop) [DecidableEq α]
+    [DecidablePred p] :
+    s.attach.filterₓ p =
+      (s.filterₓ fun x => ∃ h, p ⟨x, h⟩).attach.map
+        (Subtype.map id fun x hx =>
+          let ⟨h, _⟩ := of_mem_filter hx
+          h) :=
+  by
+  classical
+  refine' Multiset.map_injective Subtype.coe_injective _
+  simp only [Function.comp, map_filter' _ Subtype.coe_injective, Subtype.exists, coe_mk,
+    exists_and_right, exists_eq_right, attach_map_coe, map_map, map_coe, id.def]
+  rw [attach_map_coe]
+#align multiset.filter_attach' Multiset.filter_attach'
+
 end Map
 
 section Quot
diff --git a/Mathbin/Data/Multiset/Lattice.lean b/Mathbin/Data/Multiset/Lattice.lean
index 6cba1d1404..67162f81f8 100644
--- a/Mathbin/Data/Multiset/Lattice.lean
+++ b/Mathbin/Data/Multiset/Lattice.lean
@@ -6,7 +6,7 @@ Authors: Mario Carneiro
 import Data.Multiset.FinsetOps
 import Data.Multiset.Fold
 
-#align_import data.multiset.lattice from "leanprover-community/mathlib"@"f2f413b9d4be3a02840d0663dace76e8fe3da053"
+#align_import data.multiset.lattice from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"
 
 /-!
 # Lattice operations on multisets
@@ -71,6 +71,7 @@ theorem sup_add (s₁ s₂ : Multiset α) : (s₁ + s₂).sup = s₁.sup ⊔ s
 -/
 
 #print Multiset.sup_le /-
+@[simp]
 theorem sup_le {s : Multiset α} {a : α} : s.sup ≤ a ↔ ∀ b ∈ s, b ≤ a :=
   Multiset.induction_on s (by simp)
     (by simp (config := { contextual := true }) [or_imp, forall_and])
diff --git a/Mathbin/Data/Set/Finite.lean b/Mathbin/Data/Set/Finite.lean
index 93fb38e99a..dcaf9aab66 100644
--- a/Mathbin/Data/Set/Finite.lean
+++ b/Mathbin/Data/Set/Finite.lean
@@ -7,7 +7,7 @@ import Data.Finset.Basic
 import Data.Set.Functor
 import Data.Finite.Basic
 
-#align_import data.set.finite from "leanprover-community/mathlib"@"ffde2d8a6e689149e44fd95fa862c23a57f8c780"
+#align_import data.set.finite from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"
 
 /-!
 # Finite sets
@@ -1530,7 +1530,7 @@ theorem empty_card' {h : Fintype.{u} (∅ : Set α)} : @Fintype.card (∅ : Set
 #print Set.card_fintypeInsertOfNotMem /-
 theorem card_fintypeInsertOfNotMem {a : α} (s : Set α) [Fintype s] (h : a ∉ s) :
     @Fintype.card _ (fintypeInsertOfNotMem s h) = Fintype.card s + 1 := by
-  rw [fintype_insert_of_not_mem, Fintype.card_ofFinset] <;> simp [Finset.card, to_finset] <;> rfl
+  simp [fintype_insert_of_not_mem, Fintype.card_ofFinset]
 #align set.card_fintype_insert_of_not_mem Set.card_fintypeInsertOfNotMem
 -/
 
diff --git a/Mathbin/NumberTheory/KummerDedekind.lean b/Mathbin/NumberTheory/KummerDedekind.lean
index 8b2597f697..86fc32083a 100644
--- a/Mathbin/NumberTheory/KummerDedekind.lean
+++ b/Mathbin/NumberTheory/KummerDedekind.lean
@@ -6,7 +6,7 @@ Authors: Anne Baanen, Paul Lezeau
 import RingTheory.DedekindDomain.Ideal
 import RingTheory.IsAdjoinRoot
 
-#align_import number_theory.kummer_dedekind from "leanprover-community/mathlib"@"f2ad3645af9effcdb587637dc28a6074edc813f9"
+#align_import number_theory.kummer_dedekind from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"
 
 /-!
 # Kummer-Dedekind theorem
@@ -349,7 +349,7 @@ theorem normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map (hI : I
   rw [Multiset.count_map_eq_count' fun f =>
       ((normalized_factors_map_equiv_normalized_factors_min_poly_mk hI hI' hx hx').symm f :
         Ideal S),
-    Multiset.attach_count_eq_count_coe]
+    Multiset.count_attach]
   · exact subtype.coe_injective.comp (Equiv.injective _)
   · exact (normalized_factors_map_equiv_normalized_factors_min_poly_mk hI hI' hx hx' _).Prop
   ·
diff --git a/Mathbin/Topology/MetricSpace/Metrizable.lean b/Mathbin/Topology/MetricSpace/Metrizable.lean
index 181177ccd6..2922d52357 100644
--- a/Mathbin/Topology/MetricSpace/Metrizable.lean
+++ b/Mathbin/Topology/MetricSpace/Metrizable.lean
@@ -179,10 +179,10 @@ instance metrizableSpace_pi [∀ i, MetrizableSpace (π i)] : MetrizableSpace (
 variable (X) [T3Space X] [SecondCountableTopology X]
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
-#print TopologicalSpace.exists_embedding_l_infty /-
+#print TopologicalSpace.exists_inducing_l_infty /-
 /-- A T₃ topological space with second countable topology can be embedded into `l^∞ = ℕ →ᵇ ℝ`.
 -/
-theorem exists_embedding_l_infty : ∃ f : X → ℕ →ᵇ ℝ, Embedding f :=
+theorem exists_inducing_l_infty : ∃ f : X → ℕ →ᵇ ℝ, Embedding f :=
   by
   haveI : NormalSpace X := NormalSpace.of_regularSpace_secondCountableTopology X
   -- Choose a countable basis, and consider the set `s` of pairs of set `(U, V)` such that `U ∈ B`,
@@ -275,7 +275,7 @@ theorem exists_embedding_l_infty : ∃ f : X → ℕ →ᵇ ℝ, Embedding f :=
     refine' this.mono fun y hy => (BoundedContinuousFunction.dist_le δ0.le).2 fun UV => _
     cases' le_total δ (ε UV) with hle hle
     exacts [hy _ hle, (Real.dist_le_of_mem_Icc (hf0ε _ _) (hf0ε _ _)).trans (by rwa [sub_zero])]
-#align topological_space.exists_embedding_l_infty TopologicalSpace.exists_embedding_l_infty
+#align topological_space.exists_embedding_l_infty TopologicalSpace.exists_inducing_l_infty
 -/
 
 #print TopologicalSpace.metrizableSpace_of_t3_second_countable /-
@@ -283,7 +283,7 @@ theorem exists_embedding_l_infty : ∃ f : X → ℕ →ᵇ ℝ, Embedding f :=
 countable topology `X` is metrizable, i.e., there exists a metric space structure that generates the
 same topology. -/
 theorem metrizableSpace_of_t3_second_countable : MetrizableSpace X :=
-  let ⟨f, hf⟩ := exists_embedding_l_infty X
+  let ⟨f, hf⟩ := exists_inducing_l_infty X
   hf.MetrizableSpace
 #align topological_space.metrizable_space_of_t3_second_countable TopologicalSpace.metrizableSpace_of_t3_second_countable
 -/
diff --git a/README.md b/README.md
index 9e2ad8df84..821782e936 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,4 @@
-Tracking mathlib commit: [`3365b20c2ffa7c35e47e5209b89ba9abdddf3ffe`](https://github.com/leanprover-community/mathlib/commit/3365b20c2ffa7c35e47e5209b89ba9abdddf3ffe)
+Tracking mathlib commit: [`65a1391a0106c9204fe45bc73a039f056558cb83`](https://github.com/leanprover-community/mathlib/commit/65a1391a0106c9204fe45bc73a039f056558cb83)
 
 You should use this repository to inspect the Lean 4 files that `mathport` has generated from mathlib3.
 Please run `lake build` first, to download a copy of the generated `.olean` files.
diff --git a/lake-manifest.json b/lake-manifest.json
index 4b1795dcbd..4783c00ec2 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,26 +4,18 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "e30b0f6d7c048a1ca5b652d0497d9aa5ab59572d",
+    "rev": "a057bbbfed5a00b825b9d93a02a9f59e7d815d4a",
     "opts": {},
     "name": "lean3port",
-    "inputRev?": "e30b0f6d7c048a1ca5b652d0497d9aa5ab59572d",
+    "inputRev?": "a057bbbfed5a00b825b9d93a02a9f59e7d815d4a",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "a988ad9300897ae7de89811e768a0b09555e6488",
+    "rev": "41b0e9c7f0d1ab669a24a957b1bd07886fd13749",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "a988ad9300897ae7de89811e768a0b09555e6488",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "bd60d932e2c786c7347e57576598568b2816e316",
-    "opts": {},
-    "name": "std",
-    "inputRev?": "main",
+    "inputRev?": "41b0e9c7f0d1ab669a24a957b1bd07886fd13749",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover-community/quote4",
@@ -33,14 +25,6 @@
     "name": "Qq",
     "inputRev?": "master",
     "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/aesop",
-    "subDir?": null,
-    "rev": "5e016236e9e699691aaa9872fa380df12cd7f677",
-    "opts": {},
-    "name": "aesop",
-    "inputRev?": "master",
-    "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover/lean4-cli",
     "subDir?": null,
@@ -56,5 +40,21 @@
     "opts": {},
     "name": "proofwidgets",
     "inputRev?": "v0.0.21",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover/std4",
+    "subDir?": null,
+    "rev": "6747f41f28627bed83e6d5891683538211caa2c1",
+    "opts": {},
+    "name": "std",
+    "inputRev?": "main",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/aesop",
+    "subDir?": null,
+    "rev": "6749fa4e776919514dae85bfc0ad62a511bc42a7",
+    "opts": {},
+    "name": "aesop",
+    "inputRev?": "master",
     "inherited": true}}],
  "name": "mathlib3port"}
diff --git a/lakefile.lean b/lakefile.lean
index 7f375e273f..051efb93eb 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-10-30-06"
+def tag : String := "nightly-2023-10-31-06"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"e30b0f6d7c048a1ca5b652d0497d9aa5ab59572d"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"a057bbbfed5a00b825b9d93a02a9f59e7d815d4a"
 
 @[default_target]
 lean_lib Mathbin where
diff --git a/upstream-rev b/upstream-rev
index d121db0d16..a593c86b5e 100644
--- a/upstream-rev
+++ b/upstream-rev
@@ -1 +1 @@
-3365b20c2ffa7c35e47e5209b89ba9abdddf3ffe
+65a1391a0106c9204fe45bc73a039f056558cb83