no goals
α : Type u_1
β : Type ?u.19437
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
inst✝ : DecidableEq α
hi : IsIdempotent α op
s : Multiset α
b : α
⊢ fold op b (dedup 0) = fold op b 0
simp
case pos
α : Type u_1
β : Type ?u.19437
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)
α : Type u_1
β : Type ?u.19437
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)
by_cases h : a ∈ s <;> simp [IH, h]
case pos
α : Type u_1
β : Type ?u.19437
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)
case pos
α : Type u_1
β : Type ?u.19437
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)
show fold op b s = op a (fold op b s)
no goals
case pos
α : Type u_1
β : Type ?u.19437
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)
rw [← cons_erase h, fold_cons_left, ← ha.assoc, hi.idempotent]