From 86d5e52fc4272a989642f1d9187f3367c08748c7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sat, 7 Dec 2024 11:35:52 +0000 Subject: [PATCH] chore: don't import algebra in `Data.Finset.Basic` --- Mathlib/Algebra/Order/Group/Finset.lean | 33 +++++++++++++++++++ Mathlib/Algebra/Order/Group/Multiset.lean | 9 ++++- Mathlib/Algebra/Polynomial/FieldDivision.lean | 1 + Mathlib/Data/Finset/Basic.lean | 25 +------------- Mathlib/Data/Finset/Card.lean | 4 --- Mathlib/Data/Finset/Defs.lean | 4 +-- Mathlib/Data/Finset/Disjoint.lean | 8 ++--- Mathlib/Data/Finset/Lattice/Lemmas.lean | 2 +- Mathlib/Data/Finsupp/Multiset.lean | 1 + Mathlib/Data/Multiset/Dedup.lean | 14 ++------ Mathlib/Data/Multiset/NatAntidiagonal.lean | 6 ++-- Mathlib/Data/Multiset/Nodup.lean | 5 +-- Mathlib/Data/Multiset/Range.lean | 5 +-- Mathlib/Data/Multiset/Sum.lean | 9 ++--- Mathlib/RingTheory/Radical.lean | 1 + 15 files changed, 69 insertions(+), 58 deletions(-) diff --git a/Mathlib/Algebra/Order/Group/Finset.lean b/Mathlib/Algebra/Order/Group/Finset.lean index e08078aa0b808..e3f518734c79d 100644 --- a/Mathlib/Algebra/Order/Group/Finset.lean +++ b/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*} diff --git a/Mathlib/Algebra/Order/Group/Multiset.lean b/Mathlib/Algebra/Order/Group/Multiset.lean index 7fb63d8cd37e0..970a962cfde9c 100644 --- a/Mathlib/Algebra/Order/Group/Multiset.lean +++ b/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 diff --git a/Mathlib/Algebra/Polynomial/FieldDivision.lean b/Mathlib/Algebra/Polynomial/FieldDivision.lean index 36d71e8b2b9ee..07d250cccea6d 100644 --- a/Mathlib/Algebra/Polynomial/FieldDivision.lean +++ b/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 diff --git a/Mathlib/Data/Finset/Basic.lean b/Mathlib/Data/Finset/Basic.lean index b6901aef2d20c..30dcc372ee2cd 100644 --- a/Mathlib/Data/Finset/Basic.lean +++ b/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 diff --git a/Mathlib/Data/Finset/Card.lean b/Mathlib/Data/Finset/Card.lean index 3d203a0107b42..8c8e3dba2f006 100644 --- a/Mathlib/Data/Finset/Card.lean +++ b/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 diff --git a/Mathlib/Data/Finset/Defs.lean b/Mathlib/Data/Finset/Defs.lean index ff2e09b64a5eb..e63e94579aaed 100644 --- a/Mathlib/Data/Finset/Defs.lean +++ b/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 diff --git a/Mathlib/Data/Finset/Disjoint.lean b/Mathlib/Data/Finset/Disjoint.lean index fdb75054aba95..4ef7defc5e0a6 100644 --- a/Mathlib/Data/Finset/Disjoint.lean +++ b/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) := diff --git a/Mathlib/Data/Finset/Lattice/Lemmas.lean b/Mathlib/Data/Finset/Lattice/Lemmas.lean index c5783884b4b5a..32963dd45c201 100644 --- a/Mathlib/Data/Finset/Lattice/Lemmas.lean +++ b/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 diff --git a/Mathlib/Data/Finsupp/Multiset.lean b/Mathlib/Data/Finsupp/Multiset.lean index df6435246cdea..0ff33f764dd1d 100644 --- a/Mathlib/Data/Finsupp/Multiset.lean +++ b/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 diff --git a/Mathlib/Data/Multiset/Dedup.lean b/Mathlib/Data/Multiset/Dedup.lean index 7e580eb8e459b..07c9eabf1192c 100644 --- a/Mathlib/Data/Multiset/Dedup.lean +++ b/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] diff --git a/Mathlib/Data/Multiset/NatAntidiagonal.lean b/Mathlib/Data/Multiset/NatAntidiagonal.lean index b9d75740e9a1f..55e2353bf8752 100644 --- a/Mathlib/Data/Multiset/NatAntidiagonal.lean +++ b/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) = diff --git a/Mathlib/Data/Multiset/Nodup.lean b/Mathlib/Data/Multiset/Nodup.lean index 87bbfbd63a93a..66e5cd4680dd3 100644 --- a/Mathlib/Data/Multiset/Nodup.lean +++ b/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) diff --git a/Mathlib/Data/Multiset/Range.lean b/Mathlib/Data/Multiset/Range.lean index 82be6f025e6de..61399e9389712 100644 --- a/Mathlib/Data/Multiset/Range.lean +++ b/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 := diff --git a/Mathlib/Data/Multiset/Sum.lean b/Mathlib/Data/Multiset/Sum.lean index 0dd8540893604..66512fa587909 100644 --- a/Mathlib/Data/Multiset/Sum.lean +++ b/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₂ := diff --git a/Mathlib/RingTheory/Radical.lean b/Mathlib/RingTheory/Radical.lean index 8b60b67c3beb9..a213f7b39bfec 100644 --- a/Mathlib/RingTheory/Radical.lean +++ b/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