bump to nightly-2023-10-31-06

mathlib commit leanprover-community/mathlib@65a1391

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"
 

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"
 

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
 -/
 

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
 -/

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"
 

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 :=

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

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 α) :

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 : α → β)

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

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