α : Type u_1
β : Type ?u.22330
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * count a (dedup s)
α : Type u_1
β : Type ?u.22330
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ count a s ≤ count a (fold max 0 (map (fun a => count a s) s) • dedup s)
rw [count_nsmul]
case pos
α : Type u_1
β : Type ?u.22330
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * count a (dedup s)

case neg
α : Type u_1
β : Type ?u.22330
inst✝ : DecidableEq α
s : Multiset α
a : α
h : ¬a ∈ s
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * count a (dedup s)
α : Type u_1
β : Type ?u.22330
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * count a (dedup s)
by_cases h : a ∈ s
case pos
α : Type u_1
β : Type ?u.22330
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * succ 0
case pos
α : Type u_1
β : Type ?u.22330
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * count a (dedup s)
refine' le_trans _ (Nat.mul_le_mul_left _ <| count_pos.2 <| mem_dedup.2 h)
case pos
α : Type u_1
β : Type ?u.22330
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
this : count a s ≤ fold max 0 (map (fun a => count a s) (a ::ₘ erase s a))
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * succ 0
case pos
α : Type u_1
β : Type ?u.22330
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * succ 0
have : count a s ≤ fold max 0 (map (fun a => count a s) (a ::ₘ erase s a)) :=
  by simp [le_max_left]
case pos
α : Type u_1
β : Type ?u.22330
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
case pos
α : Type u_1
β : Type ?u.22330
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
this : count a s ≤ fold max 0 (map (fun a => count a s) (a ::ₘ erase s a))
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * succ 0
rw [cons_erase h] at this
no goals
case pos
α : Type u_1
β : Type ?u.22330
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
simpa [mul_succ] using this
no goals
α : Type u_1
β : Type ?u.22330
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ count a s ≤ fold max 0 (map (fun a => count a s) (a ::ₘ erase s a))
simp [le_max_left]
no goals
case neg
α : Type u_1
β : Type ?u.22330
inst✝ : DecidableEq α
s : Multiset α
a : α
h : ¬a ∈ s
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * count a (dedup s)
simp [count_eq_zero.2 h, Nat.zero_le]