[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s t : Multiset α
a : α
n : ℕ
⊢ ↑toDFinsupp (replicate n a) = DFinsupp.single a n
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s t : Multiset α
a : α
n : ℕ
i : α
⊢ ↑(↑toDFinsupp (replicate n a)) i = ↑(DFinsupp.single a n) i
[PROOFSTEP]
dsimp [toDFinsupp]
[GOAL]
case h
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s t : Multiset α
a : α
n : ℕ
i : α
⊢ count i (replicate n a) = ↑(DFinsupp.single a n) i
[PROOFSTEP]
simp [count_replicate, eq_comm]
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ ↑toDFinsupp {a} = DFinsupp.single a 1
[PROOFSTEP]
rw [← replicate_one, toDFinsupp_replicate]
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s t : Multiset α
⊢ AddMonoidHom.comp DFinsupp.toMultiset toDFinsupp = AddMonoidHom.id (Multiset α)
[PROOFSTEP]
ext
[GOAL]
case h.a
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s t : Multiset α
x✝ a✝ : α
⊢ count a✝ (↑(AddMonoidHom.comp DFinsupp.toMultiset toDFinsupp) {x✝}) = count a✝ (↑(AddMonoidHom.id (Multiset α)) {x✝})
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s t : Multiset α
⊢ AddMonoidHom.comp toDFinsupp DFinsupp.toMultiset = AddMonoidHom.id (Π₀ (x : α), ℕ)
[PROOFSTEP]
ext
[GOAL]
case H.a.h
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s t : Multiset α
x✝ i✝ : α
⊢ ↑(↑(AddMonoidHom.comp (AddMonoidHom.comp toDFinsupp DFinsupp.toMultiset) (DFinsupp.singleAddHom (fun i => ℕ) x✝)) 1)
      i✝ =
    ↑(↑(AddMonoidHom.comp (AddMonoidHom.id (Π₀ (x : α), ℕ)) (DFinsupp.singleAddHom (fun i => ℕ) x✝)) 1) i✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s t : Multiset α
⊢ ↑toDFinsupp s ≤ ↑toDFinsupp t ↔ s ≤ t
[PROOFSTEP]
simp [Multiset.le_iff_count, DFinsupp.le_def]
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s✝ t✝ s t : Multiset α
⊢ ↑toDFinsupp (s ∩ t) = ↑toDFinsupp s ⊓ ↑toDFinsupp t
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s✝ t✝ s t : Multiset α
i : α
⊢ ↑(↑toDFinsupp (s ∩ t)) i = ↑(↑toDFinsupp s ⊓ ↑toDFinsupp t) i
[PROOFSTEP]
simp [inf_eq_min]
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s✝ t✝ s t : Multiset α
⊢ ↑toDFinsupp (s ∪ t) = ↑toDFinsupp s ⊔ ↑toDFinsupp t
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
s✝ t✝ s t : Multiset α
i : α
⊢ ↑(↑toDFinsupp (s ∪ t)) i = ↑(↑toDFinsupp s ⊔ ↑toDFinsupp t) i
[PROOFSTEP]
simp [sup_eq_max]
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ ↑toMultiset f ≤ ↑toMultiset g ↔ f ≤ g
[PROOFSTEP]
simp_rw [← Multiset.toDFinsupp_le_toDFinsupp, toMultiset_toDFinsupp]
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ ↑toMultiset f < ↑toMultiset g ↔ f < g
[PROOFSTEP]
simp_rw [← Multiset.toDFinsupp_lt_toDFinsupp, toMultiset_toDFinsupp]
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ ↑Multiset.toDFinsupp (↑toMultiset (f ⊓ g)) = ↑Multiset.toDFinsupp (↑toMultiset f ∩ ↑toMultiset g)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ ↑Multiset.toDFinsupp (↑toMultiset (f ⊔ g)) = ↑Multiset.toDFinsupp (↑toMultiset f ∪ ↑toMultiset g)
[PROOFSTEP]
simp
