From 92d78f806d65b42afc02a10ac50ff5c8b3acf60a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 8 Nov 2023 22:44:30 +0000 Subject: [PATCH] feat: `attach` and `filter` lemmas (#1470) Match https://github.com/leanprover-community/mathlib/pull/18087 --- Mathlib/Algebra/BigOperators/Basic.lean | 24 +++++++--- Mathlib/Algebra/BigOperators/Order.lean | 3 +- Mathlib/Data/Finset/Card.lean | 5 ++- Mathlib/Data/Finset/Image.lean | 21 ++++++++- Mathlib/Data/List/Basic.lean | 32 ++++++++++++- Mathlib/Data/List/Count.lean | 12 ++++- Mathlib/Data/List/Perm.lean | 4 +- Mathlib/Data/Multiset/Basic.lean | 57 +++++++++++++++++++----- Mathlib/Data/Multiset/Lattice.lean | 4 +- Mathlib/Data/Set/Finite.lean | 7 +-- Mathlib/NumberTheory/KummerDedekind.lean | 4 +- 11 files changed, 142 insertions(+), 31 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Basic.lean b/Mathlib/Algebra/BigOperators/Basic.lean index c0b3464d94b24..6e351bb8a017b 100644 --- a/Mathlib/Algebra/BigOperators/Basic.lean +++ b/Mathlib/Algebra/BigOperators/Basic.lean @@ -15,7 +15,7 @@ import Mathlib.Data.Fintype.Basic import Mathlib.Data.Multiset.Powerset import Mathlib.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 @@ -187,6 +187,12 @@ theorem prod_eq_multiset_prod [CommMonoid β] (s : Finset α) (f : α → β) : #align finset.prod_eq_multiset_prod Finset.prod_eq_multiset_prod #align finset.sum_eq_multiset_sum Finset.sum_eq_multiset_sum +@[to_additive (attr := simp)] +lemma 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 + @[to_additive] theorem prod_eq_fold [CommMonoid β] (s : Finset α) (f : α → β) : ∏ x in s, f x = s.fold ((· * ·) : β → β → β) 1 f := @@ -1775,11 +1781,19 @@ theorem sum_const_nat {m : ℕ} {f : α → ℕ} (h₁ : ∀ x ∈ s, f x = m) : apply sum_congr rfl h₁ #align finset.sum_const_nat Finset.sum_const_nat +lemma natCast_card_filter [AddCommMonoidWithOne β] (p) [DecidablePred p] (s : Finset α) : + ((filter p s).card : β) = ∑ a in s, if p a then (1 : β) else 0 := by + rw [sum_ite, sum_const_zero, add_zero, sum_const, nsmul_one] +#align finset.nat_cast_card_filter Finset.natCast_card_filter + +lemma card_filter (p) [DecidablePred p] (s : Finset α) : + (filter p s).card = ∑ a in s, ite (p a) 1 0 := natCast_card_filter _ _ +#align finset.card_filter Finset.card_filter + @[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, mul_zero] +lemma sum_boole {s : Finset α} {p : α → Prop} [AddCommMonoidWithOne β] [DecidablePred p] : + (∑ x in s, if p x then 1 else 0 : β) = (s.filter p).card := + (natCast_card_filter _ _).symm #align finset.sum_boole Finset.sum_boole theorem _root_.Commute.sum_right [NonUnitalNonAssocSemiring β] (s : Finset α) (f : α → β) (b : β) diff --git a/Mathlib/Algebra/BigOperators/Order.lean b/Mathlib/Algebra/BigOperators/Order.lean index 255bc7fab3fef..10be1fa609b8f 100644 --- a/Mathlib/Algebra/BigOperators/Order.lean +++ b/Mathlib/Algebra/BigOperators/Order.lean @@ -9,7 +9,7 @@ import Mathlib.Algebra.BigOperators.Basic import Mathlib.Data.Fintype.Card import Mathlib.Tactic.GCongr.Core -#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. @@ -223,7 +223,6 @@ theorem prod_le_pow_card (s : Finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s refine' (Multiset.prod_le_pow_card (s.val.map f) n _).trans _ · simpa using h · simp - rfl #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/Mathlib/Data/Finset/Card.lean b/Mathlib/Data/Finset/Card.lean index 87700bdf17acf..12e6f055a9999 100644 --- a/Mathlib/Data/Finset/Card.lean +++ b/Mathlib/Data/Finset/Card.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad import Mathlib.Init.CCLemmas import Mathlib.Data.Finset.Image -#align_import data.finset.card from "leanprover-community/mathlib"@"9003f28797c0664a49e4179487267c494477d853" +#align_import data.finset.card from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83" /-! # Cardinality of a finite set @@ -48,6 +48,9 @@ theorem card_def (s : Finset α) : s.card = Multiset.card s.1 := rfl #align finset.card_def Finset.card_def +@[simp] lemma card_val (s : Finset α) : Multiset.card s.1 = s.card := rfl +#align finset.card_val Finset.card_val + @[simp] theorem card_mk {m nodup} : (⟨m, nodup⟩ : Finset α).card = Multiset.card m := rfl diff --git a/Mathlib/Data/Finset/Image.lean b/Mathlib/Data/Finset/Image.lean index 9644e027cb155..d55dae3d7938e 100644 --- a/Mathlib/Data/Finset/Image.lean +++ b/Mathlib/Data/Finset/Image.lean @@ -8,7 +8,7 @@ import Mathlib.Data.Fin.Basic import Mathlib.Data.Finset.Basic import Mathlib.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 @@ -187,6 +187,25 @@ theorem filter_map {p : β → Prop} [DecidablePred p] : eq_of_veq (map_filter _ _ _) #align finset.filter_map Finset.filter_map +lemma map_filter' (p : α → Prop) [DecidablePred p] (f : α ↪ β) (s : Finset α) + [DecidablePred (∃ a, p a ∧ f a = ·)] : + (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' + +lemma 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' + +lemma filter_attach (p : α → Prop) [DecidablePred p] (s : Finset α) : + s.attach.filter (fun a : s ↦ p a) = + (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 + theorem map_filter {f : α ≃ β} {p : α → Prop} [DecidablePred p] : (s.filter p).map f.toEmbedding = (s.map f.toEmbedding).filter (p ∘ f.symm) := by simp only [filter_map, Function.comp, Equiv.toEmbedding_apply, Equiv.symm_apply_apply] diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean index 561d2d79515e8..f3e196d662443 100644 --- a/Mathlib/Data/List/Basic.lean +++ b/Mathlib/Data/List/Basic.lean @@ -10,7 +10,7 @@ import Mathlib.Init.Core import Std.Data.List.Lemmas import Mathlib.Tactic.Common -#align_import data.list.basic from "leanprover-community/mathlib"@"9da1b3534b65d9661eb8f42443598a92bbb49211" +#align_import data.list.basic from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83" /-! # Basic properties of lists @@ -2989,6 +2989,9 @@ end ModifyLast #align list.pmap List.pmap #align list.attach List.attach +@[simp] lemma attach_nil : ([] : List α).attach = [] := rfl +#align list.attach_nil List.attach_nil + theorem sizeOf_lt_sizeOf_of_mem [SizeOf α] {x : α} {l : List α} (hx : x ∈ l) : SizeOf.sizeOf x < SizeOf.sizeOf l := by induction' l with h t ih <;> cases hx <;> rw [cons.sizeOf_spec] @@ -3480,8 +3483,35 @@ theorem monotone_filter_right (l : List α) ⦃p q : α → Bool⦄ #align list.map_filter List.map_filter +lemma 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' + +lemma filter_attach' (l : List α) (p : {a // a ∈ l} → Bool) [DecidableEq α] : + l.attach.filter p = + (l.filter fun x => ∃ h, p ⟨x, h⟩).attach.map (Subtype.map id fun x => mem_of_mem_filter) := by + classical + refine' map_injective_iff.2 Subtype.coe_injective _ + simp [(· ∘ ·), map_filter' _ Subtype.coe_injective] +#align list.filter_attach' List.filter_attach' + +-- porting note: `Lean.Internal.coeM` forces us to type-ascript `{x // x ∈ l}` +lemma filter_attach (l : List α) (p : α → Bool) : + (l.attach.filter fun x => p x : List {x // x ∈ l}) = + (l.filter p).attach.map (Subtype.map id fun x => mem_of_mem_filter) := + map_injective_iff.2 Subtype.coe_injective <| by + simp_rw [map_map, (· ∘ ·), Subtype.map, id.def, ←Function.comp_apply (g := Subtype.val), + ←map_filter, attach_map_val] +#align list.filter_attach List.filter_attach + #align list.filter_filter List.filter_filter +lemma filter_comm (q) (l : List α) : filter p (filter q l) = filter q (filter p l) := by + simp [and_comm] +#align list.filter_comm List.filter_comm + @[simp] theorem filter_true (l : List α) : filter (fun _ => true) l = l := by induction l <;> simp [*, filter] diff --git a/Mathlib/Data/List/Count.lean b/Mathlib/Data/List/Count.lean index 656477bf8bca9..76536cfe8b31d 100644 --- a/Mathlib/Data/List/Count.lean +++ b/Mathlib/Data/List/Count.lean @@ -5,7 +5,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M -/ import Mathlib.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 @@ -71,6 +71,11 @@ theorem length_filter_lt_length_iff_exists (l) : #align list.countp_map List.countP_map +-- porting note: `Lean.Internal.coeM` forces us to type-ascript `{x // x ∈ l}` +lemma countP_attach (l : List α) : l.attach.countP (fun a : {x // x ∈ l} ↦ p a) = l.countP p := by + simp_rw [←Function.comp_apply (g := Subtype.val), ←countP_map, attach_map_val] +#align list.countp_attach List.countP_attach + #align list.countp_mono_left List.countP_mono_left #align list.countp_congr List.countP_congr @@ -147,6 +152,11 @@ theorem count_bind {α β} [DecidableEq β] (l : List α) (f : α → List β) ( count x (l.bind f) = sum (map (count x ∘ f) l) := by rw [List.bind, count_join, map_map] #align list.count_bind List.count_bind +@[simp] +lemma count_attach (a : {x // x ∈ l}) : l.attach.count a = l.count ↑a := + Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attach _ _ +#align list.count_attach List.count_attach + @[simp] theorem count_map_of_injective {α β} [DecidableEq α] [DecidableEq β] (l : List α) (f : α → β) (hf : Function.Injective f) (x : α) : count (f x) (map f l) = count x l := by diff --git a/Mathlib/Data/List/Perm.lean b/Mathlib/Data/List/Perm.lean index e4f63357f9e01..612425e42aa79 100644 --- a/Mathlib/Data/List/Perm.lean +++ b/Mathlib/Data/List/Perm.lean @@ -8,7 +8,7 @@ import Mathlib.Data.List.Permutation import Mathlib.Data.List.Range import Mathlib.Data.Nat.Factorial.Basic -#align_import data.list.perm from "leanprover-community/mathlib"@"47adfab39a11a072db552f47594bf8ed2cf8a722" +#align_import data.list.perm from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83" /-! # List Permutations @@ -475,7 +475,7 @@ theorem Subperm.countP_le (p : α → Bool) {l₁ l₂ : List α} : #align list.subperm.countp_le List.Subperm.countP_le theorem Perm.countP_congr (s : l₁ ~ l₂) {p p' : α → Bool} - (hp : ∀ x ∈ l₁, p x = p' x) : l₁.countP p = l₂.countP p' := by + (hp : ∀ x ∈ l₁, p x ↔ p' x) : l₁.countP p = l₂.countP p' := by rw [← s.countP_eq p'] clear s induction' l₁ with y s hs diff --git a/Mathlib/Data/Multiset/Basic.lean b/Mathlib/Data/Multiset/Basic.lean index a7fb99e13a8e7..90aa0f7396a06 100644 --- a/Mathlib/Data/Multiset/Basic.lean +++ b/Mathlib/Data/Multiset/Basic.lean @@ -7,7 +7,7 @@ import Mathlib.Data.Set.List import Mathlib.Data.List.Perm import Mathlib.Init.Quot -- Porting note: added import -#align_import data.multiset.basic from "leanprover-community/mathlib"@"06a655b5fcfbda03502f9158bbf6c0f1400886f9" +#align_import data.multiset.basic from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83" /-! # Multisets @@ -2091,6 +2091,10 @@ theorem filter_filter (q) [DecidablePred q] (s : Multiset α) : Quot.inductionOn s fun l => by simp #align multiset.filter_filter Multiset.filter_filter +lemma 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 + 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 := Multiset.induction_on s rfl fun a s IH => by by_cases p a <;> by_cases q a <;> simp [*] @@ -2108,6 +2112,12 @@ theorem map_filter (f : β → α) (s : Multiset β) : filter p (map f s) = map Quot.inductionOn s fun l => by simp [List.map_filter]; rfl #align multiset.map_filter Multiset.map_filter +lemma 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 -/ @@ -2312,6 +2322,25 @@ theorem countP_map (f : α → β) (s : Multiset α) (p : β → Prop) [Decidabl add_comm] #align multiset.countp_map Multiset.countP_map +-- porting note: `Lean.Internal.coeM` forces us to type-ascript `{a // a ∈ s}` +lemma countP_attach (s : Multiset α) : s.attach.countP (fun a : {a // a ∈ s} ↦ p a) = s.countP p := + Quotient.inductionOn s fun l => by + simp only [quot_mk_to_coe, coe_countP] + -- porting note: was + -- rw [quot_mk_to_coe, coe_attach, coe_countP] + -- exact List.countP_attach _ _ + rw [coe_attach] + refine (coe_countP _ _).trans ?_ + convert List.countP_attach _ _ + rfl +#align multiset.countp_attach Multiset.countP_attach + +lemma filter_attach (s : Multiset α) (p : α → Prop) [DecidablePred p] : + (s.attach.filter fun a : {a // a ∈ s} ↦ p ↑a) = + (s.filter p).attach.map (Subtype.map id fun _ ↦ Multiset.mem_of_mem_filter) := + Quotient.inductionOn s fun l ↦ congr_arg _ (List.filter_attach l p) +#align multiset.filter_attach Multiset.filter_attach + variable {p} theorem countP_pos {s} : 0 < countP p s ↔ ∃ a ∈ s, p a := @@ -2348,7 +2377,7 @@ end section -variable [DecidableEq α] +variable [DecidableEq α] {s : Multiset α} /-- `count a s` is the multiplicity of `a` in `s`. -/ def count (a : α) : Multiset α → ℕ := @@ -2421,6 +2450,11 @@ theorem count_nsmul (a : α) (n s) : count a (n • s) = n * count a s := by induction n <;> simp [*, succ_nsmul', succ_mul, zero_nsmul] #align multiset.count_nsmul Multiset.count_nsmul +@[simp] +lemma count_attach (a : {x // x ∈ s}) : s.attach.count a = s.count ↑a := + Eq.trans (countP_congr rfl fun _ _ => by simp [Subtype.ext_iff]) <| countP_attach _ _ +#align multiset.count_attach Multiset.count_attach + theorem count_pos {a : α} {s : Multiset α} : 0 < count a s ↔ a ∈ s := by simp [count, countP_pos] #align multiset.count_pos Multiset.count_pos @@ -2577,14 +2611,6 @@ theorem count_map_eq_count' [DecidableEq β] (f : α → β) (s : Multiset α) ( contradiction #align multiset.count_map_eq_count' Multiset.count_map_eq_count' -@[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 (Subtype.val : _ → α)).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 - theorem filter_eq' (s : Multiset α) (b : α) : s.filter (· = b) = replicate (count b s) b := Quotient.inductionOn s <| fun l => by simp only [quot_mk_to_coe, coe_filter, mem_coe, coe_count] @@ -2874,6 +2900,17 @@ theorem map_injective {f : α → β} (hf : Function.Injective f) : Function.Injective (Multiset.map f) := fun _x _y => (map_eq_map hf).1 #align multiset.map_injective Multiset.map_injective +lemma 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 ↦ mem_of_mem_filter) := by + classical + refine' Multiset.map_injective Subtype.val_injective _ + rw [map_filter' _ Subtype.val_injective] + simp only [Function.comp, Subtype.exists, coe_mk, + exists_and_right, exists_eq_right, attach_map_val, map_map, map_coe, id.def] +#align multiset.filter_attach' Multiset.filter_attach' + end Map section Quot diff --git a/Mathlib/Data/Multiset/Lattice.lean b/Mathlib/Data/Multiset/Lattice.lean index 49da3f57244df..1c2cad2b84065 100644 --- a/Mathlib/Data/Multiset/Lattice.lean +++ b/Mathlib/Data/Multiset/Lattice.lean @@ -6,7 +6,7 @@ Authors: Mario Carneiro import Mathlib.Data.Multiset.FinsetOps import Mathlib.Data.Multiset.Fold -#align_import data.multiset.lattice from "leanprover-community/mathlib"@"9003f28797c0664a49e4179487267c494477d853" +#align_import data.multiset.lattice from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83" /-! # Lattice operations on multisets @@ -55,6 +55,7 @@ theorem sup_add (s₁ s₂ : Multiset α) : (s₁ + s₂).sup = s₁.sup ⊔ s Eq.trans (by simp [sup]) (fold_add _ _ _ _ _) #align multiset.sup_add Multiset.sup_add +@[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]) @@ -139,6 +140,7 @@ theorem inf_add (s₁ s₂ : Multiset α) : (s₁ + s₂).inf = s₁.inf ⊓ s Eq.trans (by simp [inf]) (fold_add _ _ _ _ _) #align multiset.inf_add Multiset.inf_add +@[simp] theorem le_inf {s : Multiset α} {a : α} : a ≤ s.inf ↔ ∀ b ∈ s, a ≤ b := Multiset.induction_on s (by simp) (by simp (config := { contextual := true }) [or_imp, forall_and]) diff --git a/Mathlib/Data/Set/Finite.lean b/Mathlib/Data/Set/Finite.lean index a84e76c4a44dd..63e6a8f6503a2 100644 --- a/Mathlib/Data/Set/Finite.lean +++ b/Mathlib/Data/Set/Finite.lean @@ -7,7 +7,7 @@ import Mathlib.Data.Finset.Basic import Mathlib.Data.Set.Functor import Mathlib.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 @@ -1208,10 +1208,7 @@ theorem empty_card' {h : Fintype.{u} (∅ : Set α)} : @Fintype.card (∅ : Set theorem card_fintypeInsertOfNotMem {a : α} (s : Set α) [Fintype s] (h : a ∉ s) : @Fintype.card _ (fintypeInsertOfNotMem s h) = Fintype.card s + 1 := by - rw [fintypeInsertOfNotMem, Fintype.card_ofFinset] - simp only [Finset.card, toFinset, Finset.map_val, Embedding.coe_subtype, - Multiset.card_cons, Multiset.card_map, add_left_inj] - rfl + simp [fintypeInsertOfNotMem, Fintype.card_ofFinset] #align set.card_fintype_insert_of_not_mem Set.card_fintypeInsertOfNotMem @[simp] diff --git a/Mathlib/NumberTheory/KummerDedekind.lean b/Mathlib/NumberTheory/KummerDedekind.lean index f3ec94c3ec3d6..056e4a27284ab 100644 --- a/Mathlib/NumberTheory/KummerDedekind.lean +++ b/Mathlib/NumberTheory/KummerDedekind.lean @@ -6,7 +6,7 @@ Authors: Anne Baanen, Paul Lezeau import Mathlib.RingTheory.DedekindDomain.Ideal import Mathlib.RingTheory.IsAdjoinRoot -#align_import number_theory.kummer_dedekind from "leanprover-community/mathlib"@"f0c8bf9245297a541f468be517f1bde6195105e9" +#align_import number_theory.kummer_dedekind from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83" /-! # Kummer-Dedekind theorem @@ -297,7 +297,7 @@ theorem normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map (hI : I rw [Multiset.count_map_eq_count' fun f => ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk 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 (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx' _).prop · exact irreducible_of_normalized_factor _