[Merged by Bors] - chore: don't import algebra in Data.Finset.Basic

Mathlib/Algebra/Order/Group/Finset.lean

@@ -14,8 +14,41 @@ import Mathlib.Data.Finset.Lattice.Fold
 # `Finset.sup` in a group
 -/
 
+open scoped Finset
+
 assert_not_exists MonoidWithZero
 
+namespace Multiset
+variable {α : Type*} [DecidableEq α]
+
+@[simp] lemma toFinset_nsmul (s : Multiset α) : ∀ n ≠ 0, (n • s).toFinset = s.toFinset
+  | 0, h => by contradiction
+  | n + 1, _ => by
+    by_cases h : n = 0
+    · rw [h, zero_add, one_nsmul]
+    · rw [add_nsmul, toFinset_add, one_nsmul, toFinset_nsmul s n h, Finset.union_idempotent]
+
+lemma toFinset_eq_singleton_iff (s : Multiset α) (a : α) :
+    s.toFinset = {a} ↔ card s ≠ 0 ∧ s = card s • {a} := by
+  refine ⟨fun H ↦ ⟨fun h ↦ ?_, ext' fun x ↦ ?_⟩, fun H ↦ ?_⟩
+  · rw [card_eq_zero.1 h, toFinset_zero] at H
+    exact Finset.singleton_ne_empty _ H.symm
+  · rw [count_nsmul, count_singleton]
+    by_cases hx : x = a
+    · simp_rw [hx, ite_true, mul_one, count_eq_card]
+      intro y hy
+      rw [← mem_toFinset, H, Finset.mem_singleton] at hy
+      exact hy.symm
+    have hx' : x ∉ s := fun h' ↦ hx <| by rwa [← mem_toFinset, H, Finset.mem_singleton] at h'
+    simp_rw [count_eq_zero_of_not_mem hx', hx, ite_false, Nat.mul_zero]
+  simpa only [toFinset_nsmul _ _ H.1, toFinset_singleton] using congr($(H.2).toFinset)
+
+lemma toFinset_card_eq_one_iff (s : Multiset α) :
+    #s.toFinset = 1 ↔ Multiset.card s ≠ 0 ∧ ∃ a : α, s = Multiset.card s • {a} := by
+  simp_rw [Finset.card_eq_one, Multiset.toFinset_eq_singleton_iff, exists_and_left]
+
+end Multiset
+
 namespace Finset
 variable {ι κ M G : Type*}
 

Mathlib/Algebra/Order/Group/Multiset.lean

@@ -7,7 +7,7 @@ import Mathlib.Algebra.Group.Hom.Defs
 import Mathlib.Algebra.Group.Nat.Basic
 import Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
 import Mathlib.Algebra.Order.Sub.Defs
-import Mathlib.Data.Multiset.Basic
+import Mathlib.Data.Multiset.Dedup
 
 /-!
 # Multisets form an ordered monoid
@@ -149,6 +149,13 @@ def countPAddMonoidHom : Multiset α →+ ℕ where
 
 end
 
+@[simp] lemma dedup_nsmul [DecidableEq α] {s : Multiset α} {n : ℕ} (hn : n ≠ 0) :
+    (n • s).dedup = s.dedup := by ext a; by_cases h : a ∈ s <;> simp [h, hn]
+
+lemma Nodup.le_nsmul_iff_le {s t : Multiset α} {n : ℕ} (h : s.Nodup) (hn : n ≠ 0) :
+    s ≤ n • t ↔ s ≤ t := by
+  classical simp [← h.le_dedup_iff_le, Iff.comm, ← h.le_dedup_iff_le, hn]
+
 /-! ### Multiplicity of an element -/
 
 section

Mathlib/Algebra/Polynomial/FieldDivision.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Kim Morrison, Jens Wagemaker
 -/
+import Mathlib.Algebra.Order.Group.Finset
 import Mathlib.Algebra.Polynomial.Derivative
 import Mathlib.Algebra.Polynomial.Eval.SMul
 import Mathlib.Algebra.Polynomial.Roots

Mathlib/Data/Finset/Basic.lean

@@ -48,7 +48,7 @@ assert_not_exists Multiset.powerset
 
 assert_not_exists CompleteLattice
 
-assert_not_exists OrderedCommMonoid
+assert_not_exists Monoid
 
 open Multiset Subtype Function
 
@@ -532,29 +532,6 @@ variable [DecidableEq α] {s t : Multiset α}
 theorem toFinset_add (s t : Multiset α) : toFinset (s + t) = toFinset s ∪ toFinset t :=
   Finset.ext <| by simp
 
-@[simp]
-theorem toFinset_nsmul (s : Multiset α) : ∀ n ≠ 0, (n • s).toFinset = s.toFinset
-  | 0, h => by contradiction
-  | n + 1, _ => by
-    by_cases h : n = 0
-    · rw [h, zero_add, one_nsmul]
-    · rw [add_nsmul, toFinset_add, one_nsmul, toFinset_nsmul s n h, Finset.union_idempotent]
-
-theorem toFinset_eq_singleton_iff (s : Multiset α) (a : α) :
-    s.toFinset = {a} ↔ card s ≠ 0 ∧ s = card s • {a} := by
-  refine ⟨fun H ↦ ⟨fun h ↦ ?_, ext' fun x ↦ ?_⟩, fun H ↦ ?_⟩
-  · rw [card_eq_zero.1 h, toFinset_zero] at H
-    exact Finset.singleton_ne_empty _ H.symm
-  · rw [count_nsmul, count_singleton]
-    by_cases hx : x = a
-    · simp_rw [hx, ite_true, mul_one, count_eq_card]
-      intro y hy
-      rw [← mem_toFinset, H, Finset.mem_singleton] at hy
-      exact hy.symm
-    have hx' : x ∉ s := fun h' ↦ hx <| by rwa [← mem_toFinset, H, Finset.mem_singleton] at h'
-    simp_rw [count_eq_zero_of_not_mem hx', hx, ite_false, Nat.mul_zero]
-  simpa only [toFinset_nsmul _ _ H.1, toFinset_singleton] using congr($(H.2).toFinset)
-
 @[simp]
 theorem toFinset_inter (s t : Multiset α) : toFinset (s ∩ t) = toFinset s ∩ toFinset t :=
   Finset.ext <| by simp

Mathlib/Data/Finset/Card.lean

@@ -610,10 +610,6 @@ theorem card_eq_one : #s = 1 ↔ ∃ a, s = {a} := by
   cases s
   simp only [Multiset.card_eq_one, Finset.card, ← val_inj, singleton_val]
 
-theorem _root_.Multiset.toFinset_card_eq_one_iff [DecidableEq α] (s : Multiset α) :
-    #s.toFinset = 1 ↔ Multiset.card s ≠ 0 ∧ ∃ a : α, s = Multiset.card s • {a} := by
-  simp_rw [card_eq_one, Multiset.toFinset_eq_singleton_iff, exists_and_left]
-
 theorem exists_eq_insert_iff [DecidableEq α] {s t : Finset α} :
     (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ #s + 1 = #t := by
   constructor

Mathlib/Data/Finset/Defs.lean

@@ -63,7 +63,7 @@ assert_not_exists DirectedSystem
 
 assert_not_exists CompleteLattice
 
-assert_not_exists OrderedCommMonoid
+assert_not_exists Monoid
 
 open Multiset Subtype Function
 
@@ -353,7 +353,7 @@ theorem sizeOf_lt_sizeOf_of_mem [SizeOf α] {x : α} {s : Finset α} (hx : x ∈
     SizeOf.sizeOf x < SizeOf.sizeOf s := by
   cases s
   dsimp [SizeOf.sizeOf, SizeOf.sizeOf, Multiset.sizeOf]
-  rw [add_comm]
+  rw [Nat.add_comm]
   refine lt_trans ?_ (Nat.lt_succ_self _)
   exact Multiset.sizeOf_lt_sizeOf_of_mem hx
 

Mathlib/Data/Finset/Disjoint.lean

@@ -27,7 +27,7 @@ assert_not_exists Multiset.powerset
 
 assert_not_exists CompleteLattice
 
-assert_not_exists OrderedCommMonoid
+assert_not_exists Monoid
 
 open Multiset Subtype Function
 
@@ -134,17 +134,17 @@ theorem coe_disjUnion {s t : Finset α} (h : Disjoint s t) :
 
 theorem disjUnion_comm (s t : Finset α) (h : Disjoint s t) :
     disjUnion s t h = disjUnion t s h.symm :=
-  eq_of_veq <| add_comm _ _
+  eq_of_veq <| Multiset.add_comm _ _
 
 @[simp]
 theorem empty_disjUnion (t : Finset α) (h : Disjoint ∅ t := disjoint_bot_left) :
     disjUnion ∅ t h = t :=
-  eq_of_veq <| zero_add _
+  eq_of_veq <| Multiset.zero_add _
 
 @[simp]
 theorem disjUnion_empty (s : Finset α) (h : Disjoint s ∅ := disjoint_bot_right) :
     disjUnion s ∅ h = s :=
-  eq_of_veq <| add_zero _
+  eq_of_veq <| Multiset.add_zero _
 
 theorem singleton_disjUnion (a : α) (t : Finset α) (h : Disjoint {a} t) :
     disjUnion {a} t h = cons a t (disjoint_singleton_left.mp h) :=

Mathlib/Data/Finset/Lattice/Lemmas.lean

@@ -25,7 +25,7 @@ assert_not_exists Multiset.powerset
 
 assert_not_exists CompleteLattice
 
-assert_not_exists OrderedCommMonoid
+assert_not_exists Monoid
 
 open Multiset Subtype Function
 

Mathlib/Data/Finsupp/Multiset.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
+import Mathlib.Algebra.Order.Group.Finset
 import Mathlib.Data.Finsupp.Basic
 import Mathlib.Data.Finsupp.Order
 

Mathlib/Data/Multiset/Dedup.lean

@@ -10,6 +10,7 @@ import Mathlib.Data.Multiset.Nodup
 # Erasing duplicates in a multiset.
 -/
 
+assert_not_exists Monoid
 
 namespace Multiset
 
@@ -104,11 +105,6 @@ theorem dedup_map_dedup_eq [DecidableEq β] (f : α → β) (s : Multiset α) :
     dedup (map f (dedup s)) = dedup (map f s) := by
   simp [dedup_ext]
 
-@[simp]
-theorem dedup_nsmul {s : Multiset α} {n : ℕ} (h0 : n ≠ 0) : (n • s).dedup = s.dedup := by
-  ext a
-  by_cases h : a ∈ s <;> simp [h, h0]
-
 theorem Nodup.le_dedup_iff_le {s t : Multiset α} (hno : s.Nodup) : s ≤ t.dedup ↔ s ≤ t := by
   simp [le_dedup, hno]
 
@@ -119,7 +115,7 @@ theorem Subset.dedup_add_right {s t : Multiset α} (h : s ⊆ t) :
 
 theorem Subset.dedup_add_left {s t : Multiset α} (h : t ⊆ s) :
     dedup (s + t) = dedup s := by
-  rw [add_comm, Subset.dedup_add_right h]
+  rw [s.add_comm, Subset.dedup_add_right h]
 
 theorem Disjoint.dedup_add {s t : Multiset α} (h : Disjoint s t) :
     dedup (s + t) = dedup s + dedup t := by
@@ -132,9 +128,3 @@ theorem _root_.List.Subset.dedup_append_left {s t : List α} (h : t ⊆ s) :
   rw [← coe_eq_coe, ← coe_dedup, ← coe_add, Subset.dedup_add_left h, coe_dedup]
 
 end Multiset
-
-theorem Multiset.Nodup.le_nsmul_iff_le {α : Type*} {s t : Multiset α} {n : ℕ} (h : s.Nodup)
-    (hn : n ≠ 0) : s ≤ n • t ↔ s ≤ t := by
-  classical
-    rw [← h.le_dedup_iff_le, Iff.comm, ← h.le_dedup_iff_le]
-    simp [hn]

Mathlib/Data/Multiset/NatAntidiagonal.lean

@@ -19,6 +19,8 @@ This refines file `Data.List.NatAntidiagonal` and is further refined by file
 `Data.Finset.NatAntidiagonal`.
 -/
 
+assert_not_exists Monoid
+
 namespace Multiset
 
 namespace Nat
@@ -55,8 +57,8 @@ theorem antidiagonal_succ {n : ℕ} :
 
 theorem antidiagonal_succ' {n : ℕ} :
     antidiagonal (n + 1) = (n + 1, 0) ::ₘ (antidiagonal n).map (Prod.map id Nat.succ) := by
-  rw [antidiagonal, List.Nat.antidiagonal_succ', ← coe_add, add_comm, antidiagonal, map_coe,
-    coe_add, List.singleton_append, cons_coe]
+  rw [antidiagonal, List.Nat.antidiagonal_succ', ← coe_add, Multiset.add_comm, antidiagonal,
+    map_coe, coe_add, List.singleton_append, cons_coe]
 
 theorem antidiagonal_succ_succ' {n : ℕ} :
     antidiagonal (n + 2) =

Mathlib/Data/Multiset/Nodup.lean

@@ -10,6 +10,7 @@ import Mathlib.Data.List.Pairwise
 # The `Nodup` predicate for multisets without duplicate elements.
 -/
 
+assert_not_exists Monoid
 
 namespace Multiset
 
@@ -62,7 +63,7 @@ theorem nodup_iff_ne_cons_cons {s : Multiset α} : s.Nodup ↔ ∀ a t, s ≠ a
   nodup_iff_le.trans
     ⟨fun h a _ s_eq => h a (s_eq.symm ▸ cons_le_cons a (cons_le_cons a (zero_le _))), fun h a le =>
       let ⟨t, s_eq⟩ := le_iff_exists_add.mp le
-      h a t (by rwa [cons_add, cons_add, zero_add] at s_eq)⟩
+      h a t (by rwa [cons_add, cons_add, Multiset.zero_add] at s_eq)⟩
 
 theorem nodup_iff_count_le_one [DecidableEq α] {s : Multiset α} : Nodup s ↔ ∀ a, count a s ≤ 1 :=
   Quot.induction_on s fun _l => by
@@ -193,7 +194,7 @@ theorem mem_sub_of_nodup [DecidableEq α] {a : α} {s t : Multiset α} (d : Nodu
       refine count_eq_zero.1 ?_ h
       rw [count_sub a s t, Nat.sub_eq_zero_iff_le]
       exact le_trans (nodup_iff_count_le_one.1 d _) (count_pos.2 h')⟩,
-    fun ⟨h₁, h₂⟩ => Or.resolve_right (mem_add.1 <| mem_of_le le_tsub_add h₁) h₂⟩
+    fun ⟨h₁, h₂⟩ => Or.resolve_right (mem_add.1 <| mem_of_le Multiset.le_sub_add h₁) h₂⟩
 
 theorem map_eq_map_of_bij_of_nodup (f : α → γ) (g : β → γ) {s : Multiset α} {t : Multiset β}
     (hs : s.Nodup) (ht : t.Nodup) (i : ∀ a ∈ s, β) (hi : ∀ a ha, i a ha ∈ t)

Mathlib/Data/Multiset/Range.lean

@@ -3,10 +3,11 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Mathlib.Algebra.Order.Group.Multiset
+import Mathlib.Data.Multiset.Basic
 
 /-! # `Multiset.range n` gives `{0, 1, ..., n-1}` as a multiset. -/
 
+assert_not_exists Monoid
 
 open List Nat
 
@@ -27,7 +28,7 @@ theorem range_zero : range 0 = 0 :=
 
 @[simp]
 theorem range_succ (n : ℕ) : range (succ n) = n ::ₘ range n := by
-  rw [range, List.range_succ, ← coe_add, add_comm]; rfl
+  rw [range, List.range_succ, ← coe_add, Multiset.add_comm]; rfl
 
 @[simp]
 theorem card_range (n : ℕ) : card (range n) = n :=

Mathlib/Data/Multiset/Sum.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
+import Mathlib.Algebra.Order.Group.Multiset
 import Mathlib.Data.Multiset.Nodup
 
 /-!
@@ -29,11 +30,11 @@ def disjSum : Multiset (α ⊕ β) :=
 
 @[simp]
 theorem zero_disjSum : (0 : Multiset α).disjSum t = t.map inr :=
-  zero_add _
+  Multiset.zero_add _
 
 @[simp]
 theorem disjSum_zero : s.disjSum (0 : Multiset β) = s.map inl :=
-  add_zero _
+  Multiset.add_zero _
 
 @[simp]
 theorem card_disjSum : Multiset.card (s.disjSum t) = Multiset.card s + Multiset.card t := by
@@ -64,11 +65,11 @@ theorem disjSum_mono (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) : s₁.disjSum t
   add_le_add (map_le_map hs) (map_le_map ht)
 
 theorem disjSum_mono_left (t : Multiset β) : Monotone fun s : Multiset α => s.disjSum t :=
-  fun _ _ hs => add_le_add_right (map_le_map hs) _
+  fun _ _ hs => Multiset.add_le_add_right (map_le_map hs)
 
 theorem disjSum_mono_right (s : Multiset α) :
     Monotone (s.disjSum : Multiset β → Multiset (α ⊕ β)) := fun _ _ ht =>
-  add_le_add_left (map_le_map ht) _
+  Multiset.add_le_add_left (map_le_map ht)
 
 theorem disjSum_lt_disjSum_of_lt_of_le (hs : s₁ < s₂) (ht : t₁ ≤ t₂) :
     s₁.disjSum t₁ < s₂.disjSum t₂ :=

Mathlib/RingTheory/Radical.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jineon Baek, Seewoo Lee
 -/
 import Mathlib.Algebra.EuclideanDomain.Basic
+import Mathlib.Algebra.Order.Group.Finset
 import Mathlib.RingTheory.Coprime.Basic
 import Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors