chore: bump Std (#6721)

This incorporates changes from #6575

I have also renamed `Multiset.countp` to `Multiset.countP` for consistency.

Co-authored-by: James Gallichio <jamesgallicchio@gmail.com>




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

Author: kim-em

Archive/MiuLanguage/DecisionNec.lean

@@ -75,9 +75,10 @@ theorem count_equiv_one_or_two_mod3_of_derivable (en : Miustr) :
   any_goals apply mod3_eq_1_or_mod3_eq_2 h_ih
   -- Porting note: `simp_rw [count_append]` usually doesn't work
   · left; rw [count_append, count_append]; rfl
-  · right; simp_rw [count_append, count_cons, if_false, two_mul]
+  · right; simp_rw [count_append, count_cons, if_false, two_mul]; simp
   · left; rw [count_append, count_append, count_append]
     simp_rw [count_cons_self, count_nil, count_cons, ite_false, add_right_comm, add_mod_right]
+    simp
   · left; rw [count_append, count_append, count_append]
     simp only [ne_eq, count_cons_of_ne, count_nil, add_zero]
 #align miu.count_equiv_one_or_two_mod3_of_derivable Miu.count_equiv_one_or_two_mod3_of_derivable

Archive/MiuLanguage/DecisionSuf.lean

@@ -262,12 +262,12 @@ theorem count_I_eq_length_of_count_U_zero_and_neg_mem {ys : Miustr} (hu : count
     · -- case `x = M` gives a contradiction.
       exfalso; exact hm (mem_cons_self M xs)
     · -- case `x = I`
-      rw [count_cons, if_pos rfl, length, succ_eq_add_one, succ_inj']
+      rw [count_cons, if_pos rfl, length, succ_inj']
       apply hxs
       · simpa only [count]
       · rw [mem_cons, not_or] at hm; exact hm.2
     · -- case `x = U` gives a contradiction.
-      exfalso; simp only [count, countp_cons_of_pos] at hu
+      exfalso; simp only [count, countP_cons_of_pos] at hu
       exact succ_ne_zero _ hu
 set_option linter.uppercaseLean3 false in
 #align miu.count_I_eq_length_of_count_U_zero_and_neg_mem Miu.count_I_eq_length_of_count_U_zero_and_neg_mem
@@ -277,7 +277,7 @@ set_option linter.uppercaseLean3 false in
 theorem base_case_suf (en : Miustr) (h : Decstr en) (hu : count U en = 0) : Derivable en := by
   rcases h with ⟨⟨mhead, nmtail⟩, hi⟩
   have : en ≠ nil := by
-    intro k; simp only [k, count, countp, if_false, zero_mod, zero_ne_one, false_or_iff] at hi
+    intro k; simp only [k, count, countP, if_false, zero_mod, zero_ne_one, false_or_iff] at hi
   rcases exists_cons_of_ne_nil this with ⟨y, ys, rfl⟩
   rcases mhead
   rsuffices ⟨c, rfl, hc⟩ : ∃ c, replicate c I = ys ∧ (c % 3 = 1 ∨ c % 3 = 2)

Mathlib.lean

@@ -1529,7 +1529,6 @@ import Mathlib.Data.List.ToFinsupp
 import Mathlib.Data.List.Zip
 import Mathlib.Data.MLList.BestFirst
 import Mathlib.Data.MLList.DepthFirst
-import Mathlib.Data.MLList.Heartbeats
 import Mathlib.Data.MLList.IO
 import Mathlib.Data.MLList.Split
 import Mathlib.Data.Matrix.Auto
@@ -2110,7 +2109,6 @@ import Mathlib.Init.Propext
 import Mathlib.Init.Quot
 import Mathlib.Init.Set
 import Mathlib.Init.ZeroOne
-import Mathlib.Lean.CoreM
 import Mathlib.Lean.Data.NameMap
 import Mathlib.Lean.Elab.Tactic.Basic
 import Mathlib.Lean.EnvExtension

Mathlib/Algebra/BigOperators/Associated.lean

@@ -63,22 +63,22 @@ theorem exists_associated_mem_of_dvd_prod [CancelCommMonoidWithZero α] {p : α}
 
 theorem Multiset.prod_primes_dvd [CancelCommMonoidWithZero α]
     [∀ a : α, DecidablePred (Associated a)] {s : Multiset α} (n : α) (h : ∀ a ∈ s, Prime a)
-    (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ a, s.countp (Associated a) ≤ 1) : s.prod ∣ n := by
+    (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ a, s.countP (Associated a) ≤ 1) : s.prod ∣ n := by
   induction' s using Multiset.induction_on with a s induct n primes divs generalizing n
   · simp only [Multiset.prod_zero, one_dvd]
   · rw [Multiset.prod_cons]
     obtain ⟨k, rfl⟩ : a ∣ n := div a (Multiset.mem_cons_self a s)
     apply mul_dvd_mul_left a
     refine induct _ (fun a ha => h a (Multiset.mem_cons_of_mem ha)) (fun b b_in_s => ?_)
-      fun a => (Multiset.countp_le_of_le _ (Multiset.le_cons_self _ _)).trans (uniq a)
+      fun a => (Multiset.countP_le_of_le _ (Multiset.le_cons_self _ _)).trans (uniq a)
     · have b_div_n := div b (Multiset.mem_cons_of_mem b_in_s)
       have a_prime := h a (Multiset.mem_cons_self a s)
       have b_prime := h b (Multiset.mem_cons_of_mem b_in_s)
       refine' (b_prime.dvd_or_dvd b_div_n).resolve_left fun b_div_a => _
       have assoc := b_prime.associated_of_dvd a_prime b_div_a
       have := uniq a
-      rw [Multiset.countp_cons_of_pos _ (Associated.refl _), Nat.succ_le_succ_iff, ← not_lt,
-        Multiset.countp_pos] at this
+      rw [Multiset.countP_cons_of_pos _ (Associated.refl _), Nat.succ_le_succ_iff, ← not_lt,
+        Multiset.countP_pos] at this
       exact this ⟨b, b_in_s, assoc.symm⟩
 #align multiset.prod_primes_dvd Multiset.prod_primes_dvd
 
@@ -90,10 +90,10 @@ theorem Finset.prod_primes_dvd [CancelCommMonoidWithZero α] [Unique αˣ] {s :
         (by simpa only [Multiset.map_id', Finset.mem_def] using div)
         (by
           -- POrting note: was
-          -- `simp only [Multiset.map_id', associated_eq_eq, Multiset.countp_eq_card_filter, ←
+          -- `simp only [Multiset.map_id', associated_eq_eq, Multiset.countP_eq_card_filter, ←
           --    Multiset.count_eq_card_filter_eq, ← Multiset.nodup_iff_count_le_one, s.nodup]`
           intro a
-          simp only [Multiset.map_id', associated_eq_eq, Multiset.countp_eq_card_filter]
+          simp only [Multiset.map_id', associated_eq_eq, Multiset.countP_eq_card_filter]
           change Multiset.card (Multiset.filter (fun b => a = b) s.val) ≤ 1
           apply le_of_eq_of_le (Multiset.count_eq_card_filter_eq _ _).symm
           apply Multiset.nodup_iff_count_le_one.mp

Mathlib/Algebra/BigOperators/Basic.lean

@@ -1308,10 +1308,10 @@ theorem prod_list_count_of_subset [DecidableEq α] [CommMonoid α] (m : List α)
 #align finset.prod_list_count_of_subset Finset.prod_list_count_of_subset
 #align finset.sum_list_count_of_subset Finset.sum_list_count_of_subset
 
-theorem sum_filter_count_eq_countp [DecidableEq α] (p : α → Prop) [DecidablePred p] (l : List α) :
-    ∑ x in l.toFinset.filter p, l.count x = l.countp p := by
-  simp [Finset.sum, sum_map_count_dedup_filter_eq_countp p l]
-#align finset.sum_filter_count_eq_countp Finset.sum_filter_count_eq_countp
+theorem sum_filter_count_eq_countP [DecidableEq α] (p : α → Prop) [DecidablePred p] (l : List α) :
+    ∑ x in l.toFinset.filter p, l.count x = l.countP p := by
+  simp [Finset.sum, sum_map_count_dedup_filter_eq_countP p l]
+#align finset.sum_filter_count_eq_countp Finset.sum_filter_count_eq_countP
 
 open Multiset
 

Mathlib/Algebra/FreeMonoid/Count.lean

@@ -11,8 +11,8 @@ import Mathlib.Data.List.Count
 /-!
 # `List.count` as a bundled homomorphism
 
-In this file we define `FreeMonoid.countp`, `FreeMonoid.count`, `FreeAddMonoid.countp`, and
-`FreeAddMonoid.count`. These are `List.countp` and `List.count` bundled as multiplicative and
+In this file we define `FreeMonoid.countP`, `FreeMonoid.count`, `FreeAddMonoid.countP`, and
+`FreeAddMonoid.count`. These are `List.countP` and `List.count` bundled as multiplicative and
 additive homomorphisms from `FreeMonoid` and `FreeAddMonoid`.
 
 We do not use `to_additive` because it can't map `Multiplicative ℕ` to `ℕ`.
@@ -22,27 +22,27 @@ variable {α : Type*} (p : α → Prop) [DecidablePred p]
 
 namespace FreeAddMonoid
 
-/-- `List.countp` as a bundled additive monoid homomorphism. -/
-def countp : FreeAddMonoid α →+ ℕ where
-  toFun := List.countp p
-  map_zero' := List.countp_nil _
-  map_add' := List.countp_append _
-#align free_add_monoid.countp FreeAddMonoid.countp
+/-- `List.countP` as a bundled additive monoid homomorphism. -/
+def countP : FreeAddMonoid α →+ ℕ where
+  toFun := List.countP p
+  map_zero' := List.countP_nil _
+  map_add' := List.countP_append _
+#align free_add_monoid.countp FreeAddMonoid.countP
 
-theorem countp_of (x : α) : countp p (of x) = if p x = true then 1 else 0 := by
-  simp [countp, List.countp, List.countp.go]
-#align free_add_monoid.countp_of FreeAddMonoid.countp_of
+theorem countP_of (x : α) : countP p (of x) = if p x = true then 1 else 0 := by
+  simp [countP, List.countP, List.countP.go]
+#align free_add_monoid.countp_of FreeAddMonoid.countP_of
 
-theorem countp_apply (l : FreeAddMonoid α) : countp p l = List.countp p l := rfl
-#align free_add_monoid.countp_apply FreeAddMonoid.countp_apply
+theorem countP_apply (l : FreeAddMonoid α) : countP p l = List.countP p l := rfl
+#align free_add_monoid.countp_apply FreeAddMonoid.countP_apply
 
 /-- `List.count` as a bundled additive monoid homomorphism. -/
 -- Porting note: was (x = ·)
-def count [DecidableEq α] (x : α) : FreeAddMonoid α →+ ℕ := countp (· = x)
+def count [DecidableEq α] (x : α) : FreeAddMonoid α →+ ℕ := countP (· = x)
 #align free_add_monoid.count FreeAddMonoid.count
 
 theorem count_of [DecidableEq α] (x y : α) : count x (of y) = (Pi.single x 1 : α → ℕ) y := by
-  simp [Pi.single, Function.update, count, countp, List.countp, List.countp.go,
+  simp [Pi.single, Function.update, count, countP, List.countP, List.countP.go,
     Bool.beq_eq_decide_eq]
 #align free_add_monoid.count_of FreeAddMonoid.count_of
 
@@ -54,28 +54,28 @@ end FreeAddMonoid
 
 namespace FreeMonoid
 
-/-- `List.countp` as a bundled multiplicative monoid homomorphism. -/
-def countp : FreeMonoid α →* Multiplicative ℕ :=
-    AddMonoidHom.toMultiplicative (FreeAddMonoid.countp p)
-#align free_monoid.countp FreeMonoid.countp
+/-- `List.countP` as a bundled multiplicative monoid homomorphism. -/
+def countP : FreeMonoid α →* Multiplicative ℕ :=
+    AddMonoidHom.toMultiplicative (FreeAddMonoid.countP p)
+#align free_monoid.countp FreeMonoid.countP
 
-theorem countp_of' (x : α) :
-    countp p (of x) = if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0 := by
-    erw [FreeAddMonoid.countp_of]
+theorem countP_of' (x : α) :
+    countP p (of x) = if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0 := by
+    erw [FreeAddMonoid.countP_of]
     simp only [eq_iff_iff, iff_true, ofAdd_zero]; rfl
-#align free_monoid.countp_of' FreeMonoid.countp_of'
+#align free_monoid.countp_of' FreeMonoid.countP_of'
 
-theorem countp_of (x : α) : countp p (of x) = if p x then Multiplicative.ofAdd 1 else 1 := by
-  rw [countp_of', ofAdd_zero]
-#align free_monoid.countp_of FreeMonoid.countp_of
+theorem countP_of (x : α) : countP p (of x) = if p x then Multiplicative.ofAdd 1 else 1 := by
+  rw [countP_of', ofAdd_zero]
+#align free_monoid.countp_of FreeMonoid.countP_of
 
 -- `rfl` is not transitive
-theorem countp_apply (l : FreeAddMonoid α) : countp p l = Multiplicative.ofAdd (List.countp p l) :=
+theorem countP_apply (l : FreeAddMonoid α) : countP p l = Multiplicative.ofAdd (List.countP p l) :=
   rfl
-#align free_monoid.countp_apply FreeMonoid.countp_apply
+#align free_monoid.countp_apply FreeMonoid.countP_apply
 
 /-- `List.count` as a bundled additive monoid homomorphism. -/
-def count [DecidableEq α] (x : α) : FreeMonoid α →* Multiplicative ℕ := countp (· = x)
+def count [DecidableEq α] (x : α) : FreeMonoid α →* Multiplicative ℕ := countP (· = x)
 #align free_monoid.count FreeMonoid.count
 
 theorem count_apply [DecidableEq α] (x : α) (l : FreeAddMonoid α) :
@@ -84,7 +84,7 @@ theorem count_apply [DecidableEq α] (x : α) (l : FreeAddMonoid α) :
 
 theorem count_of [DecidableEq α] (x y : α) :
     count x (of y) = @Pi.mulSingle α (fun _ => Multiplicative ℕ) _ _ x (Multiplicative.ofAdd 1) y :=
-  by simp [count, countp_of, Pi.mulSingle_apply, eq_comm, Bool.beq_eq_decide_eq]
+  by simp [count, countP_of, Pi.mulSingle_apply, eq_comm, Bool.beq_eq_decide_eq]
 #align free_monoid.count_of FreeMonoid.count_of
 
 end FreeMonoid

Mathlib/Combinatorics/SimpleGraph/Trails.lean

@@ -18,7 +18,7 @@ as Eulerian circuits).
 ## Main definitions
 
 * `SimpleGraph.Walk.IsEulerian` is the predicate that a trail is an Eulerian trail.
-* `SimpleGraph.Walk.IsTrail.even_countp_edges_iff` gives a condition on the number of edges
+* `SimpleGraph.Walk.IsTrail.even_countP_edges_iff` gives a condition on the number of edges
   in a trail that can be incident to a given vertex.
 * `SimpleGraph.Walk.IsEulerian.even_degree_iff` gives a condition on the degrees of vertices
   when there exists an Eulerian trail.
@@ -51,13 +51,13 @@ def IsTrail.edgesFinset {u v : V} {p : G.Walk u v} (h : p.IsTrail) : Finset (Sym
 
 variable [DecidableEq V]
 
-theorem IsTrail.even_countp_edges_iff {u v : V} {p : G.Walk u v} (ht : p.IsTrail) (x : V) :
-    Even (p.edges.countp fun e => x ∈ e) ↔ u ≠ v → x ≠ u ∧ x ≠ v := by
+theorem IsTrail.even_countP_edges_iff {u v : V} {p : G.Walk u v} (ht : p.IsTrail) (x : V) :
+    Even (p.edges.countP fun e => x ∈ e) ↔ u ≠ v → x ≠ u ∧ x ≠ v := by
   induction' p with u u v w huv p ih
   · simp
   · rw [cons_isTrail_iff] at ht
     specialize ih ht.1
-    simp only [List.countp_cons, Ne.def, edges_cons, Sym2.mem_iff]
+    simp only [List.countP_cons, Ne.def, edges_cons, Sym2.mem_iff]
     split_ifs with h
     · rw [decide_eq_true_eq] at h
       obtain (rfl | rfl) := h
@@ -80,7 +80,7 @@ theorem IsTrail.even_countp_edges_iff {u v : V} {p : G.Walk u v} (ht : p.IsTrail
           simp only [imp_false, eq_self_iff_true, not_true, Classical.not_not] at h'
           cases h'
           simp only [not_true, and_false, false_and] at h
-#align simple_graph.walk.is_trail.even_countp_edges_iff SimpleGraph.Walk.IsTrail.even_countp_edges_iff
+#align simple_graph.walk.is_trail.even_countp_edges_iff SimpleGraph.Walk.IsTrail.even_countP_edges_iff
 
 /-- An *Eulerian trail* (also known as an "Eulerian path") is a walk
 `p` that visits every edge exactly once.  The lemma `SimpleGraph.Walk.IsEulerian.IsTrail` shows
@@ -101,7 +101,8 @@ theorem IsEulerian.isTrail {u v : V} {p : G.Walk u v} (h : p.IsEulerian) : p.IsT
 
 theorem IsEulerian.mem_edges_iff {u v : V} {p : G.Walk u v} (h : p.IsEulerian) {e : Sym2 V} :
     e ∈ p.edges ↔ e ∈ G.edgeSet :=
-  ⟨fun h => p.edges_subset_edgeSet h, fun he => by simpa using (h e he).ge⟩
+  ⟨ fun h => p.edges_subset_edgeSet h
+  , fun he => by apply List.count_pos_iff_mem.mp; simpa using (h e he).ge ⟩
 #align simple_graph.walk.is_eulerian.mem_edges_iff SimpleGraph.Walk.IsEulerian.mem_edges_iff
 
 /-- The edge set of an Eulerian graph is finite. -/
@@ -133,8 +134,8 @@ theorem IsEulerian.edgesFinset_eq [Fintype G.edgeSet] {u v : V} {p : G.Walk u v}
 
 theorem IsEulerian.even_degree_iff {x u v : V} {p : G.Walk u v} (ht : p.IsEulerian) [Fintype V]
     [DecidableRel G.Adj] : Even (G.degree x) ↔ u ≠ v → x ≠ u ∧ x ≠ v := by
-  convert ht.isTrail.even_countp_edges_iff x
-  rw [← Multiset.coe_countp, Multiset.countp_eq_card_filter, ← card_incidenceFinset_eq_degree]
+  convert ht.isTrail.even_countP_edges_iff x
+  rw [← Multiset.coe_countP, Multiset.countP_eq_card_filter, ← card_incidenceFinset_eq_degree]
   change Multiset.card _ = _
   congr 1
   convert_to _ = (ht.isTrail.edgesFinset.filter (Membership.mem x)).val

Mathlib/Data/Bool/Count.lean

@@ -23,8 +23,8 @@ namespace List
 @[simp]
 theorem count_not_add_count (l : List Bool) (b : Bool) : count (!b) l + count b l = length l := by
   -- Porting note: Proof re-written
-  -- Old proof: simp only [length_eq_countp_add_countp (Eq (!b)), Bool.not_not_eq, count]
-  simp only [length_eq_countp_add_countp (· == !b), count, add_right_inj]
+  -- Old proof: simp only [length_eq_countP_add_countP (Eq (!b)), Bool.not_not_eq, count]
+  simp only [length_eq_countP_add_countP (· == !b), count, add_right_inj]
   suffices : (fun x => x == b) = (fun a => decide ¬(a == !b) = true); rw [this]
   ext x; cases x <;> cases b <;> rfl
 #align list.count_bnot_add_count List.count_not_add_count
@@ -110,7 +110,7 @@ theorem two_mul_count_bool_eq_ite (hl : Chain' (· ≠ ·) l) (b : Bool) :
   · rw [if_pos h2, hl.two_mul_count_bool_of_even h2]
   · cases' l with x l
     · exact (h2 even_zero).elim
-    simp only [if_neg h2, count_cons', mul_add, head?, Option.mem_some_iff, @eq_comm _ x]
+    simp only [if_neg h2, count_cons, mul_add, head?, Option.mem_some_iff, @eq_comm _ x]
     rw [length_cons, Nat.even_add_one, not_not] at h2
     replace hl : l.Chain' (· ≠ ·) := hl.tail
     rw [hl.two_mul_count_bool_of_even h2]
@@ -138,4 +138,3 @@ theorem two_mul_count_bool_le_length_add_one (hl : Chain' (· ≠ ·) l) (b : Bo
 end Chain'
 
 end List
-

Mathlib/Data/Fintype/Fin.lean

@@ -87,7 +87,7 @@ theorem card_filter_univ_eq_vector_get_eq_count [DecidableEq α] (a : α) (v : V
   induction' v using Vector.inductionOn with n x xs hxs
   · simp
   · simp_rw [card_filter_univ_succ', Vector.get_cons_zero, Vector.toList_cons, Function.comp,
-      Vector.get_cons_succ, hxs, List.count_cons', add_comm (ite (a = x) 1 0)]
+      Vector.get_cons_succ, hxs, List.count_cons, add_comm (ite (a = x) 1 0)]
 #align fin.card_filter_univ_eq_vector_nth_eq_count Fin.card_filter_univ_eq_vector_get_eq_count
 
 end Fin