Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
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 α ophc : IsCommutative: (α : Type ?u.3279) → (α → α → α) → PropIsCommutative α: Type ?u.152α op: α → α → αop] [ha: IsAssociative α opha : IsAssociative: (α : Type ?u.3284) → (α → α → α) → PropIsAssociative α: Type ?u.152α op: α → α → αop]

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

/-- `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.2327Multiset α: 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 fleft_comm _: ?m.2346 → ?m.2346 → ?m.2346_ hc: IsCommutative α ophc.comm: ∀ {α : Type ?u.2358} {op : α → α → α} [self : IsCommutative α op] (a b : α), op a b = op b acomm ha: IsAssociative α opha.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 sfold_eq_foldr (b: αb : α: Type ?u.2489α) (s: Multiset αs : Multiset: Type ?u.2513 → Type ?u.2513Multiset α: 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 fleft_comm _: ?m.2557 → ?m.2557 → ?m.2557_ hc: IsCommutative α ophc.comm: ∀ {α : Type ?u.2569} {op : α → α → α} [self : IsCommutative α op] (a b : α), op a b = op b acomm ha: IsAssociative α opha.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 = arfl
#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 sMultiset.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 lcoe_fold_r (b: αb : α: Type ?u.2618α) (l: List αl : List: Type ?u.2642 → Type ?u.2642List α: 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 = arfl
#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 lMultiset.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 lcoe_fold_l (b: αb : α: Type ?u.2858α) (l: List αl : List: Type ?u.2882 → Type ?u.2882List α: 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 lcoe_foldr_swap op: α → α → αop _: LeftCommutative op_ b: αb l: List αl).trans: ∀ {α : Sort ?u.3052} {a b c : α}, a = b → b = c → a = ctrans <| byGoals accomplished! 🐙 α: Type u_1β: Type ?u.2861op: α → α → αhc: IsCommutative α opha: IsAssociative α opb: αl: List αList.foldl (fun x y => op y x) b l = List.foldl op b lsimp [hc: IsCommutative α ophc.comm: ∀ {α : Type ?u.3098} {op : α → α → α} [self : IsCommutative α op] (a b : α), op a b = op b acomm]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 lMultiset.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 sfold_eq_foldl (b: αb : α: Type ?u.3267α) (s: Multiset αs : Multiset: Type ?u.3291 → Type ?u.3291Multiset α: 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 fright_comm _: ?m.3335 → ?m.3335 → ?m.3335_ hc: IsCommutative α ophc.comm: ∀ {α : Type ?u.3347} {op : α → α → α} [self : IsCommutative α op] (a b : α), op a b = op b acomm ha: IsAssociative α opha.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 qQuot.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 lcoe_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 sMultiset.fold_eq_foldl

@[simp]
theorem fold_zero: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α), fold op b 0 = bfold_zero (b: αb : α: Type ?u.3514α) : (0: ?m.35420 : Multiset: Type ?u.3540 → Type ?u.3540Multiset α: 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 = arfl
#align multiset.fold_zero Multiset.fold_zero: ∀ {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α), fold op b 0 = bMultiset.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.3680Multiset α: 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) afold_cons_right (b: αb a: αa : α: Type ?u.4793α) (s: Multiset αs : Multiset: Type ?u.4819 → Type ?u.4819Multiset α: 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 := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.4796op: α → α → αhc: IsCommutative α opha: IsAssociative α opb, a: αs: Multiset αfold op b (a ::ₘ s) = op (fold op b s) asimp [hc: IsCommutative α ophc.comm: ∀ {α : Type ?u.5867} {op : α → α → α} [self : IsCommutative α op] (a b : α), op a b = op b acomm]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) aMultiset.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) sfold_cons'_right (b: αb a: αa : α: Type ?u.6036α) (s: Multiset αs : Multiset: Type ?u.6062 → Type ?u.6062Multiset α: 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) := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.6039op: α → α → αhc: IsCommutative α opha: IsAssociative α opb, a: αs: Multiset αfold op b (a ::ₘ s) = fold op (op b a) srw [α: Type u_1β: Type ?u.6039op: α → α → αhc: IsCommutative α opha: IsAssociative α opb, a: αs: Multiset αfold op b (a ::ₘ s) = fold op (op b a) sfold_eq_foldl: ∀ {α : Type ?u.7093} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (s : Multiset α),
fold op b s = foldl op (_ : RightCommutative op) b sfold_eq_foldl,α: Type u_1β: Type ?u.6039op: α → α → αhc: IsCommutative α opha: IsAssociative α opb, a: αs: Multiset αfoldl op (_ : RightCommutative op) b (a ::ₘ s) = fold op (op b a) s α: Type u_1β: Type ?u.6039op: α → α → αhc: IsCommutative α opha: IsAssociative α opb, a: αs: Multiset αfold op b (a ::ₘ s) = fold op (op b a) sfoldl_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) sfoldl_cons,α: Type u_1β: Type ?u.6039op: α → α → αhc: IsCommutative α opha: IsAssociative α opb, a: αs: Multiset αfoldl op (_ : RightCommutative op) (op b a) s = fold op (op b a) s α: Type u_1β: Type ?u.6039op: α → α → αhc: IsCommutative α opha: IsAssociative α opb, 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 sfold_eq_foldlα: Type u_1β: Type ?u.6039op: α → α → αhc: IsCommutative α opha: IsAssociative α opb, 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) sMultiset.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) sfold_cons'_left (b: αb a: αa : α: Type ?u.7201α) (s: Multiset αs : Multiset: Type ?u.7227 → Type ?u.7227Multiset α: 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) := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.7204op: α → α → αhc: IsCommutative α opha: IsAssociative α opb, a: αs: Multiset αfold op b (a ::ₘ s) = fold op (op a b) srw [α: Type u_1β: Type ?u.7204op: α → α → αhc: IsCommutative α opha: IsAssociative α opb, a: αs: Multiset αfold op b (a ::ₘ s) = fold op (op a b) sfold_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) sfold_cons'_right,α: Type u_1β: Type ?u.7204op: α → α → αhc: IsCommutative α opha: IsAssociative α opb, a: αs: Multiset αfold op (op b a) s = fold op (op a b) s α: Type u_1β: Type ?u.7204op: α → α → αhc: IsCommutative α opha: IsAssociative α opb, a: αs: Multiset αfold op b (a ::ₘ s) = fold op (op a b) shc: IsCommutative α ophc.comm: ∀ {α : Type ?u.8299} {op : α → α → α} [self : IsCommutative α op] (a b : α), op a b = op b acommα: Type u_1β: Type ?u.7204op: α → α → αhc: IsCommutative α opha: IsAssociative α opb, 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) sMultiset.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.8358Multiset α: 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 sMultiset.induction_on s₂: Multiset αs₂ (byGoals accomplished! 🐙 α: Type u_1β: Type ?u.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, 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.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, 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 = aadd_zero,α: Type u_1β: Type ?u.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, b₂: αs₁, s₂: Multiset αfold op (op b₁ b₂) s₁ = op (fold op b₁ s₁) (fold op b₂ 0) α: Type u_1β: Type ?u.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, 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 = bfold_zero,α: Type u_1β: Type ?u.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, b₂: αs₁, s₂: Multiset αfold op (op b₁ b₂) s₁ = op (fold op b₁ s₁) b₂ α: Type u_1β: Type ?u.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, 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) sfold_cons'_right,α: Type u_1β: Type ?u.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, b₂: αs₁, s₂: Multiset αfold op b₁ (b₂ ::ₘ s₁) = op (fold op b₁ s₁) b₂ α: Type u_1β: Type ?u.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, 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) afold_cons_right op: α → α → αopα: Type u_1β: Type ?u.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, b₂: αs₁, s₂: Multiset αfold op b₁ (b₂ ::ₘ s₁) = fold op b₁ (b₂ ::ₘ s₁)]Goals accomplished! 🐙)
(fun a: ?m.9940a b: ?m.9943b h: ?m.9946h => byGoals accomplished! 🐙 α: Type u_1β: Type ?u.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, 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.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, 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.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, 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.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, 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.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, 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.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, 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.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, 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.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, 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.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, 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.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, 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 α opha.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.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, 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.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, 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 α ophc.comm: ∀ {α : Type ?u.10488} {op : α → α → α} [self : IsCommutative α op] (a b : α), op a b = op b acomm a: αa,α: Type u_1β: Type ?u.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, 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.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, 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 α opha.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.8332op: α → α → αhc: IsCommutative α opha: IsAssociative α opb₁, 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.10567Multiset ι: Type ?u.10564ι) (t: ι → Multiset αt : ι: Type ?u.10564ι → Multiset: Type ?u.10572 → Type ?u.10572Multiset α: 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.10668i => (t: ι → Multiset αt i: ?m.10668i).fold: {α : Type ?u.10670} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → αfold op: α → α → αop (b: ι → αb i: ?m.10668i)).fold: {α : Type ?u.10689} → (op : α → α → α) → [hc : IsCommutative α op] → [ha : IsAssociative α op] → α → Multiset α → αfold op: α → α → αop b₀: αb₀ := byGoals accomplished! 🐙
α: Type u_2β: Type ?u.10545op: α → α → αhc: IsCommutative α opha: IsAssociative α opι: Type u_1s: 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 sMultiset.induction_on with a: ?m.10731a ha: Multiset ?m.10731ha ih: ?m.10732 haihα: Type u_2β: Type ?u.10545op: α → α → αhc: IsCommutative α opha: IsAssociative α opι: Type u_1t: ι → Multiset αb: ι → αb₀: αemptyfold 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.10545op: α → α → αhc: IsCommutative α opha✝: IsAssociative α opι: Type u_1t: ι → 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)consfold 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.10545op: α → α → αhc: IsCommutative α opha: IsAssociative α opι: Type u_1s: 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.10545op: α → α → αhc: IsCommutative α opha: IsAssociative α opι: Type u_1t: ι → Multiset αb: ι → αb₀: αemptyfold 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.10545op: α → α → αhc: IsCommutative α opha: IsAssociative α opι: Type u_1t: ι → Multiset αb: ι → αb₀: αemptyfold 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.10545op: α → α → αhc: IsCommutative α opha✝: IsAssociative α opι: Type u_1t: ι → 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)consfold 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.10545op: α → α → αhc: IsCommutative α opha: IsAssociative α opι: Type u_1t: ι → Multiset αb: ι → αb₀: αemptyfold 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 = 0zero_bind,α: Type u_2β: Type ?u.10545op: α → α → αhc: IsCommutative α opha: IsAssociative α opι: Type u_1t: ι → Multiset αb: ι → αb₀: αemptyfold 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.10545op: α → α → αhc: IsCommutative α opha: IsAssociative α opι: Type u_1t: ι → Multiset αb: ι → αb₀: αemptyfold 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 = 0map_zero,α: Type u_2β: Type ?u.10545op: α → α → αhc: IsCommutative α opha: IsAssociative α opι: Type u_1t: ι → Multiset αb: ι → αb₀: αemptyfold op (fold op b₀ 0) 0 = fold op b₀ (map (fun i => fold op (b i) (t i)) 0) α: Type u_2β: Type ?u.10545op: α → α → αhc: IsCommutative α opha: IsAssociative α opι: Type u_1t: ι → Multiset αb: ι → αb₀: αemptyfold 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 = 0map_zero,α: Type u_2β: Type ?u.10545op: α → α → αhc: IsCommutative α opha: IsAssociative α opι: Type u_1t: ι → Multiset αb: ι → αb₀: αemptyfold op (fold op b₀ 0) 0 = fold op b₀ 0 α: Type u_2β: Type ?u.10545op: α → α → αhc: IsCommutative α opha: IsAssociative α opι: Type u_1t: ι → Multiset αb: ι → αb₀: αemptyfold 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 = bfold_zeroα: Type u_2β: Type ?u.10545op: α → α → αhc: IsCommutative α opha: IsAssociative α opι: Type u_1t: ι → Multiset αb: ι → αb₀: αemptyfold op b₀ 0 = fold op b₀ 0]Goals accomplished! 🐙
α: Type u_2β: Type ?u.10545op: α → α → αhc: IsCommutative α opha: IsAssociative α opι: Type u_1s: 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.10545op: α → α → αhc: IsCommutative α opha✝: IsAssociative α opι: Type u_1t: ι → 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)consfold 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.10545op: α → α → αhc: IsCommutative α opha✝: IsAssociative α opι: Type u_1t: ι → 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)consfold 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.10545op: α → α → αhc: IsCommutative α opha✝: IsAssociative α opι: Type u_1t: ι → 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)consfold 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 fcons_bind,α: Type u_2β: Type ?u.10545op: α → α → αhc: IsCommutative α opha✝: IsAssociative α opι: Type u_1t: ι → 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)consfold 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.10545op: α → α → αhc: IsCommutative α opha✝: IsAssociative α opι: Type u_1t: ι → 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)consfold 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 smap_cons,α: Type u_2β: Type ?u.10545op: α → α → αhc: IsCommutative α opha✝: IsAssociative α opι: Type u_1t: ι → 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)consfold 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.10545op: α → α → αhc: IsCommutative α opha✝: IsAssociative α opι: Type u_1t: ι → 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)consfold 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 smap_cons,α: Type u_2β: Type ?u.10545op: α → α → αhc: IsCommutative α opha✝: IsAssociative α opι: Type u_1t: ι → 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)consfold 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.10545op: α → α → αhc: IsCommutative α opha✝: IsAssociative α opι: Type u_1t: ι → 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)consfold 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.10545op: α → α → αhc: IsCommutative α opha✝: IsAssociative α opι: Type u_1t: ι → 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)consfold 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.10545op: α → α → αhc: IsCommutative α opha✝: IsAssociative α opι: Type u_1t: ι → 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)consfold 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.10545op: α → α → αhc: IsCommutative α opha✝: IsAssociative α opι: Type u_1t: ι → 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)consfold 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.10545op: α → α → αhc: IsCommutative α opha✝: IsAssociative α opι: Type u_1t: ι → 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)consfold 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.10545op: α → α → αhc: IsCommutative α opha✝: IsAssociative α opι: Type u_1t: ι → 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)consop (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.10545op: α → α → αhc: IsCommutative α opha✝: IsAssociative α opι: Type u_1t: ι → 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)consfold 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 haihα: Type u_2β: Type ?u.10545op: α → α → αhc: IsCommutative α opha✝: IsAssociative α opι: Type u_1t: ι → 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)consop (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 bfold_singleton (b: αb a: αa : α: Type ?u.11021α) : ({a: αa} : Multiset: Type ?u.11049 → Type ?u.11049Multiset α: 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 bfoldr_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 bMultiset.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.12164Multiset β: Type ?u.12133β) :
(s: Multiset βs.map: {α : Type ?u.12169} → {β : Type ?u.12168} → (α → β) → Multiset α → Multiset βmap fun x: ?m.12177x => f: β → αf x: ?m.12177x * g: β → αg x: ?m.12177x).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 sMultiset.induction_on s: Multiset βs (byGoals accomplished! 🐙 α: Type u_2β: Type u_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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))simpGoals accomplished! 🐙) (fun a: ?m.14189a b: ?m.14192b h: ?m.14195h => byGoals accomplished! 🐙
α: Type u_2β: Type u_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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 smap_cons,α: Type u_2β: Type u_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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 smap_cons,α: Type u_2β: Type u_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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 smap_cons,α: Type u_2β: Type u_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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) afold_cons_right,α: Type u_2β: Type u_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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 α opha.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_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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 α opha.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_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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 α ophc.comm: ∀ {α : Type ?u.14802} {op : α → α → α} [self : IsCommutative α op] (a b : α), op a b = op b acomm (g: β → αg a: βa),α: Type u_2β: Type u_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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 α opha.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_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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 α ophc.comm: ∀ {α : Type ?u.14826} {op : α → α → α} [self : IsCommutative α op] (a b : α), op a b = op b acomm (g: β → αg a: βa),α: Type u_2β: Type u_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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 α opha.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_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opf, 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) → (α → α → α) → PropIsCommutative β: Type ?u.14890β op': β → β → βop'] [IsAssociative: (α : Type ?u.14920) → (α → α → α) → PropIsAssociative β: 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.14930x y: ?m.14933y, m: α → βm (op: α → α → αop x: ?m.14930x y: ?m.14933y) = op': β → β → βop' (m: α → βm x: ?m.14930x) (m: α → βm y: ?m.14933y)) (b: αb : α: Type ?u.14887α) (s: Multiset αs : Multiset: Type ?u.14942 → Type ?u.14942Multiset α: 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 sMultiset.induction_on s: Multiset αs (byGoals accomplished! 🐙 α: Type u_2β: Type u_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opop': β → β → β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)simpGoals accomplished! 🐙) (byGoals accomplished! 🐙 α: Type u_2β: Type u_1op: α → α → αhc: IsCommutative α opha: IsAssociative α opop': β → β → β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: Booltrue }) [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.17530Multiset α: 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₂ := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.17499op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: 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.17499op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: 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.17499op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: 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.17499op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: 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 + tunion_add_inter,α: Type u_1β: Type ?u.17499op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: 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.17499op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: 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.17499op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: 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 sfold_dedup_idem [DecidableEq: Sort ?u.19430 → Sort (max1?u.19430)DecidableEq α: Type ?u.19408α] [hi: IsIdempotent α ophi : IsIdempotent: (α : Type ?u.19439) → (α → α → α) → PropIsIdempotent α: Type ?u.19408α op: α → α → αop] (s: Multiset αs : Multiset: Type ?u.19444 → Type ?u.19444Multiset α: 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 sMultiset.induction_on s: Multiset αs (byGoals accomplished! 🐙 α: Type u_1β: Type ?u.19411op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: DecidableEq αhi: IsIdempotent α ops: Multiset αb: αfold op b (dedup 0) = fold op b 0simpGoals accomplished! 🐙) fun a: ?m.19583a s: ?m.19586s IH: ?m.19589IH => byGoals accomplished! 🐙
α: Type u_1β: Type ?u.19411op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: DecidableEq αhi: IsIdempotent α ops✝: Multiset αb, a: αs: Multiset αIH: fold op b (dedup s) = fold op b sfold op b (dedup (a ::ₘ s)) = fold op b (a ::ₘ s)by_cases h: ?m.19856h : a: αa ∈ s: Multiset αsα: Type u_1β: Type ?u.19411op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: DecidableEq αhi: IsIdempotent α ops✝: Multiset αb, a: αs: Multiset αIH: fold op b (dedup s) = fold op b sh: a ∈ sposfold op b (dedup (a ::ₘ s)) = fold op b (a ::ₘ s)α: Type u_1β: Type ?u.19411op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: DecidableEq αhi: IsIdempotent α ops✝: Multiset αb, a: αs: Multiset αIH: fold op b (dedup s) = fold op b sh: ¬a ∈ snegfold op b (dedup (a ::ₘ s)) = fold op b (a ::ₘ s) α: Type u_1β: Type ?u.19411op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: DecidableEq αhi: IsIdempotent α ops✝: Multiset αb, a: αs: Multiset αIH: fold op b (dedup s) = fold op b sfold op b (dedup (a ::ₘ s)) = fold op b (a ::ₘ s)<;>α: Type u_1β: Type ?u.19411op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: DecidableEq αhi: IsIdempotent α ops✝: Multiset αb, a: αs: Multiset αIH: fold op b (dedup s) = fold op b sh: a ∈ sposfold op b (dedup (a ::ₘ s)) = fold op b (a ::ₘ s)α: Type u_1β: Type ?u.19411op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: DecidableEq αhi: IsIdempotent α ops✝: Multiset αb, a: αs: Multiset αIH: fold op b (dedup s) = fold op b sh: ¬a ∈ snegfold op b (dedup (a ::ₘ s)) = fold op b (a ::ₘ s) α: Type u_1β: Type ?u.19411op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: DecidableEq αhi: IsIdempotent α ops✝: Multiset αb, a: αs: Multiset αIH: fold op b (dedup s) = fold op b sfold op b (dedup (a ::ₘ s)) = fold op b (a ::ₘ s)simp [IH: fold op b (dedup s) = fold op b sIH, h: ?m.19849h]Goals accomplished! 🐙
α: Type u_1β: Type ?u.19411op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: DecidableEq αhi: IsIdempotent α ops✝: Multiset αb, a: αs: Multiset αIH: fold op b (dedup s) = fold op b sfold 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.19411op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: DecidableEq αhi: IsIdempotent α ops✝: Multiset αb, a: αs: Multiset αIH: fold op b (dedup s) = fold op b sh: a ∈ sposfold op b s = op a (fold op b s)
α: Type u_1β: Type ?u.19411op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: DecidableEq αhi: IsIdempotent α ops✝: Multiset αb, a: αs: Multiset αIH: fold op b (dedup s) = fold op b sfold op b (dedup (a ::ₘ s)) = fold op b (a ::ₘ s)rw [α: Type u_1β: Type ?u.19411op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: DecidableEq αhi: IsIdempotent α ops✝: Multiset αb, a: αs: Multiset αIH: fold op b (dedup s) = fold op b sh: a ∈ sposfold 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 = scons_erase h: ?m.19849h,α: Type u_1β: Type ?u.19411op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: DecidableEq αhi: IsIdempotent α ops✝: Multiset αb, a: αs: Multiset αIH: fold op b (dedup s) = fold op b sh: a ∈ sposfold op b (a ::ₘ erase s a) = op a (fold op b (a ::ₘ erase s a)) α: Type u_1β: Type ?u.19411op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: DecidableEq αhi: IsIdempotent α ops✝: Multiset αb, a: αs: Multiset αIH: fold op b (dedup s) = fold op b sh: a ∈ sposfold 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.19411op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: DecidableEq αhi: IsIdempotent α ops✝: Multiset αb, a: αs: Multiset αIH: fold op b (dedup s) = fold op b sh: a ∈ sposop a (fold op b (erase s a)) = op a (op a (fold op b (erase s a))) α: Type u_1β: Type ?u.19411op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: DecidableEq αhi: IsIdempotent α ops✝: Multiset αb, a: αs: Multiset αIH: fold op b (dedup s) = fold op b sh: a ∈ sposfold op b s = op a (fold op b s)← ha: IsAssociative α opha.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.19411op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: DecidableEq αhi: IsIdempotent α ops✝: Multiset αb, a: αs: Multiset αIH: fold op b (dedup s) = fold op b sh: a ∈ sposop a (fold op b (erase s a)) = op (op a a) (fold op b (erase s a)) α: Type u_1β: Type ?u.19411op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: DecidableEq αhi: IsIdempotent α ops✝: Multiset αb, a: αs: Multiset αIH: fold op b (dedup s) = fold op b sh: a ∈ sposfold op b s = op a (fold op b s)hi: IsIdempotent α ophi.idempotent: ∀ {α : Type ?u.20377} {op : α → α → α} [self : IsIdempotent α op] (a : α), op a a = aidempotentα: Type u_1β: Type ?u.19411op: α → α → αhc: IsCommutative α opha: IsAssociative α opinst✝: DecidableEq αhi: IsIdempotent α ops✝: Multiset αb, a: αs: Multiset αIH: fold op b (dedup s) = fold op b sh: a ∈ sposop 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 sMultiset.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 ≤ nmax_le_of_forall_le {α: Type ?u.20502α : Type _: Type (?u.20502+1)Type _} [CanonicallyLinearOrderedAddMonoid: Type ?u.20505 → Type ?u.20505CanonicallyLinearOrderedAddMonoid α: Type ?u.20502α] (l: Multiset αl : Multiset: Type ?u.20508 → Type ?u.20508Multiset α: Type ?u.20502α)
(n: αn : α: Type ?u.20502α) (h: ∀ (x : α), x ∈ l → x ≤ nh : ∀ x: ?m.20514x ∈ l: Multiset αl, x: ?m.20514x ≤ 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 := byGoals accomplished! 🐙
α✝: Type ?u.20496β: Type ?u.20499α: Type u_1inst✝: CanonicallyLinearOrderedAddMonoid αl: Multiset αn: αh: ∀ (x : α), x ∈ l → x ≤ nfold 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 qQuotient.inductionOnα✝: Type ?u.20496β: Type ?u.20499α: Type u_1inst✝: CanonicallyLinearOrderedAddMonoid αn: αa✝: List αh: ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) a✝ → x ≤ nhfold max ⊥ (Quotient.mk (List.isSetoid α) a✝) ≤ n
α✝: Type ?u.20496β: Type ?u.20499α: Type u_1inst✝: CanonicallyLinearOrderedAddMonoid αl: Multiset αn: αh: ∀ (x : α), x ∈ l → x ≤ nfold 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 ≤ aList.max_le_of_forall_le _: List ?m.21636_ _: ?m.21636_ h: ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) a✝ → x ≤ nhGoals 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 ≤ nMultiset.max_le_of_forall_le

theorem max_nat_le_of_forall_le: ∀ (l : Multiset ℕ) (n : ℕ), (∀ (x : ℕ), x ∈ l → x ≤ n) → fold max 0 l ≤ nmax_nat_le_of_forall_le (l: Multiset ℕl : Multiset: Type ?u.22102 → Type ?u.22102Multiset ℕ: Typeℕ) (n: ℕn : ℕ: Typeℕ) (h: ∀ (x : ℕ), x ∈ l → x ≤ nh : ∀ x: ?m.22108x ∈ l: Multiset ℕl, x: ?m.22108x ≤ 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.221950 ≤ n: ℕn :=
max_le_of_forall_le: ∀ {α : Type ?u.22271} [inst : CanonicallyLinearOrderedAddMonoid α] (l : Multiset α) (n : α),
(∀ (x : α), x ∈ l → x ≤ n) → fold max ⊥ l ≤ nmax_le_of_forall_le l: Multiset ℕl n: ℕn h: ∀ (x : ℕ), x ∈ l → x ≤ nh
#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 ≤ nMultiset.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 sle_smul_dedup [DecidableEq: Sort ?u.22307 → Sort (max1?u.22307)DecidableEq α: Type ?u.22301α] (s: Multiset αs : Multiset: Type ?u.22316 → Type ?u.22316Multiset α: 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.22820a => count: {α : Type ?u.22822} → [inst : DecidableEq α] → α → Multiset α → ℕcount a: ?m.22820a 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.229430,
le_iff_count: ∀ {α : Type ?u.22988} [inst : DecidableEq α] {s t : Multiset α}, s ≤ t ↔ ∀ (a : α), count a s ≤ count a tle_iff_count.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 fun a: ?m.23056a => byGoals accomplished! 🐙
α: Type u_1β: Type ?u.22304inst✝: 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.22304inst✝: 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 scount_nsmulα: Type u_1β: Type ?u.22304inst✝: 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.22304inst✝: 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.22304inst✝: DecidableEq αs: Multiset α```