/-
Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro

! This file was ported from Lean 3 source module data.multiset.fold
! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Multiset.Dedup
import Mathlib.Data.List.MinMax

/-!
# The fold operation for a commutative associative operation over a multiset.
-/


namespace Multiset

variable {
α: Type ?u.4793
α 
β: Type ?u.5
β : 
Type _: Type (?u.5+1)
Type _}

/-! ### fold -/


section Fold

variable (
op: α → α → α
op : 
α: Type ?u.8
α → 
α: Type ?u.8
α → 
α: Type ?u.8
α) [
hc: IsCommutative α op
hc : 
IsCommutative: (α : Type ?u.3279) → (α → α → α) → Prop
IsCommutative 
α: Type ?u.152
α 
op: α → α → α
op] [
ha: IsAssociative α op
ha : 
IsAssociative: (α : Type ?u.3284) → (α → α → α) → Prop
IsAssociative 
α: Type ?u.152
α 
op: α → α → α
op]

local notation 
a: ?m.236
a " * " 
b: ?m.227
b => op 
a: ?m.236
a 
b: ?m.227
b

/-- `fold op b s` folds a commutative associative operation `op` over
  the multiset `s`. -/
def 
fold: α → Multiset α → α
fold : 
α: Type ?u.2302
α → 
Multiset: Type ?u.2327 → Type ?u.2327
Multiset 
α: Type ?u.2302
α → 
α: Type ?u.2302
α :=
  
foldr: {α : Type ?u.2331} → {β : Type ?u.2330} → (f : α → β → β) → LeftCommutative f → β → Multiset α → β
foldr 
op: α → α → α
op (
left_comm: ∀ {α : Type ?u.2345} (f : α → α → α), Commutative f → Associative f → LeftCommutative f
left_comm 
_: ?m.2346 → ?m.2346 → ?m.2346
_ 
hc: IsCommutative α op
hc.
comm: ∀ {α : Type ?u.2358} {op : α → α → α} [self : IsCommutative α op] (a b : α), op a b = op b a
comm 
ha: IsAssociative α op
ha.
assoc: ∀ {α : Type ?u.2369} {op : α → α → α} [self : IsAssociative α op] (a b c : α), op (op a b) c = op a (op b c)
assoc)
#align multiset.fold 
Multiset.fold: {α : Type u_1} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
Multiset.fold

theorem 
fold_eq_foldr: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (s : Multiset α),
  fold op b s = foldr op (_ : LeftCommutative op) b s
fold_eq_foldr (
b: α
b : 
α: Type ?u.2489
α) (
s: Multiset α
s : 
Multiset: Type ?u.2513 → Type ?u.2513
Multiset 
α: Type ?u.2489
α) :
    
fold: {α : Type ?u.2517} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b: α
b 
s: Multiset α
s = 
foldr: {α : Type ?u.2547} → {β : Type ?u.2546} → (f : α → β → β) → LeftCommutative f → β → Multiset α → β
foldr 
op: α → α → α
op (
left_comm: ∀ {α : Type ?u.2556} (f : α → α → α), Commutative f → Associative f → LeftCommutative f
left_comm 
_: ?m.2557 → ?m.2557 → ?m.2557
_ 
hc: IsCommutative α op
hc.
comm: ∀ {α : Type ?u.2569} {op : α → α → α} [self : IsCommutative α op] (a b : α), op a b = op b a
comm 
ha: IsAssociative α op
ha.
assoc: ∀ {α : Type ?u.2576} {op : α → α → α} [self : IsAssociative α op] (a b c : α), op (op a b) c = op a (op b c)
assoc) 
b: α
b 
s: Multiset α
s :=
  
rfl: ∀ {α : Sort ?u.2591} {a : α}, a = a
rfl
#align multiset.fold_eq_foldr 
Multiset.fold_eq_foldr: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (s : Multiset α),
  fold op b s = foldr op (_ : LeftCommutative op) b s
Multiset.fold_eq_foldr

@[simp]
theorem 
coe_fold_r: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (l : List α),
  fold op b ↑l = List.foldr op b l
coe_fold_r (
b: α
b : 
α: Type ?u.2618
α) (
l: List α
l : 
List: Type ?u.2642 → Type ?u.2642
List 
α: Type ?u.2618
α) : 
fold: {α : Type ?u.2646} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b: α
b 
l: List α
l = 
l: List α
l.
foldr: {α : Type ?u.2782} → {β : Type ?u.2781} → (α → β → β) → β → List α → β
foldr 
op: α → α → α
op 
b: α
b :=
  
rfl: ∀ {α : Sort ?u.2800} {a : α}, a = a
rfl
#align multiset.coe_fold_r 
Multiset.coe_fold_r: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (l : List α),
  fold op b ↑l = List.foldr op b l
Multiset.coe_fold_r

theorem 
coe_fold_l: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (l : List α),
  fold op b ↑l = List.foldl op b l
coe_fold_l (
b: α
b : 
α: Type ?u.2858
α) (
l: List α
l : 
List: Type ?u.2882 → Type ?u.2882
List 
α: Type ?u.2858
α) : 
fold: {α : Type ?u.2886} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b: α
b 
l: List α
l = 
l: List α
l.
foldl: {α : Type ?u.3022} → {β : Type ?u.3021} → (α → β → α) → α → List β → α
foldl 
op: α → α → α
op 
b: α
b :=
  (
coe_foldr_swap: ∀ {α : Type ?u.3040} {β : Type ?u.3041} (f : α → β → β) (H : LeftCommutative f) (b : β) (l : List α),
  foldr f H b ↑l = List.foldl (fun x y => f y x) b l
coe_foldr_swap 
op: α → α → α
op 
_: LeftCommutative op
_ 
b: α
b 
l: List α
l).
trans: ∀ {α : Sort ?u.3052} {a b c : α}, a = b → b = c → a = c
trans <| by
Goals accomplished! 🐙 
α: Type u_1

β: Type ?u.2861

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

b: α

l: List α

List.foldl (fun x y => op y x) b l = List.foldl op b lsimp [
hc: IsCommutative α op
hc.
comm: ∀ {α : Type ?u.3098} {op : α → α → α} [self : IsCommutative α op] (a b : α), op a b = op b a
comm]
Goals accomplished! 🐙
#align multiset.coe_fold_l 
Multiset.coe_fold_l: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (l : List α),
  fold op b ↑l = List.foldl op b l
Multiset.coe_fold_l

theorem 
fold_eq_foldl: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (s : Multiset α),
  fold op b s = foldl op (_ : RightCommutative op) b s
fold_eq_foldl (
b: α
b : 
α: Type ?u.3267
α) (
s: Multiset α
s : 
Multiset: Type ?u.3291 → Type ?u.3291
Multiset 
α: Type ?u.3267
α) :
    
fold: {α : Type ?u.3295} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b: α
b 
s: Multiset α
s = 
foldl: {α : Type ?u.3325} → {β : Type ?u.3324} → (f : β → α → β) → RightCommutative f → β → Multiset α → β
foldl 
op: α → α → α
op (
right_comm: ∀ {α : Type ?u.3334} (f : α → α → α), Commutative f → Associative f → RightCommutative f
right_comm 
_: ?m.3335 → ?m.3335 → ?m.3335
_ 
hc: IsCommutative α op
hc.
comm: ∀ {α : Type ?u.3347} {op : α → α → α} [self : IsCommutative α op] (a b : α), op a b = op b a
comm 
ha: IsAssociative α op
ha.
assoc: ∀ {α : Type ?u.3354} {op : α → α → α} [self : IsAssociative α op] (a b c : α), op (op a b) c = op a (op b c)
assoc) 
b: α
b 
s: Multiset α
s :=
  
Quot.inductionOn: ∀ {α : Sort ?u.3369} {r : α → α → Prop} {motive : Quot r → Prop} (q : Quot r),
  (∀ (a : α), motive (Quot.mk r a)) → motive q
Quot.inductionOn 
s: Multiset α
s fun 
_: ?m.3401
_ => 
coe_fold_l: ∀ {α : Type ?u.3403} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (l : List α),
  fold op b ↑l = List.foldl op b l
coe_fold_l 
_: ?m.3404 → ?m.3404 → ?m.3404
_ 
_: ?m.3404
_ 
_: List ?m.3404
_
#align multiset.fold_eq_foldl 
Multiset.fold_eq_foldl: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (s : Multiset α),
  fold op b s = foldl op (_ : RightCommutative op) b s
Multiset.fold_eq_foldl

@[simp]
theorem 
fold_zero: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α), fold op b 0 = b
fold_zero (
b: α
b : 
α: Type ?u.3514
α) : (
0: ?m.3542
0 : 
Multiset: Type ?u.3540 → Type ?u.3540
Multiset 
α: Type ?u.3514
α).
fold: {α : Type ?u.3571} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b: α
b = 
b: α
b :=
  
rfl: ∀ {α : Sort ?u.3608} {a : α}, a = a
rfl
#align multiset.fold_zero 
Multiset.fold_zero: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α), fold op b 0 = b
Multiset.fold_zero

@[simp]
theorem 
fold_cons_left: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b a : α) (s : Multiset α),
  fold op b (a ::ₘ s) = op a (fold op b s)
fold_cons_left : ∀ (
b: α
b 
a: α
a : 
α: Type ?u.3653
α) (
s: Multiset α
s : 
Multiset: Type ?u.3680 → Type ?u.3680
Multiset 
α: Type ?u.3653
α), (
a: α
a ::ₘ 
s: Multiset α
s).
fold: {α : Type ?u.3687} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b: α
b = 
a: α
a * 
s: Multiset α
s.
fold: {α : Type ?u.3721} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b: α
b :=
  
foldr_cons: ∀ {α : Type ?u.4722} {β : Type ?u.4723} (f : α → β → β) (H : LeftCommutative f) (b : β) (a : α) (s : Multiset α),
  foldr f H b (a ::ₘ s) = f a (foldr f H b s)
foldr_cons 
_: ?m.4724 → ?m.4725 → ?m.4725
_ 
_: LeftCommutative ?m.4726
_
#align multiset.fold_cons_left 
Multiset.fold_cons_left: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b a : α) (s : Multiset α),
  fold op b (a ::ₘ s) = op a (fold op b s)
Multiset.fold_cons_left

theorem 
fold_cons_right: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b a : α) (s : Multiset α),
  fold op b (a ::ₘ s) = op (fold op b s) a
fold_cons_right (
b: α
b 
a: α
a : 
α: Type ?u.4793
α) (
s: Multiset α
s : 
Multiset: Type ?u.4819 → Type ?u.4819
Multiset 
α: Type ?u.4793
α) : (
a: α
a ::ₘ 
s: Multiset α
s).
fold: {α : Type ?u.4826} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b: α
b = 
s: Multiset α
s.
fold: {α : Type ?u.4860} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b: α
b * 
a: α
a := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.4796

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

b, a: α

s: Multiset α

fold op b (a ::ₘ s) = op (fold op b s) asimp [
hc: IsCommutative α op
hc.
comm: ∀ {α : Type ?u.5867} {op : α → α → α} [self : IsCommutative α op] (a b : α), op a b = op b a
comm]
Goals accomplished! 🐙
#align multiset.fold_cons_right 
Multiset.fold_cons_right: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b a : α) (s : Multiset α),
  fold op b (a ::ₘ s) = op (fold op b s) a
Multiset.fold_cons_right

theorem 
fold_cons'_right: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b a : α) (s : Multiset α),
  fold op b (a ::ₘ s) = fold op (op b a) s
fold_cons'_right (
b: α
b 
a: α
a : 
α: Type ?u.6036
α) (
s: Multiset α
s : 
Multiset: Type ?u.6062 → Type ?u.6062
Multiset 
α: Type ?u.6036
α) : (
a: α
a ::ₘ 
s: Multiset α
s).
fold: {α : Type ?u.6069} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b: α
b = 
s: Multiset α
s.
fold: {α : Type ?u.6103} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op (
b: α
b * 
a: α
a) := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.6039

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

b, a: α

s: Multiset α

fold op b (a ::ₘ s) = fold op (op b a) srw [
α: Type u_1

β: Type ?u.6039

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

b, a: α

s: Multiset α

fold op b (a ::ₘ s) = fold op (op b a) s
fold_eq_foldl: ∀ {α : Type ?u.7093} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (s : Multiset α),
  fold op b s = foldl op (_ : RightCommutative op) b s
fold_eq_foldl,
α: Type u_1

β: Type ?u.6039

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

b, a: α

s: Multiset α

foldl op (_ : RightCommutative op) b (a ::ₘ s) = fold op (op b a) s 
α: Type u_1

β: Type ?u.6039

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

b, a: α

s: Multiset α

fold op b (a ::ₘ s) = fold op (op b a) s
foldl_cons: ∀ {α : Type ?u.7129} {β : Type ?u.7130} (f : β → α → β) (H : RightCommutative f) (b : β) (a : α) (s : Multiset α),
  foldl f H b (a ::ₘ s) = foldl f H (f b a) s
foldl_cons,
α: Type u_1

β: Type ?u.6039

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

b, a: α

s: Multiset α

foldl op (_ : RightCommutative op) (op b a) s = fold op (op b a) s 
α: Type u_1

β: Type ?u.6039

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

b, a: α

s: Multiset α

fold op b (a ::ₘ s) = fold op (op b a) s← 
fold_eq_foldl: ∀ {α : Type ?u.7167} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (s : Multiset α),
  fold op b s = foldl op (_ : RightCommutative op) b s
fold_eq_foldl
α: Type u_1

β: Type ?u.6039

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

b, a: α

s: Multiset α

fold op (op b a) s = fold op (op b a) s]
Goals accomplished! 🐙
#align multiset.fold_cons'_right 
Multiset.fold_cons'_right: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b a : α) (s : Multiset α),
  fold op b (a ::ₘ s) = fold op (op b a) s
Multiset.fold_cons'_right

theorem 
fold_cons'_left: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b a : α) (s : Multiset α),
  fold op b (a ::ₘ s) = fold op (op a b) s
fold_cons'_left (
b: α
b 
a: α
a : 
α: Type ?u.7201
α) (
s: Multiset α
s : 
Multiset: Type ?u.7227 → Type ?u.7227
Multiset 
α: Type ?u.7201
α) : (
a: α
a ::ₘ 
s: Multiset α
s).
fold: {α : Type ?u.7234} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b: α
b = 
s: Multiset α
s.
fold: {α : Type ?u.7268} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op (
a: α
a * 
b: α
b) := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.7204

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

b, a: α

s: Multiset α

fold op b (a ::ₘ s) = fold op (op a b) srw [
α: Type u_1

β: Type ?u.7204

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

b, a: α

s: Multiset α

fold op b (a ::ₘ s) = fold op (op a b) s
fold_cons'_right: ∀ {α : Type ?u.8258} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b a : α) (s : Multiset α),
  fold op b (a ::ₘ s) = fold op (op b a) s
fold_cons'_right,
α: Type u_1

β: Type ?u.7204

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

b, a: α

s: Multiset α

fold op (op b a) s = fold op (op a b) s 
α: Type u_1

β: Type ?u.7204

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

b, a: α

s: Multiset α

fold op b (a ::ₘ s) = fold op (op a b) s
hc: IsCommutative α op
hc.
comm: ∀ {α : Type ?u.8299} {op : α → α → α} [self : IsCommutative α op] (a b : α), op a b = op b a
comm
α: Type u_1

β: Type ?u.7204

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

b, a: α

s: Multiset α

fold op (op a b) s = fold op (op a b) s]
Goals accomplished! 🐙
#align multiset.fold_cons'_left 
Multiset.fold_cons'_left: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b a : α) (s : Multiset α),
  fold op b (a ::ₘ s) = fold op (op a b) s
Multiset.fold_cons'_left

theorem 
fold_add: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b₁ b₂ : α) (s₁ s₂ : Multiset α),
  fold op (op b₁ b₂) (s₁ + s₂) = op (fold op b₁ s₁) (fold op b₂ s₂)
fold_add (
b₁: α
b₁ 
b₂: α
b₂ : 
α: Type ?u.8329
α) (
s₁: Multiset α
s₁ 
s₂: Multiset α
s₂ : 
Multiset: Type ?u.8358 → Type ?u.8358
Multiset 
α: Type ?u.8329
α) :
    (
s₁: Multiset α
s₁ + 
s₂: Multiset α
s₂).
fold: {α : Type ?u.8407} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op (
b₁: α
b₁ * 
b₂: α
b₂) = 
s₁: Multiset α
s₁.
fold: {α : Type ?u.9409} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b₁: α
b₁ * 
s₂: Multiset α
s₂.
fold: {α : Type ?u.9425} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b₂: α
b₂ :=
  
Multiset.induction_on: ∀ {α : Type ?u.9908} {p : Multiset α → Prop} (s : Multiset α),
  p 0 → (∀ ⦃a : α⦄ {s : Multiset α}, p s → p (a ::ₘ s)) → p s
Multiset.induction_on 
s₂: Multiset α
s₂ (by
Goals accomplished! 🐙 
α: Type u_1

β: Type ?u.8332

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)rw [
α: Type u_1

β: Type ?u.8332

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)
add_zero: ∀ {M : Type ?u.9953} [inst : AddZeroClass M] (a : M), a + 0 = a
add_zero,
α: Type u_1

β: Type ?u.8332

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

b₁, b₂: α

s₁, s₂: Multiset α

fold op (op b₁ b₂) s₁ = op (fold op b₁ s₁) (fold op b₂ 0) 
α: Type u_1

β: Type ?u.8332

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)
fold_zero: ∀ {α : Type ?u.10318} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α), fold op b 0 = b
fold_zero,
α: Type u_1

β: Type ?u.8332

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

b₁, b₂: α

s₁, s₂: Multiset α

fold op (op b₁ b₂) s₁ = op (fold op b₁ s₁) b₂ 
α: Type u_1

β: Type ?u.8332

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)← 
fold_cons'_right: ∀ {α : Type ?u.10355} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b a : α) (s : Multiset α),
  fold op b (a ::ₘ s) = fold op (op b a) s
fold_cons'_right,
α: Type u_1

β: Type ?u.8332

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

b₁, b₂: α

s₁, s₂: Multiset α

fold op b₁ (b₂ ::ₘ s₁) = op (fold op b₁ s₁) b₂ 
α: Type u_1

β: Type ?u.8332

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)← 
fold_cons_right: ∀ {α : Type ?u.10376} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b a : α) (s : Multiset α),
  fold op b (a ::ₘ s) = op (fold op b s) a
fold_cons_right 
op: α → α → α
op
α: Type u_1

β: Type ?u.8332

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

b₁, b₂: α

s₁, s₂: Multiset α

fold op b₁ (b₂ ::ₘ s₁) = fold op b₁ (b₂ ::ₘ s₁)]
Goals accomplished! 🐙)
    (fun 
a: ?m.9940
a 
b: ?m.9943
b 
h: ?m.9946
h => by
Goals accomplished! 🐙 
α: Type u_1

β: Type ?u.8332

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))rw [
α: Type u_1

β: Type ?u.8332

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))
fold_cons_left: ∀ {α : Type ?u.10399} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b a : α) (s : Multiset α),
  fold op b (a ::ₘ s) = op a (fold op b s)
fold_cons_left,
α: Type u_1

β: Type ?u.8332

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₁) (op a (fold op b₂ b)) 
α: Type u_1

β: Type ?u.8332

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))
add_cons: ∀ {α : Type ?u.10431} (a : α) (s t : Multiset α), s + a ::ₘ t = a ::ₘ (s + t)
add_cons,
α: Type u_1

β: Type ?u.8332

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₂) (a ::ₘ (s₁ + b)) = op (fold op b₁ s₁) (op a (fold op b₂ b)) 
α: Type u_1

β: Type ?u.8332

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))
fold_cons_left: ∀ {α : Type ?u.10444} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b a : α) (s : Multiset α),
  fold op b (a ::ₘ s) = op a (fold op b s)
fold_cons_left,
α: Type u_1

β: Type ?u.8332

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)

op a (fold op (op b₁ b₂) (s₁ + b)) = op (fold op b₁ s₁) (op a (fold op b₂ b)) 
α: Type u_1

β: Type ?u.8332

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))
h: fold op (op b₁ b₂) (s₁ + b) = op (fold op b₁ s₁) (fold op b₂ b)
h,
α: Type u_1

β: Type ?u.8332

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)

op a (op (fold op b₁ s₁) (fold op b₂ b)) = op (fold op b₁ s₁) (op a (fold op b₂ b)) 
α: Type u_1

β: Type ?u.8332

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))← 
ha: IsAssociative α op
ha.
assoc: ∀ {α : Type ?u.10466} {op : α → α → α} [self : IsAssociative α op] (a b c : α), op (op a b) c = op a (op b c)
assoc,
α: Type u_1

β: Type ?u.8332

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)

op (op a (fold op b₁ s₁)) (fold op b₂ b) = op (fold op b₁ s₁) (op a (fold op b₂ b)) 
α: Type u_1

β: Type ?u.8332

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))
hc: IsCommutative α op
hc.
comm: ∀ {α : Type ?u.10488} {op : α → α → α} [self : IsCommutative α op] (a b : α), op a b = op b a
comm 
a: α
a,
α: Type u_1

β: Type ?u.8332

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)

op (op (fold op b₁ s₁) a) (fold op b₂ b) = op (fold op b₁ s₁) (op a (fold op b₂ b))
      
α: Type u_1

β: Type ?u.8332

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))
ha: IsAssociative α op
ha.
assoc: ∀ {α : Type ?u.10498} {op : α → α → α} [self : IsAssociative α op] (a b c : α), op (op a b) c = op a (op b c)
assoc
α: Type u_1

β: Type ?u.8332

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)

op (fold op b₁ s₁) (op a (fold op b₂ b)) = op (fold op b₁ s₁) (op a (fold op b₂ b))]
Goals accomplished! 🐙)
#align multiset.fold_add 
Multiset.fold_add: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b₁ b₂ : α) (s₁ s₂ : Multiset α),
  fold op (op b₁ b₂) (s₁ + s₂) = op (fold op b₁ s₁) (fold op b₂ s₂)
Multiset.fold_add

theorem 
fold_bind: ∀ {α : Type u_2} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] {ι : Type u_1} (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)
fold_bind {
ι: Type u_1
ι : 
Type _: Type (?u.10564+1)
Type _} (
s: Multiset ι
s : 
Multiset: Type ?u.10567 → Type ?u.10567
Multiset 
ι: Type ?u.10564
ι) (
t: ι → Multiset α
t : 
ι: Type ?u.10564
ι → 
Multiset: Type ?u.10572 → Type ?u.10572
Multiset 
α: Type ?u.10542
α) (
b: ι → α
b : 
ι: Type ?u.10564
ι → 
α: Type ?u.10542
α) (
b₀: α
b₀ : 
α: Type ?u.10542
α) :
    (
s: Multiset ι
s.
bind: {α : Type ?u.10584} → {β : Type ?u.10583} → Multiset α → (α → Multiset β) → Multiset β
bind 
t: ι → Multiset α
t).
fold: {α : Type ?u.10598} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op ((
s: Multiset ι
s.
map: {α : Type ?u.10615} → {β : Type ?u.10614} → (α → β) → Multiset α → Multiset β
map 
b: ι → α
b).
fold: {α : Type ?u.10625} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b₀: α
b₀) =
    (
s: Multiset ι
s.
map: {α : Type ?u.10660} → {β : Type ?u.10659} → (α → β) → Multiset α → Multiset β
map fun 
i: ?m.10668
i => (
t: ι → Multiset α
t 
i: ?m.10668
i).
fold: {α : Type ?u.10670} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op (
b: ι → α
b 
i: ?m.10668
i)).
fold: {α : Type ?u.10689} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b₀: α
b₀ := by
Goals accomplished! 🐙
  
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

ι: Type u_1

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)induction' 
s: Multiset ι
s using 
Multiset.induction_on: ∀ {α : Type u_1} {p : Multiset α → Prop} (s : Multiset α), p 0 → (∀ ⦃a : α⦄ {s : Multiset α}, p s → p (a ::ₘ s)) → p s
Multiset.induction_on with 
a: ?m.10731
a 
ha: Multiset ?m.10731
ha 
ih: ?m.10732 ha
ih
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

ι: Type u_1

t: ι → Multiset α

b: ι → α

b₀: α

empty
fold op (fold op b₀ (map b 0)) (bind 0 t) = fold op b₀ (map (fun i => fold op (b i) (t i)) 0)
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha✝: IsAssociative α op

ι: Type u_1

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)

cons
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))
  
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

ι: Type u_1

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)·
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

ι: Type u_1

t: ι → Multiset α

b: ι → α

b₀: α

empty
fold op (fold op b₀ (map b 0)) (bind 0 t) = fold op b₀ (map (fun i => fold op (b i) (t i)) 0) 
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

ι: Type u_1

t: ι → Multiset α

b: ι → α

b₀: α

empty
fold op (fold op b₀ (map b 0)) (bind 0 t) = fold op b₀ (map (fun i => fold op (b i) (t i)) 0)
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha✝: IsAssociative α op

ι: Type u_1

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)

cons
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))rw [
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

ι: Type u_1

t: ι → Multiset α

b: ι → α

b₀: α

empty
fold op (fold op b₀ (map b 0)) (bind 0 t) = fold op b₀ (map (fun i => fold op (b i) (t i)) 0)
zero_bind: ∀ {α : Type ?u.10746} {β : Type ?u.10745} (f : α → Multiset β), bind 0 f = 0
zero_bind,
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

ι: Type u_1

t: ι → Multiset α

b: ι → α

b₀: α

empty
fold op (fold op b₀ (map b 0)) 0 = fold op b₀ (map (fun i => fold op (b i) (t i)) 0) 
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

ι: Type u_1

t: ι → Multiset α

b: ι → α

b₀: α

empty
fold op (fold op b₀ (map b 0)) (bind 0 t) = fold op b₀ (map (fun i => fold op (b i) (t i)) 0)
map_zero: ∀ {α : Type ?u.10770} {β : Type ?u.10769} (f : α → β), map f 0 = 0
map_zero,
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

ι: Type u_1

t: ι → Multiset α

b: ι → α

b₀: α

empty
fold op (fold op b₀ 0) 0 = fold op b₀ (map (fun i => fold op (b i) (t i)) 0) 
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

ι: Type u_1

t: ι → Multiset α

b: ι → α

b₀: α

empty
fold op (fold op b₀ (map b 0)) (bind 0 t) = fold op b₀ (map (fun i => fold op (b i) (t i)) 0)
map_zero: ∀ {α : Type ?u.10795} {β : Type ?u.10794} (f : α → β), map f 0 = 0
map_zero,
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

ι: Type u_1

t: ι → Multiset α

b: ι → α

b₀: α

empty
fold op (fold op b₀ 0) 0 = fold op b₀ 0 
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

ι: Type u_1

t: ι → Multiset α

b: ι → α

b₀: α

empty
fold op (fold op b₀ (map b 0)) (bind 0 t) = fold op b₀ (map (fun i => fold op (b i) (t i)) 0)
fold_zero: ∀ {α : Type ?u.10805} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α), fold op b 0 = b
fold_zero
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

ι: Type u_1

t: ι → Multiset α

b: ι → α

b₀: α

empty
fold op b₀ 0 = fold op b₀ 0]
Goals accomplished! 🐙
  
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

ι: Type u_1

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)·
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha✝: IsAssociative α op

ι: Type u_1

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)

cons
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)) 
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha✝: IsAssociative α op

ι: Type u_1

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)

cons
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))rw [
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha✝: IsAssociative α op

ι: Type u_1

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)

cons
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))
cons_bind: ∀ {α : Type ?u.10846} {β : Type ?u.10845} (a : α) (s : Multiset α) (f : α → Multiset β),
  bind (a ::ₘ s) f = f a + bind s f
cons_bind,
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha✝: IsAssociative α op

ι: Type u_1

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)

cons
fold op (fold op b₀ (map b (a ::ₘ ha))) (t a + bind ha t) = fold op b₀ (map (fun i => fold op (b i) (t i)) (a ::ₘ ha)) 
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha✝: IsAssociative α op

ι: Type u_1

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)

cons
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))
map_cons: ∀ {α : Type ?u.10865} {β : Type ?u.10866} (f : α → β) (a : α) (s : Multiset α), map f (a ::ₘ s) = f a ::ₘ map f s
map_cons,
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha✝: IsAssociative α op

ι: Type u_1

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)

cons
fold op (fold op b₀ (b a ::ₘ map b ha)) (t a + bind ha t) = fold op b₀ (map (fun i => fold op (b i) (t i)) (a ::ₘ ha)) 
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha✝: IsAssociative α op

ι: Type u_1

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)

cons
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))
map_cons: ∀ {α : Type ?u.10881} {β : Type ?u.10882} (f : α → β) (a : α) (s : Multiset α), map f (a ::ₘ s) = f a ::ₘ map f s
map_cons,
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha✝: IsAssociative α op

ι: Type u_1

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)

cons
fold op (fold op b₀ (b a ::ₘ map b ha)) (t a + bind ha t) =   fold op b₀ (fold op (b a) (t a) ::ₘ map (fun i => fold op (b i) (t i)) ha) 
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha✝: IsAssociative α op

ι: Type u_1

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)

cons
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))
fold_cons_left: ∀ {α : Type ?u.10897} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b a : α) (s : Multiset α),
  fold op b (a ::ₘ s) = op a (fold op b s)
fold_cons_left,
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha✝: IsAssociative α op

ι: Type u_1

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)

cons
fold op (op (b a) (fold op b₀ (map b ha))) (t a + bind ha t) =   fold op b₀ (fold op (b a) (t a) ::ₘ map (fun i => fold op (b i) (t i)) ha) 
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha✝: IsAssociative α op

ι: Type u_1

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)

cons
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))
fold_cons_left: ∀ {α : Type ?u.10928} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b a : α) (s : Multiset α),
  fold op b (a ::ₘ s) = op a (fold op b s)
fold_cons_left,
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha✝: IsAssociative α op

ι: Type u_1

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)

cons
fold op (op (b a) (fold op b₀ (map b ha))) (t a + bind ha t) =   op (fold op (b a) (t a)) (fold op b₀ (map (fun i => fold op (b i) (t i)) ha)) 
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha✝: IsAssociative α op

ι: Type u_1

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)

cons
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))
fold_add: ∀ {α : Type ?u.10952} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b₁ b₂ : α)
  (s₁ s₂ : Multiset α), fold op (op b₁ b₂) (s₁ + s₂) = op (fold op b₁ s₁) (fold op b₂ s₂)
fold_add,
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha✝: IsAssociative α op

ι: Type u_1

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)

cons
op (fold op (b a) (t a)) (fold op (fold op b₀ (map b ha)) (bind ha t)) =   op (fold op (b a) (t a)) (fold op b₀ (map (fun i => fold op (b i) (t i)) ha)) 
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha✝: IsAssociative α op

ι: Type u_1

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)

cons
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))
ih: ?m.10732 ha
ih
α: Type u_2

β: Type ?u.10545

op: α → α → α

hc: IsCommutative α op

ha✝: IsAssociative α op

ι: Type u_1

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)

cons
op (fold op (b a) (t a)) (fold op b₀ (map (fun i => fold op (b i) (t i)) ha)) =   op (fold op (b a) (t a)) (fold op b₀ (map (fun i => fold op (b i) (t i)) ha))]
Goals accomplished! 🐙
#align multiset.fold_bind 
Multiset.fold_bind: ∀ {α : Type u_2} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] {ι : Type u_1} (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)
Multiset.fold_bind

theorem 
fold_singleton: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b a : α), fold op b {a} = op a b
fold_singleton (
b: α
b 
a: α
a : 
α: Type ?u.11021
α) : ({
a: α
a} : 
Multiset: Type ?u.11049 → Type ?u.11049
Multiset 
α: Type ?u.11021
α).
fold: {α : Type ?u.11074} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b: α
b = 
a: α
a * 
b: α
b :=
  
foldr_singleton: ∀ {α : Type ?u.12079} {β : Type ?u.12080} (f : α → β → β) (H : LeftCommutative f) (b : β) (a : α),
  foldr f H b {a} = f a b
foldr_singleton 
_: ?m.12081 → ?m.12082 → ?m.12082
_ 
_: LeftCommutative ?m.12083
_ 
_: ?m.12082
_ 
_: ?m.12081
_
#align multiset.fold_singleton 
Multiset.fold_singleton: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b a : α), fold op b {a} = op a b
Multiset.fold_singleton

theorem 
fold_distrib: ∀ {α : Type u_2} {β : Type u_1} (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)) s) = op (fold op u₁ (map f s)) (fold op u₂ (map g s))
fold_distrib {
f: β → α
f 
g: β → α
g : 
β: Type ?u.12133
β → 
α: Type ?u.12130
α} (
u₁: α
u₁ 
u₂: α
u₂ : 
α: Type ?u.12130
α) (
s: Multiset β
s : 
Multiset: Type ?u.12164 → Type ?u.12164
Multiset 
β: Type ?u.12133
β) :
    (
s: Multiset β
s.
map: {α : Type ?u.12169} → {β : Type ?u.12168} → (α → β) → Multiset α → Multiset β
map fun 
x: ?m.12177
x => 
f: β → α
f 
x: ?m.12177
x * 
g: β → α
g 
x: ?m.12177
x).
fold: {α : Type ?u.13149} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op (
u₁: α
u₁ * 
u₂: α
u₂) = (
s: Multiset β
s.
map: {α : Type ?u.13614} → {β : Type ?u.13613} → (α → β) → Multiset α → Multiset β
map 
f: β → α
f).
fold: {α : Type ?u.13624} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
u₁: α
u₁ * (
s: Multiset β
s.
map: {α : Type ?u.13641} → {β : Type ?u.13640} → (α → β) → Multiset α → Multiset β
map 
g: β → α
g).
fold: {α : Type ?u.13651} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
u₂: α
u₂ :=
  
Multiset.induction_on: ∀ {α : Type ?u.14157} {p : Multiset α → Prop} (s : Multiset α),
  p 0 → (∀ ⦃a : α⦄ {s : Multiset α}, p s → p (a ::ₘ s)) → p s
Multiset.induction_on 
s: Multiset β
s (by
Goals accomplished! 🐙 
α: Type u_2

β: Type u_1

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))simp
Goals accomplished! 🐙) (fun 
a: ?m.14189
a 
b: ?m.14192
b 
h: ?m.14195
h => by
Goals accomplished! 🐙
    
α: Type u_2

β: Type u_1

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)))rw [
α: Type u_2

β: Type u_1

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)))
map_cons: ∀ {α : Type ?u.14638} {β : Type ?u.14639} (f : α → β) (a : α) (s : Multiset α), map f (a ::ₘ s) = f a ::ₘ map f s
map_cons,
α: Type u_2

β: Type u_1

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₂) (op (f a) (g a) ::ₘ map (fun x => op (f x) (g x)) b) =   op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b))) 
α: Type u_2

β: Type u_1

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)))
fold_cons_left: ∀ {α : Type ?u.14659} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b a : α) (s : Multiset α),
  fold op b (a ::ₘ s) = op a (fold op b s)
fold_cons_left,
α: Type u_2

β: Type u_1

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))

op (op (f a) (g a)) (fold op (op u₁ u₂) (map (fun x => op (f x) (g x)) b)) =   op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b))) 
α: Type u_2

β: Type u_1

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)))
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))
h,
α: Type u_2

β: Type u_1

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))

op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =   op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b))) 
α: Type u_2

β: Type u_1

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)))
map_cons: ∀ {α : Type ?u.14695} {β : Type ?u.14696} (f : α → β) (a : α) (s : Multiset α), map f (a ::ₘ s) = f a ::ₘ map f s
map_cons,
α: Type u_2

β: Type u_1

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))

op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =   op (fold op u₁ (f a ::ₘ map f b)) (fold op u₂ (map g (a ::ₘ b))) 
α: Type u_2

β: Type u_1

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)))
fold_cons_left: ∀ {α : Type ?u.14711} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b a : α) (s : Multiset α),
  fold op b (a ::ₘ s) = op a (fold op b s)
fold_cons_left,
α: Type u_2

β: Type u_1

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))

op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =   op (op (f a) (fold op u₁ (map f b))) (fold op u₂ (map g (a ::ₘ b))) 
α: Type u_2

β: Type u_1

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)))
map_cons: ∀ {α : Type ?u.14734} {β : Type ?u.14735} (f : α → β) (a : α) (s : Multiset α), map f (a ::ₘ s) = f a ::ₘ map f s
map_cons,
α: Type u_2

β: Type u_1

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))

op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =   op (op (f a) (fold op u₁ (map f b))) (fold op u₂ (g a ::ₘ map g b))
      
α: Type u_2

β: Type u_1

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)))
fold_cons_right: ∀ {α : Type ?u.14751} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b a : α) (s : Multiset α),
  fold op b (a ::ₘ s) = op (fold op b s) a
fold_cons_right,
α: Type u_2

β: Type u_1

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))

op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =   op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a)) 
α: Type u_2

β: Type u_1

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)))
ha: IsAssociative α op
ha.
assoc: ∀ {α : Type ?u.14776} {op : α → α → α} [self : IsAssociative α op] (a b c : α), op (op a b) c = op a (op b c)
assoc,
α: Type u_2

β: Type u_1

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))

op (f a) (op (g a) (op (fold op u₁ (map f b)) (fold op u₂ (map g b)))) =   op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a)) 
α: Type u_2

β: Type u_1

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)))← 
ha: IsAssociative α op
ha.
assoc: ∀ {α : Type ?u.14790} {op : α → α → α} [self : IsAssociative α op] (a b c : α), op (op a b) c = op a (op b c)
assoc (
g: β → α
g 
a: β
a),
α: Type u_2

β: Type u_1

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))

op (f a) (op (op (g a) (fold op u₁ (map f b))) (fold op u₂ (map g b))) =   op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a)) 
α: Type u_2

β: Type u_1

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)))
hc: IsCommutative α op
hc.
comm: ∀ {α : Type ?u.14802} {op : α → α → α} [self : IsCommutative α op] (a b : α), op a b = op b a
comm (
g: β → α
g 
a: β
a),
α: Type u_2

β: Type u_1

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))

op (f a) (op (op (fold op u₁ (map f b)) (g a)) (fold op u₂ (map g b))) =   op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
      
α: Type u_2

β: Type u_1

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)))
ha: IsAssociative α op
ha.
assoc: ∀ {α : Type ?u.14812} {op : α → α → α} [self : IsAssociative α op] (a b c : α), op (op a b) c = op a (op b c)
assoc,
α: Type u_2

β: Type u_1

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))

op (f a) (op (fold op u₁ (map f b)) (op (g a) (fold op u₂ (map g b)))) =   op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a)) 
α: Type u_2

β: Type u_1

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)))
hc: IsCommutative α op
hc.
comm: ∀ {α : Type ?u.14826} {op : α → α → α} [self : IsCommutative α op] (a b : α), op a b = op b a
comm (
g: β → α
g 
a: β
a),
α: Type u_2

β: Type u_1

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))

op (f a) (op (fold op u₁ (map f b)) (op (fold op u₂ (map g b)) (g a))) =   op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a)) 
α: Type u_2

β: Type u_1

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)))
ha: IsAssociative α op
ha.
assoc: ∀ {α : Type ?u.14836} {op : α → α → α} [self : IsAssociative α op] (a b c : α), op (op a b) c = op a (op b c)
assoc
α: Type u_2

β: Type u_1

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))

op (f a) (op (fold op u₁ (map f b)) (op (fold op u₂ (map g b)) (g a))) =   op (f a) (op (fold op u₁ (map f b)) (op (fold op u₂ (map g b)) (g a)))]
Goals accomplished! 🐙)
#align multiset.fold_distrib 
Multiset.fold_distrib: ∀ {α : Type u_2} {β : Type u_1} (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)) s) = op (fold op u₁ (map f s)) (fold op u₂ (map g s))
Multiset.fold_distrib

theorem 
fold_hom: ∀ {α : Type u_2} {β : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] {op' : β → β → β}
  [inst : IsCommutative β op'] [inst_1 : IsAssociative β op'] {m : α → β},
  (∀ (x y : α), m (op x y) = op' (m x) (m y)) → ∀ (b : α) (s : Multiset α), fold op' (m b) (map m s) = m (fold op b s)
fold_hom {
op': β → β → β
op' : 
β: Type ?u.14890
β → 
β: Type ?u.14890
β → 
β: Type ?u.14890
β} [
IsCommutative: (α : Type ?u.14915) → (α → α → α) → Prop
IsCommutative 
β: Type ?u.14890
β 
op': β → β → β
op'] [
IsAssociative: (α : Type ?u.14920) → (α → α → α) → Prop
IsAssociative 
β: Type ?u.14890
β 
op': β → β → β
op'] {
m: α → β
m : 
α: Type ?u.14887
α → 
β: Type ?u.14890
β}
    (
hm: ∀ (x y : α), m (op x y) = op' (m x) (m y)
hm : ∀ 
x: ?m.14930
x 
y: ?m.14933
y, 
m: α → β
m (
op: α → α → α
op 
x: ?m.14930
x 
y: ?m.14933
y) = 
op': β → β → β
op' (
m: α → β
m 
x: ?m.14930
x) (
m: α → β
m 
y: ?m.14933
y)) (
b: α
b : 
α: Type ?u.14887
α) (
s: Multiset α
s : 
Multiset: Type ?u.14942 → Type ?u.14942
Multiset 
α: Type ?u.14887
α) :
    (
s: Multiset α
s.
map: {α : Type ?u.14947} → {β : Type ?u.14946} → (α → β) → Multiset α → Multiset β
map 
m: α → β
m).
fold: {α : Type ?u.14958} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op': β → β → β
op' (
m: α → β
m 
b: α
b) = 
m: α → β
m (
s: Multiset α
s.
fold: {α : Type ?u.14993} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b: α
b) :=
  
Multiset.induction_on: ∀ {α : Type ?u.15036} {p : Multiset α → Prop} (s : Multiset α),
  p 0 → (∀ ⦃a : α⦄ {s : Multiset α}, p s → p (a ::ₘ s)) → p s
Multiset.induction_on 
s: Multiset α
s (by
Goals accomplished! 🐙 
α: Type u_2

β: Type u_1

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)simp
Goals accomplished! 🐙) (by
Goals accomplished! 🐙 
α: Type u_2

β: Type u_1

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))simp (config := { contextual := 
true: Bool
true }) [
hm: ∀ (x y : α), m (op x y) = op' (m x) (m y)
hm]
Goals accomplished! 🐙)
#align multiset.fold_hom 
Multiset.fold_hom: ∀ {α : Type u_2} {β : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] {op' : β → β → β}
  [inst : IsCommutative β op'] [inst_1 : IsAssociative β op'] {m : α → β},
  (∀ (x y : α), m (op x y) = op' (m x) (m y)) → ∀ (b : α) (s : Multiset α), fold op' (m b) (map m s) = m (fold op b s)
Multiset.fold_hom

theorem 
fold_union_inter: ∀ [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₂)
fold_union_inter [
DecidableEq: Sort ?u.17518 → Sort (max1?u.17518)
DecidableEq 
α: Type ?u.17496
α] (
s₁: Multiset α
s₁ 
s₂: Multiset α
s₂ : 
Multiset: Type ?u.17530 → Type ?u.17530
Multiset 
α: Type ?u.17496
α) (
b₁: α
b₁ 
b₂: α
b₂ : 
α: Type ?u.17496
α) :
    ((
s₁: Multiset α
s₁ ∪ 
s₂: Multiset α
s₂).
fold: {α : Type ?u.17577} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b₁: α
b₁ * (
s₁: Multiset α
s₁ ∩ 
s₂: Multiset α
s₂).
fold: {α : Type ?u.17640} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b₂: α
b₂) = 
s₁: Multiset α
s₁.
fold: {α : Type ?u.18661} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b₁: α
b₁ * 
s₂: Multiset α
s₂.
fold: {α : Type ?u.18677} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b₂: α
b₂ := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.17499

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₂)rw [
α: Type u_1

β: Type ?u.17499

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₂)← 
fold_add: ∀ {α : Type ?u.19165} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b₁ b₂ : α)
  (s₁ s₂ : Multiset α), fold op (op b₁ b₂) (s₁ + s₂) = op (fold op b₁ s₁) (fold op b₂ s₂)
fold_add 
op: α → α → α
op,
α: Type u_1

β: Type ?u.17499

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

inst✝: DecidableEq α

s₁, s₂: Multiset α

b₁, b₂: α

fold op (op b₁ b₂) (s₁ ∪ s₂ + s₁ ∩ s₂) = op (fold op b₁ s₁) (fold op b₂ s₂) 
α: Type u_1

β: Type ?u.17499

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₂)
union_add_inter: ∀ {α : Type ?u.19210} [inst : DecidableEq α] (s t : Multiset α), s ∪ t + s ∩ t = s + t
union_add_inter,
α: Type u_1

β: Type ?u.17499

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

inst✝: DecidableEq α

s₁, s₂: Multiset α

b₁, b₂: α

fold op (op b₁ b₂) (s₁ + s₂) = op (fold op b₁ s₁) (fold op b₂ s₂) 
α: Type u_1

β: Type ?u.17499

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₂)
fold_add: ∀ {α : Type ?u.19364} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b₁ b₂ : α)
  (s₁ s₂ : Multiset α), fold op (op b₁ b₂) (s₁ + s₂) = op (fold op b₁ s₁) (fold op b₂ s₂)
fold_add 
op: α → α → α
op
α: Type u_1

β: Type ?u.17499

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

inst✝: DecidableEq α

s₁, s₂: Multiset α

b₁, b₂: α

op (fold op b₁ s₁) (fold op b₂ s₂) = op (fold op b₁ s₁) (fold op b₂ s₂)]
Goals accomplished! 🐙
#align multiset.fold_union_inter 
Multiset.fold_union_inter: ∀ {α : Type u_1} (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₂)
Multiset.fold_union_inter

@[simp]
theorem 
fold_dedup_idem: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] [inst : DecidableEq α]
  [hi : IsIdempotent α op] (s : Multiset α) (b : α), fold op b (dedup s) = fold op b s
fold_dedup_idem [
DecidableEq: Sort ?u.19430 → Sort (max1?u.19430)
DecidableEq 
α: Type ?u.19408
α] [
hi: IsIdempotent α op
hi : 
IsIdempotent: (α : Type ?u.19439) → (α → α → α) → Prop
IsIdempotent 
α: Type ?u.19408
α 
op: α → α → α
op] (
s: Multiset α
s : 
Multiset: Type ?u.19444 → Type ?u.19444
Multiset 
α: Type ?u.19408
α) (
b: α
b : 
α: Type ?u.19408
α) :
    (
dedup: {α : Type ?u.19450} → [inst : DecidableEq α] → Multiset α → Multiset α
dedup 
s: Multiset α
s).
fold: {α : Type ?u.19493} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b: α
b = 
s: Multiset α
s.
fold: {α : Type ?u.19527} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b: α
b :=
  
Multiset.induction_on: ∀ {α : Type ?u.19551} {p : Multiset α → Prop} (s : Multiset α),
  p 0 → (∀ ⦃a : α⦄ {s : Multiset α}, p s → p (a ::ₘ s)) → p s
Multiset.induction_on 
s: Multiset α
s (by
Goals accomplished! 🐙 
α: Type u_1

β: Type ?u.19411

op: α → α → α

hc: IsCommutative α op

ha: IsAssociative α op

inst✝: DecidableEq α

hi: IsIdempotent α op

s: Multiset α

b: α

fold op b (dedup 0) = fold op b 0simp
Goals accomplished! 🐙) fun 
a: ?m.19583
a 
s: ?m.19586
s 
IH: ?m.19589
IH => by
Goals accomplished! 🐙
    
α: Type u_1

β: Type ?u.19411

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: ?m.19856
h : 
a: α
a ∈ 
s: Multiset α
s
α: Type u_1

β: Type ?u.19411

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

pos
fold op b (dedup (a ::ₘ s)) = fold op b (a ::ₘ s)
α: Type u_1

β: Type ?u.19411

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

neg
fold op b (dedup (a ::ₘ s)) = fold op b (a ::ₘ s) 
α: Type u_1

β: Type ?u.19411

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)<;>
α: Type u_1

β: Type ?u.19411

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

pos
fold op b (dedup (a ::ₘ s)) = fold op b (a ::ₘ s)
α: Type u_1

β: Type ?u.19411

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

neg
fold op b (dedup (a ::ₘ s)) = fold op b (a ::ₘ s) 
α: Type u_1

β: Type ?u.19411

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)simp [
IH: fold op b (dedup s) = fold op b s
IH, 
h: ?m.19849
h]
Goals accomplished! 🐙
    
α: Type u_1

β: Type ?u.19411

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)show 
fold: {α : Type ?u.20295} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b: α
b 
s: Multiset α
s = 
op: α → α → α
op 
a: α
a (
fold: {α : Type ?u.20305} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
op: α → α → α
op 
b: α
b 
s: Multiset α
s)
α: Type u_1

β: Type ?u.19411

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

pos
fold op b s = op a (fold op b s)
    
α: Type u_1

β: Type ?u.19411

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)rw [
α: Type u_1

β: Type ?u.19411

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

pos
fold op b s = op a (fold op b s)← 
cons_erase: ∀ {α : Type ?u.20324} [inst : DecidableEq α] {s : Multiset α} {a : α}, a ∈ s → a ::ₘ erase s a = s
cons_erase 
h: ?m.19849
h,
α: Type u_1

β: Type ?u.19411

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

pos
fold op b (a ::ₘ erase s a) = op a (fold op b (a ::ₘ erase s a)) 
α: Type u_1

β: Type ?u.19411

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

pos
fold op b s = op a (fold op b s)
fold_cons_left: ∀ {α : Type ?u.20340} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b a : α) (s : Multiset α),
  fold op b (a ::ₘ s) = op a (fold op b s)
fold_cons_left,
α: Type u_1

β: Type ?u.19411

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

pos
op a (fold op b (erase s a)) = op a (op a (fold op b (erase s a))) 
α: Type u_1

β: Type ?u.19411

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

pos
fold op b s = op a (fold op b s)← 
ha: IsAssociative α op
ha.
assoc: ∀ {α : Type ?u.20361} {op : α → α → α} [self : IsAssociative α op] (a b c : α), op (op a b) c = op a (op b c)
assoc,
α: Type u_1

β: Type ?u.19411

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

pos
op a (fold op b (erase s a)) = op (op a a) (fold op b (erase s a)) 
α: Type u_1

β: Type ?u.19411

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

pos
fold op b s = op a (fold op b s)
hi: IsIdempotent α op
hi.
idempotent: ∀ {α : Type ?u.20377} {op : α → α → α} [self : IsIdempotent α op] (a : α), op a a = a
idempotent
α: Type u_1

β: Type ?u.19411

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

pos
op a (fold op b (erase s a)) = op a (fold op b (erase s a))]
Goals accomplished! 🐙
#align multiset.fold_dedup_idem 
Multiset.fold_dedup_idem: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] [inst : DecidableEq α]
  [hi : IsIdempotent α op] (s : Multiset α) (b : α), fold op b (dedup s) = fold op b s
Multiset.fold_dedup_idem

end Fold

section Order

theorem 
max_le_of_forall_le: ∀ {α : Type u_1} [inst : CanonicallyLinearOrderedAddMonoid α] (l : Multiset α) (n : α),
  (∀ (x : α), x ∈ l → x ≤ n) → fold max ⊥ l ≤ n
max_le_of_forall_le {
α: Type ?u.20502
α : 
Type _: Type (?u.20502+1)
Type _} [
CanonicallyLinearOrderedAddMonoid: Type ?u.20505 → Type ?u.20505
CanonicallyLinearOrderedAddMonoid 
α: Type ?u.20502
α] (
l: Multiset α
l : 
Multiset: Type ?u.20508 → Type ?u.20508
Multiset 
α: Type ?u.20502
α)
    (
n: α
n : 
α: Type ?u.20502
α) (
h: ∀ (x : α), x ∈ l → x ≤ n
h : ∀ 
x: ?m.20514
x ∈ 
l: Multiset α
l, 
x: ?m.20514
x ≤ 
n: α
n) : 
l: Multiset α
l.
fold: {α : Type ?u.20758} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
max: {α : Type ?u.20766} → [self : Max α] → α → α → α
max 
⊥: ?m.20801
⊥ ≤ 
n: α
n := by
Goals accomplished! 🐙
  
α✝: Type ?u.20496

β: Type ?u.20499

α: Type u_1

inst✝: CanonicallyLinearOrderedAddMonoid α

l: Multiset α

n: α

h: ∀ (x : α), x ∈ l → x ≤ n

fold max ⊥ l ≤ ninduction 
l: Multiset α
l using 
Quotient.inductionOn: ∀ {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop} (q : Quotient s),
  (∀ (a : α), motive (Quotient.mk s a)) → motive q
Quotient.inductionOn
α✝: Type ?u.20496

β: Type ?u.20499

α: Type u_1

inst✝: CanonicallyLinearOrderedAddMonoid α

n: α

a✝: List α

h: ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) a✝ → x ≤ n

h
fold max ⊥ (Quotient.mk (List.isSetoid α) a✝) ≤ n
  
α✝: Type ?u.20496

β: Type ?u.20499

α: Type u_1

inst✝: CanonicallyLinearOrderedAddMonoid α

l: Multiset α

n: α

h: ∀ (x : α), x ∈ l → x ≤ n

fold max ⊥ l ≤ nsimpa using 
List.max_le_of_forall_le: ∀ {α : Type ?u.21635} [inst : LinearOrder α] [inst_1 : OrderBot α] (l : List α) (a : α),
  (∀ (x : α), x ∈ l → x ≤ a) → List.foldr max ⊥ l ≤ a
List.max_le_of_forall_le 
_: List ?m.21636
_ 
_: ?m.21636
_ 
h: ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) a✝ → x ≤ n
h
Goals accomplished! 🐙
#align multiset.max_le_of_forall_le 
Multiset.max_le_of_forall_le: ∀ {α : Type u_1} [inst : CanonicallyLinearOrderedAddMonoid α] (l : Multiset α) (n : α),
  (∀ (x : α), x ∈ l → x ≤ n) → fold max ⊥ l ≤ n
Multiset.max_le_of_forall_le

theorem 
max_nat_le_of_forall_le: ∀ (l : Multiset ℕ) (n : ℕ), (∀ (x : ℕ), x ∈ l → x ≤ n) → fold max 0 l ≤ n
max_nat_le_of_forall_le (
l: Multiset ℕ
l : 
Multiset: Type ?u.22102 → Type ?u.22102
Multiset 
ℕ: Type
ℕ) (
n: ℕ
n : 
ℕ: Type
ℕ) (
h: ∀ (x : ℕ), x ∈ l → x ≤ n
h : ∀ 
x: ?m.22108
x ∈ 
l: Multiset ℕ
l, 
x: ?m.22108
x ≤ 
n: ℕ
n) : 
l: Multiset ℕ
l.
fold: {α : Type ?u.22152} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
max: {α : Type ?u.22160} → [self : Max α] → α → α → α
max 
0: ?m.22195
0 ≤ 
n: ℕ
n :=
  
max_le_of_forall_le: ∀ {α : Type ?u.22271} [inst : CanonicallyLinearOrderedAddMonoid α] (l : Multiset α) (n : α),
  (∀ (x : α), x ∈ l → x ≤ n) → fold max ⊥ l ≤ n
max_le_of_forall_le 
l: Multiset ℕ
l 
n: ℕ
n 
h: ∀ (x : ℕ), x ∈ l → x ≤ n
h
#align multiset.max_nat_le_of_forall_le 
Multiset.max_nat_le_of_forall_le: ∀ (l : Multiset ℕ) (n : ℕ), (∀ (x : ℕ), x ∈ l → x ≤ n) → fold max 0 l ≤ n
Multiset.max_nat_le_of_forall_le

end Order

open Nat

theorem 
le_smul_dedup: ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), ∃ n, s ≤ n • dedup s
le_smul_dedup [
DecidableEq: Sort ?u.22307 → Sort (max1?u.22307)
DecidableEq 
α: Type ?u.22301
α] (
s: Multiset α
s : 
Multiset: Type ?u.22316 → Type ?u.22316
Multiset 
α: Type ?u.22301
α) : ∃ 
n: ℕ
n : 
ℕ: Type
ℕ, 
s: Multiset α
s ≤ 
n: ℕ
n • 
dedup: {α : Type ?u.22332} → [inst : DecidableEq α] → Multiset α → Multiset α
dedup 
s: Multiset α
s :=
  ⟨(
s: Multiset α
s.
map: {α : Type ?u.22812} → {β : Type ?u.22811} → (α → β) → Multiset α → Multiset β
map fun 
a: ?m.22820
a => 
count: {α : Type ?u.22822} → [inst : DecidableEq α] → α → Multiset α → ℕ
count 
a: ?m.22820
a 
s: Multiset α
s).
fold: {α : Type ?u.22899} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → α
fold 
max: {α : Type ?u.22907} → [self : Max α] → α → α → α
max 
0: ?m.22943
0,
    
le_iff_count: ∀ {α : Type ?u.22988} [inst : DecidableEq α] {s t : Multiset α}, s ≤ t ↔ ∀ (a : α), count a s ≤ count a t
le_iff_count.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 fun 
a: ?m.23056
a => by
Goals accomplished! 🐙
      
α: Type u_1

β: Type ?u.22304

inst✝: DecidableEq α

s: Multiset α

a: α

count a s ≤ count a (fold max 0 (map (fun a => count a s) s) • dedup s)rw [
α: Type u_1

β: Type ?u.22304

inst✝: DecidableEq α

s: Multiset α

a: α

count a s ≤ count a (fold max 0 (map (fun a => count a s) s) • dedup s)
count_nsmul: ∀ {α : Type ?u.23080} [inst : DecidableEq α] (a : α) (n : ℕ) (s : Multiset α), count a (n • s) = n * count a s
count_nsmul
α: Type u_1

β: Type ?u.22304

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.22304

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.22304

inst✝: DecidableEq α

s: Multiset α