-- Mathlib/Algebra/Order/Group/Multiset.lean
theorem le_smul_dedup [DecidableEq α] (s : Multiset α) : ∃ n : ℕ, s ≤ n • dedup s :=
  ⟨(s.map fun a => count a s).fold max 0,
    le_iff_count.2 fun a => by
      rw [count_nsmul]; by_cases h : a ∈ s
      · refine le_trans ?_ (Nat.mul_le_mul_left _ <| count_pos.2 <| mem_dedup.2 h)
        have : count a s ≤ fold max 0 (map (fun a => count a s) (a ::ₘ erase s a))

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ count a s ≤ count a (fold max 0 (map (fun a => count a s) s) • s.dedup)

Tactic:
rw [count_nsmul]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * count a s.dedup

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∉ s
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * count a s.dedup

Tactic:
simp [count_eq_zero.2 h, Nat.zero_le]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * succ 0

Tactic:
have : count a s ≤ fold max 0 (map (fun a => count a s) (a ::ₘ erase s a)) := by
  simp [le_max_left]

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
this : count a s ≤ fold max 0 (map (fun a => count a s) (a ::ₘ s.erase a))
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * succ 0

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * count a s.dedup

Tactic:
by_cases h : a ∈ s

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * count a s.dedup

case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∉ s
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * count a s.dedup

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ count a s ≤ fold max 0 (map (fun a => count a s) (a ::ₘ s.erase a))

Tactic:
simp [le_max_left]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
this : count a s ≤ fold max 0 (map (fun a => count a s) (a ::ₘ s.erase a))
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * succ 0

Tactic:
rw [cons_erase h] at this

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
this : count a s ≤ fold max 0 (map (fun a => count a s) s)
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * succ 0

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
this : count a s ≤ fold max 0 (map (fun a => count a s) s)
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * succ 0

Tactic:
simpa [mul_succ] using this

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * count a s.dedup

Tactic:
refine le_trans ?_ (Nat.mul_le_mul_left _ <| count_pos.2 <| mem_dedup.2 h)

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * succ 0