ι : Type ?u.938329
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
s : Multiset α
k : ℕ
h : ∀ (a : α), a ∈ s → k ∣ count a s
⊢ s = k • ∑ a in toFinset s, (count a s / k) • {a}
ι : Type ?u.938329
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
s : Multiset α
k : ℕ
h : ∀ (a : α), a ∈ s → k ∣ count a s
⊢ ∃ u, s = k • u
use ∑ a in s.toFinset, (s.count a / k) • {a}
ι : Type ?u.938329
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
s : Multiset α
k : ℕ
h : ∀ (a : α), a ∈ s → k ∣ count a s
h₂ : ∑ x in toFinset s, k • (count x s / k) • {x} = ∑ x in toFinset s, count x s • {x}
⊢ s = k • ∑ a in toFinset s, (count a s / k) • {a}
ι : Type ?u.938329
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
s : Multiset α
k : ℕ
h : ∀ (a : α), a ∈ s → k ∣ count a s
⊢ s = k • ∑ a in toFinset s, (count a s / k) • {a}
have h₂ :
  (∑ x : α in s.toFinset, k • (count x s / k) • ({x} : Multiset α)) =
    ∑ x : α in s.toFinset, count x s • {x} := by
  apply Finset.sum_congr rfl
  intro x hx
  rw [← mul_nsmul', Nat.mul_div_cancel' (h x (mem_toFinset.mp hx))]
no goals
ι : Type ?u.938329
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
s : Multiset α
k : ℕ
h : ∀ (a : α), a ∈ s → k ∣ count a s
h₂ : ∑ x in toFinset s, k • (count x s / k) • {x} = ∑ x in toFinset s, count x s • {x}
⊢ s = k • ∑ a in toFinset s, (count a s / k) • {a}
rw [← Finset.sum_nsmul, h₂, toFinset_sum_count_nsmul_eq]
ι : Type ?u.938329
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
s : Multiset α
k : ℕ
h : ∀ (a : α), a ∈ s → k ∣ count a s
⊢ ∀ (x : α), x ∈ toFinset s → k • (count x s / k) • {x} = count x s • {x}
ι : Type ?u.938329
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
s : Multiset α
k : ℕ
h : ∀ (a : α), a ∈ s → k ∣ count a s
⊢ ∑ x in toFinset s, k • (count x s / k) • {x} = ∑ x in toFinset s, count x s • {x}
apply Finset.sum_congr rfl
ι : Type ?u.938329
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
s : Multiset α
k : ℕ
h : ∀ (a : α), a ∈ s → k ∣ count a s
x : α
hx : x ∈ toFinset s
⊢ k • (count x s / k) • {x} = count x s • {x}
ι : Type ?u.938329
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
s : Multiset α
k : ℕ
h : ∀ (a : α), a ∈ s → k ∣ count a s
⊢ ∀ (x : α), x ∈ toFinset s → k • (count x s / k) • {x} = count x s • {x}
intro x hx
no goals
ι : Type ?u.938329
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
s : Multiset α
k : ℕ
h : ∀ (a : α), a ∈ s → k ∣ count a s
x : α
hx : x ∈ toFinset s
⊢ k • (count x s / k) • {x} = count x s • {x}
rw [← mul_nsmul', Nat.mul_div_cancel' (h x (mem_toFinset.mp hx))]