[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
b : α
l : List α
⊢ List.foldl (fun x y => op y x) b l = List.foldl op b l
[PROOFSTEP]
simp [hc.comm]
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
b a : α
s : Multiset α
⊢ fold op b (a ::ₘ s) = op (fold op b s) a
[PROOFSTEP]
simp [hc.comm]
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
b a : α
s : Multiset α
⊢ fold op b (a ::ₘ s) = fold op (op b a) s
[PROOFSTEP]
rw [fold_eq_foldl, foldl_cons, ← fold_eq_foldl]
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
b a : α
s : Multiset α
⊢ fold op b (a ::ₘ s) = fold op (op a b) s
[PROOFSTEP]
rw [fold_cons'_right, hc.comm]
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
b₁ b₂ : α
s₁ s₂ : Multiset α
⊢ fold op (op b₁ b₂) (s₁ + 0) = op (fold op b₁ s₁) (fold op b₂ 0)
[PROOFSTEP]
rw [add_zero, fold_zero, ← fold_cons'_right, ← fold_cons_right op]
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
b₁ b₂ : α
s₁ s₂ : Multiset α
a : α
b : Multiset α
h : fold op (op b₁ b₂) (s₁ + b) = op (fold op b₁ s₁) (fold op b₂ b)
⊢ fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (fold op b₂ (a ::ₘ b))
[PROOFSTEP]
rw [fold_cons_left, add_cons, fold_cons_left, h, ← ha.assoc, hc.comm a, ha.assoc]
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
ι : Type u_3
s : Multiset ι
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op (fold op b₀ (map b s)) (bind s t) = fold op b₀ (map (fun i => fold op (b i) (t i)) s)
[PROOFSTEP]
induction' s using Multiset.induction_on with a ha ih
[GOAL]
case empty
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
ι : Type u_3
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op (fold op b₀ (map b 0)) (bind 0 t) = fold op b₀ (map (fun i => fold op (b i) (t i)) 0)
[PROOFSTEP]
rw [zero_bind, map_zero, map_zero, fold_zero]
[GOAL]
case cons
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha✝ : IsAssociative α op
ι : Type u_3
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (bind ha t) = fold op b₀ (map (fun i => fold op (b i) (t i)) ha)
⊢ fold op (fold op b₀ (map b (a ::ₘ ha))) (bind (a ::ₘ ha) t) =
    fold op b₀ (map (fun i => fold op (b i) (t i)) (a ::ₘ ha))
[PROOFSTEP]
rw [cons_bind, map_cons, map_cons, fold_cons_left, fold_cons_left, fold_add, ih]
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
f g : β → α
u₁ u₂ : α
s : Multiset β
⊢ fold op (op u₁ u₂) (map (fun x => op (f x) (g x)) 0) = op (fold op u₁ (map f 0)) (fold op u₂ (map g 0))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
f g : β → α
u₁ u₂ : α
s : Multiset β
a : β
b : Multiset β
h : fold op (op u₁ u₂) (map (fun x => op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))
⊢ fold op (op u₁ u₂) (map (fun x => op (f x) (g x)) (a ::ₘ b)) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
[PROOFSTEP]
rw [map_cons, fold_cons_left, h, map_cons, fold_cons_left, map_cons, fold_cons_right, ha.assoc, ← ha.assoc (g a),
  hc.comm (g a), ha.assoc, hc.comm (g a), ha.assoc]
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
op' : β → β → β
inst✝¹ : IsCommutative β op'
inst✝ : IsAssociative β op'
m : α → β
hm : ∀ (x y : α), m (op x y) = op' (m x) (m y)
b : α
s : Multiset α
⊢ fold op' (m b) (map m 0) = m (fold op b 0)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
op' : β → β → β
inst✝¹ : IsCommutative β op'
inst✝ : IsAssociative β op'
m : α → β
hm : ∀ (x y : α), m (op x y) = op' (m x) (m y)
b : α
s : Multiset α
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    fold op' (m b) (map m s) = m (fold op b s) → fold op' (m b) (map m (a ::ₘ s)) = m (fold op b (a ::ₘ s))
[PROOFSTEP]
simp (config := { contextual := true }) [hm]
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
b₁ b₂ : α
⊢ op (fold op b₁ (s₁ ∪ s₂)) (fold op b₂ (s₁ ∩ s₂)) = op (fold op b₁ s₁) (fold op b₂ s₂)
[PROOFSTEP]
rw [← fold_add op, union_add_inter, fold_add op]
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
inst✝ : DecidableEq α
hi : IsIdempotent α op
s : Multiset α
b : α
⊢ fold op b (dedup 0) = fold op b 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
inst✝ : DecidableEq α
hi : IsIdempotent α op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b (dedup s) = fold op b s
⊢ fold op b (dedup (a ::ₘ s)) = fold op b (a ::ₘ s)
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
inst✝ : DecidableEq α
hi : IsIdempotent α op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b (dedup s) = fold op b s
h : a ∈ s
⊢ fold op b (dedup (a ::ₘ s)) = fold op b (a ::ₘ s)
[PROOFSTEP]
simp [IH, h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
inst✝ : DecidableEq α
hi : IsIdempotent α op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b (dedup s) = fold op b s
h : ¬a ∈ s
⊢ fold op b (dedup (a ::ₘ s)) = fold op b (a ::ₘ s)
[PROOFSTEP]
simp [IH, h]
[GOAL]
case pos
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
inst✝ : DecidableEq α
hi : IsIdempotent α op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b (dedup s) = fold op b s
h : a ∈ s
⊢ fold op b s = op a (fold op b s)
[PROOFSTEP]
show fold op b s = op a (fold op b s)
[GOAL]
case pos
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
inst✝ : DecidableEq α
hi : IsIdempotent α op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b (dedup s) = fold op b s
h : a ∈ s
⊢ fold op b s = op a (fold op b s)
[PROOFSTEP]
rw [← cons_erase h, fold_cons_left, ← ha.assoc, hi.idempotent]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : CanonicallyLinearOrderedAddMonoid α
l : Multiset α
n : α
h : ∀ (x : α), x ∈ l → x ≤ n
⊢ fold max ⊥ l ≤ n
[PROOFSTEP]
induction l using Quotient.inductionOn
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : CanonicallyLinearOrderedAddMonoid α
n : α
a✝ : List α
h : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) a✝ → x ≤ n
⊢ fold max ⊥ (Quotient.mk (List.isSetoid α) a✝) ≤ n
[PROOFSTEP]
simpa using List.max_le_of_forall_le _ _ h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ count a s ≤ count a (fold max 0 (map (fun a => count a s) s) • dedup s)
[PROOFSTEP]
rw [count_nsmul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * count a (dedup s)
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
refine' le_trans _ (Nat.mul_le_mul_left _ <| count_pos.2 <| mem_dedup.2 h)
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * succ 0
[PROOFSTEP]
have : count a s ≤ fold max 0 (map (fun a => count a s) (a ::ₘ erase s a)) := by simp [le_max_left]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ count a s ≤ fold max 0 (map (fun a => count a s) (a ::ₘ erase s a))
[PROOFSTEP]
simp [le_max_left]
[GOAL]
case pos
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [cons_erase h] at this 
[GOAL]
case pos
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simpa [mul_succ] using this
[GOAL]
case neg
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp [count_eq_zero.2 h, Nat.zero_le]
