[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
a : α
n : ℕ
⊢ ↑toMultiset (single a n) = n • {a}
[PROOFSTEP]
rw [toMultiset_apply, sum_single_index]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
a : α
n : ℕ
⊢ 0 • {a} = 0
[PROOFSTEP]
apply zero_nsmul
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
s : Finset ι
n : ℕ
⊢ ↑toMultiset (∑ i in s, single i n) = n • s.val
[PROOFSTEP]
simp_rw [toMultiset_sum, Finsupp.toMultiset_single, sum_nsmul, sum_multiset_singleton]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : α →₀ ℕ
⊢ ↑Multiset.card (↑toMultiset f) = sum f fun x => id
[PROOFSTEP]
simp [toMultiset_apply, map_finsupp_sum, Function.id_def]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : α →₀ ℕ
g : α → β
⊢ Multiset.map g (↑toMultiset f) = ↑toMultiset (mapDomain g f)
[PROOFSTEP]
refine' f.induction _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
f : α →₀ ℕ
g : α → β
⊢ Multiset.map g (↑toMultiset 0) = ↑toMultiset (mapDomain g 0)
[PROOFSTEP]
rw [toMultiset_zero, Multiset.map_zero, mapDomain_zero, toMultiset_zero]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
f : α →₀ ℕ
g : α → β
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    ¬a ∈ f.support →
      b ≠ 0 →
        Multiset.map g (↑toMultiset f) = ↑toMultiset (mapDomain g f) →
          Multiset.map g (↑toMultiset (single a b + f)) = ↑toMultiset (mapDomain g (single a b + f))
[PROOFSTEP]
intro a n f _ _ ih
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : ¬a ∈ f.support
a✝ : n ≠ 0
ih : Multiset.map g (↑toMultiset f) = ↑toMultiset (mapDomain g f)
⊢ Multiset.map g (↑toMultiset (single a n + f)) = ↑toMultiset (mapDomain g (single a n + f))
[PROOFSTEP]
rw [toMultiset_add, Multiset.map_add, ih, mapDomain_add, mapDomain_single, toMultiset_single, toMultiset_add,
  toMultiset_single, ← Multiset.coe_mapAddMonoidHom, (Multiset.mapAddMonoidHom g).map_nsmul]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : ¬a ∈ f.support
a✝ : n ≠ 0
ih : Multiset.map g (↑toMultiset f) = ↑toMultiset (mapDomain g f)
⊢ n • ↑(Multiset.mapAddMonoidHom g) {a} + ↑toMultiset (mapDomain g f) = n • {g a} + ↑toMultiset (mapDomain g f)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ Multiset.prod (↑toMultiset f) = prod f fun a n => a ^ n
[PROOFSTEP]
refine' f.induction _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ Multiset.prod (↑toMultiset 0) = prod 0 fun a n => a ^ n
[PROOFSTEP]
rw [toMultiset_zero, Multiset.prod_zero, Finsupp.prod_zero_index]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    ¬a ∈ f.support →
      b ≠ 0 →
        (Multiset.prod (↑toMultiset f) = prod f fun a n => a ^ n) →
          Multiset.prod (↑toMultiset (single a b + f)) = prod (single a b + f) fun a n => a ^ n
[PROOFSTEP]
intro a n f _ _ ih
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : ¬a ∈ f.support
a✝ : n ≠ 0
ih : Multiset.prod (↑toMultiset f) = prod f fun a n => a ^ n
⊢ Multiset.prod (↑toMultiset (single a n + f)) = prod (single a n + f) fun a n => a ^ n
[PROOFSTEP]
rw [toMultiset_add, Multiset.prod_add, ih, toMultiset_single, Multiset.prod_nsmul,
  Finsupp.prod_add_index' pow_zero pow_add, Finsupp.prod_single_index, Multiset.prod_singleton]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : ¬a ∈ f.support
a✝ : n ≠ 0
ih : Multiset.prod (↑toMultiset f) = prod f fun a n => a ^ n
⊢ a ^ 0 = 1
[PROOFSTEP]
exact pow_zero a
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ Multiset.toFinset (↑toMultiset f) = f.support
[PROOFSTEP]
refine' f.induction _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ Multiset.toFinset (↑toMultiset 0) = 0.support
[PROOFSTEP]
rw [toMultiset_zero, Multiset.toFinset_zero, support_zero]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    ¬a ∈ f.support →
      b ≠ 0 →
        Multiset.toFinset (↑toMultiset f) = f.support →
          Multiset.toFinset (↑toMultiset (single a b + f)) = (single a b + f).support
[PROOFSTEP]
intro a n f ha hn ih
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : ¬a ∈ f.support
hn : n ≠ 0
ih : Multiset.toFinset (↑toMultiset f) = f.support
⊢ Multiset.toFinset (↑toMultiset (single a n + f)) = (single a n + f).support
[PROOFSTEP]
rw [toMultiset_add, Multiset.toFinset_add, ih, toMultiset_single, support_add_eq, support_single_ne_zero _ hn,
  Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : ¬a ∈ f.support
hn : n ≠ 0
ih : Multiset.toFinset (↑toMultiset f) = f.support
⊢ Disjoint (single a n).support f.support
[PROOFSTEP]
refine' Disjoint.mono_left support_single_subset _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : ¬a ∈ f.support
hn : n ≠ 0
ih : Multiset.toFinset (↑toMultiset f) = f.support
⊢ Disjoint {a} f.support
[PROOFSTEP]
rwa [Finset.disjoint_singleton_left]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Multiset.count a (↑toMultiset f) = sum f fun x n => Multiset.count a (n • {x})
[PROOFSTEP]
rw [toMultiset_apply]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Multiset.count a (sum f fun a n => n • {a}) = sum f fun x n => Multiset.count a (n • {x})
[PROOFSTEP]
exact map_sum (Multiset.countAddMonoidHom a) _ f.support
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ (sum f fun x n => Multiset.count a (n • {x})) = sum f fun x n => n * Multiset.count a {x}
[PROOFSTEP]
simp only [Multiset.count_nsmul]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
a a' : α
x✝ : a' ∈ f.support
H : a' ≠ a
⊢ (fun x n => n * Multiset.count a {x}) a' (↑f a') = 0
[PROOFSTEP]
simp only [Multiset.count_singleton, if_false, H.symm, mul_zero]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
H : ¬a ∈ f.support
⊢ (fun x n => n * Multiset.count a {x}) a (↑f a) = 0
[PROOFSTEP]
simp only [not_mem_support_iff.1 H, zero_mul]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ ↑f a * Multiset.count a {a} = ↑f a
[PROOFSTEP]
rw [Multiset.count_singleton_self, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : α →₀ ℕ
i : α
⊢ i ∈ ↑toMultiset f ↔ i ∈ f.support
[PROOFSTEP]
classical rw [← Multiset.count_ne_zero, Finsupp.count_toMultiset, Finsupp.mem_support_iff]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : α →₀ ℕ
i : α
⊢ i ∈ ↑toMultiset f ↔ i ∈ f.support
[PROOFSTEP]
rw [← Multiset.count_ne_zero, Finsupp.count_toMultiset, Finsupp.mem_support_iff]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ a ∈ toFinset s ↔ (fun a => count a s) a ≠ 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
s : Multiset α
⊢ (fun f => ↑Finsupp.toMultiset f)
      ((fun s =>
          { support := toFinset s, toFun := fun a => count a s,
            mem_support_toFun := (_ : ∀ (a : α), a ∈ toFinset s ↔ ¬count a s = 0) })
        s) =
    s
[PROOFSTEP]
simp only [Finsupp.toMultiset_apply, Finsupp.sum, Finsupp.coe_mk, Multiset.toFinset_sum_count_nsmul_eq]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ ↑((fun s =>
            { support := toFinset s, toFun := fun a => count a s,
              mem_support_toFun := (_ : ∀ (a : α), a ∈ toFinset s ↔ ¬count a s = 0) })
          ((fun f => ↑Finsupp.toMultiset f) f))
      a =
    ↑f a
[PROOFSTEP]
simp only [Finsupp.toMultiset_apply, Finsupp.sum, Multiset.count_sum', Multiset.count_singleton, mul_boole,
  Finsupp.coe_mk, Finsupp.mem_support_iff, Multiset.count_nsmul, Finset.sum_ite_eq, ite_not, ite_eq_right_iff]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ ↑f a = 0 → 0 = ↑f a
[PROOFSTEP]
exact Eq.symm
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
a : α
⊢ ↑toFinsupp {a} = Finsupp.single a 1
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
a a✝ : α
⊢ ↑(↑toFinsupp {a}) a✝ = ↑(Finsupp.single a 1) a✝
[PROOFSTEP]
rw [toFinsupp_apply, count_singleton, Finsupp.single_eq_pi_single, Pi.single_apply]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq ι
f g : ι →₀ ℕ
⊢ ↑(AddEquiv.symm Multiset.toFinsupp).toEquiv f ≤ ↑(AddEquiv.symm Multiset.toFinsupp).toEquiv g ↔ f ≤ g
[PROOFSTEP]
simp [le_def, Multiset.le_iff_count]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
⊢ StrictMono ↑toMultiset
[PROOFSTEP]
classical exact (@orderIsoMultiset ι _).strictMono
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
⊢ StrictMono ↑toMultiset
[PROOFSTEP]
exact (@orderIsoMultiset ι _).strictMono
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m n : ι →₀ ℕ
h : m < n
⊢ (sum m fun x => id) < sum n fun x => id
[PROOFSTEP]
rw [← card_toMultiset, ← card_toMultiset]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m n : ι →₀ ℕ
h : m < n
⊢ ↑Multiset.card (↑toMultiset m) < ↑Multiset.card (↑toMultiset n)
[PROOFSTEP]
apply Multiset.card_lt_of_lt
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
m n : ι →₀ ℕ
h : m < n
⊢ ↑toMultiset m < ↑toMultiset n
[PROOFSTEP]
exact toMultiset_strictMono h
