awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst : DecidablePred p
a : ∀ (a : α), a ∈ m → bind (if p a then {a} else 0) f = if p a then f a else 0
⊢ Eq.{v + 1} (α := Multiset β) (m.bind fun (a : α) ↦ bind (if p a then {a} else 0) f)
    (m.bind fun (a : α) ↦ if p a then f a else 0)

Tactic:
apply Multiset.bind_congr

Premises used: Multiset.bind_congr
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst : DecidablePred p
a : α
ham : a ∈ m
pos : p a → bind {a} f = f a
neg : ¬p a → bind 0 f = 0
⊢ bind (if p a then {a} else 0) f = if p a then f a else 0

Tactic:
split_ifs
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst : DecidablePred p
a : α
ham : a ∈ m
h : p a
⊢ bind {a} f = f a

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst : DecidablePred p
a : α
ham : a ∈ m
h : ¬p a
⊢ bind 0 f = 0

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
m : Multiset α
f : α → Multiset β
p : β → Prop
inst : DecidablePred p
⊢ filter p (m.bind f) = m.bind fun (a : α) ↦ filter p (f a)

Tactic:
simp [bind, filter_join]

Premises used: Multiset.filter_join, Multiset.bind
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
f : α → Option β
⊢ filterMap f 0 = bind 0 fun (a : α) ↦ Option.getD (Option.map singleton (f a)) 0

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
f : α → Option β
a : α
m : Multiset α
ih : filterMap f m = m.bind fun (a : α) ↦ Option.getD (Option.map singleton (f a)) 0
⊢ filterMap f (a ::ₘ m) = (a ::ₘ m).bind fun (a : α) ↦ Option.getD (Option.map singleton (f a)) 0

Tactic:
simp [filterMap_cons, ih]

Premises used: Multiset.filterMap_cons
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
m : Multiset α
f : α → Option β
empty : filterMap f 0 = bind 0 fun (a : α) ↦ Option.getD (Option.map singleton (f a)) 0
cons :
  ∀ (a : α) (m : Multiset α) (ih : filterMap f m = m.bind fun (a : α) ↦ Option.getD (Option.map singleton (f a)) 0),
    filterMap f (a ::ₘ m) = (a ::ₘ m).bind fun (a : α) ↦ Option.getD (Option.map singleton (f a)) 0
⊢ filterMap f m = m.bind fun (a : α) ↦ Option.getD (Option.map singleton (f a)) 0

Tactic:
induction m using Multiset.induction with
  | empty => simp
  | cons a m ih => simp [filterMap_cons, ih]

Premises used: Multiset.cons, Multiset.filterMap_cons
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
simp :
  Eq.{u_2 + 1} (α := Multiset γ) (m.bind fun (a : α) ↦ bind (Option.getD (Option.map singleton (f a)) 0) g)
    (m.bind fun (a : α) ↦ (Option.map g (f a)).getD 0)
⊢ (filterMap f m).bind g = m.bind fun (a : α) ↦ (Option.map g (f a)).getD 0

Tactic:
simp only [filterMap_eq_bind, Multiset.bind_assoc]

Premises used: Multiset.filterMap_eq_bind, Multiset.bind_assoc
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
a : ∀ (a : α), a ∈ m → bind (Option.getD (Option.map singleton (f a)) 0) g = (Option.map g (f a)).getD 0
⊢ Eq.{u_2 + 1} (α := Multiset γ) (m.bind fun (a : α) ↦ bind (Option.getD (Option.map singleton (f a)) 0) g)
    (m.bind fun (a : α) ↦ (Option.map g (f a)).getD 0)

Tactic:
apply Multiset.bind_congr

Premises used: Multiset.bind_congr
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
a : α
ham : a ∈ m
⊢ bind (Option.getD (Option.map singleton none) 0) g = (Option.map g none).getD 0

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
a : α
ham : a ∈ m
b : β
⊢ bind (Option.getD (Option.map singleton (some b)) 0) g = (Option.map g (some b)).getD 0

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
a : α
ham : a ∈ m
a₁ : ∀ (x : Option β), bind (Option.getD (Option.map singleton x) 0) g = (Option.map g x).getD 0
⊢ bind (Option.getD (Option.map singleton (f a)) 0) g = (Option.map g (f a)).getD 0

Tactic:
cases f a with
  | none => simp
  | some b => simp

Premises used: Option.some, Option.none
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Multiset β
g : β → Option γ
⊢ filterMap g (m.bind f) = m.bind fun (a : α) ↦ filterMap g (f a)

Tactic:
simp [bind, filterMap_join]

Premises used: Multiset.bind, Multiset.filterMap_join
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
inst : CommMonoid β
s : Multiset α
t : α → Multiset β
⊢ (s.bind t).prod = prod (map (fun (a : α) ↦ (t a).prod) s)

Tactic:
simp [bind]

Premises used: Multiset.bind
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
γ : Type u_2
δ : Type u_3
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
h₁ : Rel (Rel p) (map f s) (map g t)
⊢ Rel p (s.bind f) (t.bind g)

Tactic:
apply rel_join

Premises used: Multiset.rel_join
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
γ : Type u_2
δ : Type u_3
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
h₁ : Rel (fun (a : α) (b : β) ↦ Rel p (f a) (g b)) s t
⊢ Rel (Rel p) (map f s) (map g t)

Tactic:
rw [rel_map]

Premises used: Multiset.rel_map
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
γ : Type u_2
δ : Type u_3
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel (fun (a : α) (b : β) ↦ Rel p (f a) (g b)) s t

Tactic:
hst.mono fun a _ b _ hr => h hr

Premises used: Multiset.Rel.mono
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
γ : Type u_2
δ : Type u_3
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel (fun (a : α) (b : β) ↦ Rel p (f a) (g b)) s t

Tactic:
exact hst.mono fun a _ b _ hr => h hr

Premises used: Multiset.Rel.mono
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
m : Multiset β
f : β → Multiset α
a : α
⊢ count a (map f 0).sum = sum (map (fun (b : β) ↦ count a (f b)) 0)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
m : Multiset β
f : β → Multiset α
a : α
⊢ ∀ (a_1 : β) (s : Multiset β),
    count a (map f s).sum = sum (map (fun (b : β) ↦ count a (f b)) s) →
      count a (map f (a_1 ::ₘ s)).sum = sum (map (fun (b : β) ↦ count a (f b)) (a_1 ::ₘ s))

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
m : Multiset β
f : β → Multiset α
a : α
⊢ count a (m.bind f) = sum (map (fun (b : β) ↦ count a (f b)) m)

Tactic:
count_sum

Premises used: Multiset.count_sum, Multiset.join, Multiset.bind
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
⊢ f x ≤ S.bind f

Tactic:
le_iff_count.2 fun a ↦ ?_

Premises used: Iff.mpr, Multiset.le_iff_count
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
refine : ∀ (a : β), count a (f x) ≤ count a (S.bind f)
⊢ f x ≤ S.bind f

Tactic:
refine le_iff_count.2 fun a ↦ ?_

Premises used: Iff.mpr, Multiset.le_iff_count
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
obtain :
  ∀ (m' : Multiset ℕ) (hm' : map (fun (b : α) ↦ count a (f b)) S = (fun (b : α) ↦ count a (f b)) x ::ₘ m'),
    count a (f x) ≤ count a (S.bind f)
⊢ count a (f x) ≤ count a (S.bind f)

Tactic:
obtain ⟨m', hm'⟩ := exists_cons_of_mem <| mem_map_of_mem (fun b ↦ count a (f b)) hx

Premises used: Multiset.exists_cons_of_mem, Multiset.count, Multiset.mem_map_of_mem
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
m' : Multiset ℕ
hm' : map (fun (b : α) ↦ count a (f b)) S = (fun (b : α) ↦ count a (f b)) x ::ₘ m'
rw : count a (f x) ≤ (fun (b : α) ↦ count a (f b)) x + m'.sum
⊢ count a (f x) ≤ count a (S.bind f)

Tactic:
rw [count_bind, hm', sum_cons]

Premises used: Multiset.count_bind, Multiset.sum_cons
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
m' : Multiset ℕ
hm' : map (fun (b : α) ↦ count a (f b)) S = (fun (b : α) ↦ count a (f b)) x ::ₘ m'
⊢ count a (f x) ≤ (fun (b : α) ↦ count a (f b)) x + m'.sum

Tactic:
Nat.le_add_right _ _

Premises used: Nat.le_add_right
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
m' : Multiset ℕ
hm' : map (fun (b : α) ↦ count a (f b)) S = (fun (b : α) ↦ count a (f b)) x ::ₘ m'
⊢ count a (f x) ≤ (fun (b : α) ↦ count a (f b)) x + m'.sum

Tactic:
exact Nat.le_add_right _ _

Premises used: Nat.le_add_right
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
refine : ∀ (a : β), count a (f x) ≤ count a (S.bind f)
refine₁ :
  ∀ (a : β) (m' : Multiset ℕ) (hm' : map (fun (b : α) ↦ count a (f b)) S = (fun (b : α) ↦ count a (f b)) x ::ₘ m'),
    count a (f x) ≤ count a (S.bind f)
refine₂ :
  ∀ (a : β) (m' : Multiset ℕ) (hm' : map (fun (b : α) ↦ count a (f b)) S = (fun (b : α) ↦ count a (f b)) x ::ₘ m'),
    count a (f x) ≤ (fun (b : α) ↦ count a (f b)) x + m'.sum
⊢ f x ≤ S.bind f

Tactic:
classical
  refine le_iff_count.2 fun a ↦ ?_
  obtain ⟨m', hm'⟩ := exists_cons_of_mem <| mem_map_of_mem (fun b ↦ count a (f b)) hx
  rw [count_bind, hm', sum_cons]
  exact Nat.le_add_right _ _

Premises used: Iff.mpr, Multiset.le_iff_count, Nat.le_add_right, Multiset.exists_cons_of_mem, Multiset.count_bind, Multiset.sum_cons
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
⊢ (s.attach.bind fun (i : { x : α // x ∈ s }) ↦ f (↑i : α)) = s.bind f

Tactic:
congr_arg join <| attach_map_val' _ _

Premises used: Multiset.attach_map_val', congr_arg, Multiset.join, Multiset.bind
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
⊢ ∀ (a : α), ∃ (l : List β), f a = (↑l : Multiset β)

Tactic:
have : ∀ a, ∃ l : List β, f a = l := fun a => Quot.induction_on (f a) fun l => ⟨l, rfl⟩
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
this : ∀ (a : α), ∃ (l : List β), f a = (↑l : Multiset β)
choose :
  ∀ (f' : (a : α) → List β) (h' : ∀ (a : α), f a = (↑(f' a) : Multiset β)),
    (s.bind f).Nodup ↔ (∀ (a : α), a ∈ s → (f a).Nodup) ∧ Pairwise (Disjoint on f) s
⊢ (s.bind f).Nodup ↔ (∀ (a : α), a ∈ s → (f a).Nodup) ∧ Pairwise (Disjoint on f) s

Tactic:
choose f' h' using this
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : (a : α) → List β
h' : ∀ (a : α), f a = (↑(f' a) : Multiset β)
⊢ f = fun (a : α) ↦ (↑(f' a) : Multiset β)

Tactic:
have : f = fun a ↦ ofList (f' a) := funext h'
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : (a : α) → List β
h' : ∀ (a : α), f a = (↑(f' a) : Multiset β)
this : f = fun (a : α) ↦ (↑(f' a) : Multiset β)
⊢ Symmetric fun (a b : α) ↦ (f' a).Disjoint (f' b)

Tactic:
have hd : Symmetric fun a b ↦ List.Disjoint (f' a) (f' b) := fun a b h ↦ h.symm
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : (a : α) → List β
h' : ∀ (a : α), f a = (↑(f' a) : Multiset β)
this : f = fun (a : α) ↦ (↑(f' a) : Multiset β)
hd : Symmetric fun (a b : α) ↦ (f' a).Disjoint (f' b)
⊢ ∀ (a : List α),
    (bind (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) a) f).Nodup ↔
      (∀ (a_1 : α),
          Membership.mem (γ := Multiset α) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) a) a_1 →
            (f a_1).Nodup) ∧
        Pairwise (fun (x y : α) ↦ Disjoint (f x) (f y)) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) a)

Tactic:
simp [this, List.nodup_flatMap, pairwise_coe_iff_pairwise hd]

Premises used: List.nodup_flatMap, Multiset.pairwise_coe_iff_pairwise
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : (a : α) → List β
h' : ∀ (a : α), f a = (↑(f' a) : Multiset β)
this : f = fun (a : α) ↦ (↑(f' a) : Multiset β)
hd : Symmetric fun (a b : α) ↦ (f' a).Disjoint (f' b)
⊢ (s.bind f).Nodup ↔ (∀ (a : α), a ∈ s → (f a).Nodup) ∧ Pairwise (Disjoint on f) s

Tactic:
exact Quot.induction_on s <| by
    unfold Function.onFun
    simp [this, List.nodup_flatMap, pairwise_coe_iff_pairwise hd]
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
s : Multiset α
f : α → Multiset β
a : ∀ (x : β), count x (s.dedup.bind f).dedup = count x (s.bind f).dedup
⊢ (s.dedup.bind f).dedup = (s.bind f).dedup

Tactic:
ext x
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
s : Multiset α
f : α → Multiset β
x : β
a : Eq (α := ℕ) (if x ∈ s.dedup.bind f then 1 else 0) (if x ∈ s.bind f then 1 else 0)
⊢ count x (s.dedup.bind f).dedup = count x (s.bind f).dedup

Tactic:
simp_rw [count_dedup]

Premises used: Multiset.count_dedup
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
s : Multiset α
f : α → Multiset β
x : β
a : (x ∈ s.dedup.bind f) = (x ∈ s.bind f)
⊢ Eq (α := ℕ) (if x ∈ s.dedup.bind f then 1 else 0) (if x ∈ s.bind f then 1 else 0)

Tactic:
congr 1
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
s : Multiset α
f : α → Multiset β
x : β
⊢ (x ∈ s.dedup.bind f) = (x ∈ s.bind f)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
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)
empty₁ : fold op (fold op b₀ 0) 0 = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) 0)
empty₂ : fold op (fold op b₀ 0) 0 = fold op b₀ 0
empty₃ empty₄ : fold op b₀ 0 = fold op b₀ 0
⊢ fold op (fold op b₀ (map b 0)) (bind 0 t) = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) 0)

Tactic:
rw [zero_bind, map_zero, map_zero, fold_zero]

Premises used: Multiset.map_zero, Multiset.fold_zero, Multiset.zero_bind
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha_1 : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (ha.bind 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 + ha.bind t) =
    fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))
cons₁ :
  fold op (fold op b₀ (b a ::ₘ map b ha)) (t a + ha.bind t) =
    fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))
cons₂ :
  fold op (fold op b₀ (b a ::ₘ map b ha)) (t a + ha.bind t) =
    fold op b₀ (fold op (b a) (t a) ::ₘ map (fun (i : ι) ↦ fold op (b i) (t i)) ha)
cons₃ :
  fold op (op (b a) (fold op b₀ (map b ha))) (t a + ha.bind t) =
    fold op b₀ (fold op (b a) (t a) ::ₘ map (fun (i : ι) ↦ fold op (b i) (t i)) ha)
cons₄ :
  fold op (op (b a) (fold op b₀ (map b ha))) (t a + ha.bind t) =
    op (fold op (b a) (t a)) (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)) (ha.bind t)) =
    op (fold op (b a) (t a)) (fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) ha))
cons₆ 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))
⊢ fold op (fold op b₀ (map b (a ::ₘ ha))) ((a ::ₘ ha).bind t) =
    fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha))

Tactic:
rw [cons_bind, map_cons, map_cons, fold_cons_left, fold_cons_left, fold_add, ih]

Premises used: Multiset.fold_cons_left, Multiset.fold_add, Multiset.map_cons, Multiset.cons_bind
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
s : Multiset ι
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)
cons :
  ∀ (a : ι) (ha_1 : Multiset ι)
    (ih : fold op (fold op b₀ (map b ha_1)) (ha_1.bind t) = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) ha_1)),
    fold op (fold op b₀ (map b (a ::ₘ ha_1))) ((a ::ₘ ha_1).bind t) =
      fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) (a ::ₘ ha_1))
⊢ fold op (fold op b₀ (map b s)) (s.bind t) = fold op b₀ (map (fun (i : ι) ↦ fold op (b i) (t i)) s)

Tactic:
induction s using Multiset.induction_on with
  | empty => rw [zero_bind, map_zero, map_zero, fold_zero]
  | cons a ha ih => rw [cons_bind, map_cons, map_cons, fold_cons_left, fold_cons_left, fold_add, ih]

Premises used: Multiset.fold_cons_left, Multiset.fold_add, Multiset.map_cons, Multiset.map_zero, Multiset.cons, Multiset.fold_zero, Multiset.zero_bind, Multiset.cons_bind
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
l₁ : List α
l₂ : List β
rw :
  Eq (α := Multiset (α × β)) ((↑l₁ : Multiset α).bind fun (a : α) ↦ map (Prod.mk a) (↑l₂ : Multiset β))
    ((↑l₁ : Multiset α).bind fun (a : α) ↦ (↑(List.map (Prod.mk a) l₂) : Multiset (α × β)))
⊢ (↑l₁ : Multiset α).product (↑l₂ : Multiset β) = (↑(l₁.product l₂) : Multiset (α × β))

Tactic:
rw [product, List.product, ← coe_bind]

Premises used: List.product, Multiset.coe_bind, Multiset.product
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
l₁ : List α
l₂ : List β
⊢ Eq (α := Multiset (α × β)) ((↑l₁ : Multiset α).bind fun (a : α) ↦ map (Prod.mk a) (↑l₂ : Multiset β))
    ((↑l₁ : Multiset α).bind fun (a : α) ↦ (↑(List.map (Prod.mk a) l₂) : Multiset (α × β)))

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
t : Multiset β
⊢ SProd.sprod (α := Multiset α) 0 t = 0

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Multiset.join, Multiset.product, List.foldr, Multiset.bind, rfl
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
a : α
s : Multiset α
t : Multiset β
⊢ (a ::ₘ s) ×ˢ t = map (Prod.mk a) t + s ×ˢ t

Tactic:
simp [SProd.sprod, product]

Premises used: SProd.sprod, Multiset.product
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s : Multiset α
⊢ SProd.sprod (β := Multiset β) s 0 = 0

Tactic:
simp [SProd.sprod, product]

Premises used: SProd.sprod, Multiset.product
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
b : β
s : Multiset α
t : Multiset β
⊢ s ×ˢ (b ::ₘ t) = map (fun (a : α) ↦ (a, b)) s + s ×ˢ t

Tactic:
simp [SProd.sprod, product]

Premises used: SProd.sprod, Multiset.product
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
a : α
b : β
⊢ SProd.sprod (α := Multiset α) (β := Multiset β) {a} {b} = {(a, b)}

Tactic:
simp only [SProd.sprod, product, bind_singleton, map_singleton]

Premises used: Multiset.map_singleton, SProd.sprod, Multiset.bind_singleton, Multiset.product
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s t : Multiset α
u : Multiset β
⊢ (s + t) ×ˢ u = s ×ˢ u + t ×ˢ u

Tactic:
simp [SProd.sprod, product]

Premises used: SProd.sprod, Multiset.product
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s_1 : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
t u : Multiset β
rw : map (Prod.mk a) (t + u) + (s ×ˢ t + s ×ˢ u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u
⊢ (a ::ₘ s) ×ˢ (t + u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u

Tactic:
rw [cons_product, IH]

Premises used: Multiset.cons_product
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s_1 : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
t u : Multiset β
⊢ map (Prod.mk a) (t + u) + (s ×ˢ t + s ×ˢ u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u

Tactic:
simp [add_left_comm, add_assoc]

Premises used: add_left_comm, add_assoc
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s : Multiset α
t : Multiset β
⊢ (s ×ˢ t).card = s.card * t.card

Tactic:
simp [SProd.sprod, product]

Premises used: SProd.sprod, Multiset.product
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s : Multiset α
t : Multiset β
a : α
b : β
⊢ (a, b) ∈ s ×ˢ t ↔ (a, b).1 ∈ s ∧ (a, b).2 ∈ t

Tactic:
simp [SProd.sprod, product, and_left_comm]

Premises used: SProd.sprod, and_left_comm, Multiset.product
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s : Multiset α
t : Multiset β
l₁ : List α
l₂ : List β
d₁ : Nodup ⟦l₁⟧
d₂ : Nodup ⟦l₂⟧
⊢ (⟦l₁⟧ ×ˢ ⟦l₂⟧).Nodup

Tactic:
simp [List.Nodup.product d₁ d₂]

Premises used: List.Nodup.product
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
s : Multiset α
t : Multiset β
empty : map Prod.swap (SProd.sprod (α := Multiset α) 0 t) = SProd.sprod (β := Multiset α) t 0
cons : ∀ (a : α) (s : Multiset α), map Prod.swap (s ×ˢ t) = t ×ˢ s → map Prod.swap ((a ::ₘ s) ×ˢ t) = t ×ˢ (a ::ₘ s)
⊢ map Prod.swap (s ×ˢ t) = t ×ˢ s

Tactic:
induction s using Multiset.induction
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
t : Multiset β
⊢ map Prod.swap (SProd.sprod (α := Multiset α) 0 t) = SProd.sprod (β := Multiset α) t 0

Tactic:
simp_all
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
t : Multiset β
a : α
s : Multiset α
h : map Prod.swap (s ×ˢ t) = t ×ˢ s
⊢ map Prod.swap ((a ::ₘ s) ×ˢ t) = t ×ˢ (a ::ₘ s)

Tactic:
simp_all
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
M : Type u_4
inst : CommMonoid M
s : Multiset α
t : Multiset β
f : α × β → M
empty :
  (map f (SProd.sprod (α := Multiset α) 0 t)).prod = prod (map (fun (i : α) ↦ prod (map (fun (j : β) ↦ f (i, j)) t)) 0)
cons :
  ∀ (a : α) (s : Multiset α),
    (map f (s ×ˢ t)).prod = prod (map (fun (i : α) ↦ prod (map (fun (j : β) ↦ f (i, j)) t)) s) →
      (map f ((a ::ₘ s) ×ˢ t)).prod = prod (map (fun (i : α) ↦ prod (map (fun (j : β) ↦ f (i, j)) t)) (a ::ₘ s))
⊢ (map f (s ×ˢ t)).prod = prod (map (fun (i : α) ↦ prod (map (fun (j : β) ↦ f (i, j)) t)) s)

Tactic:
induction s using Multiset.induction
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
M : Type u_4
inst : CommMonoid M
t : Multiset β
f : α × β → M
⊢ (map f (SProd.sprod (α := Multiset α) 0 t)).prod = prod (map (fun (i : α) ↦ prod (map (fun (j : β) ↦ f (i, j)) t)) 0)

Tactic:
simp_all
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
M : Type u_4
inst : CommMonoid M
t : Multiset β
f : α × β → M
a : α
s : Multiset α
h : (map f (s ×ˢ t)).prod = prod (map (fun (i : α) ↦ prod (map (fun (j : β) ↦ f (i, j)) t)) s)
⊢ (map f ((a ::ₘ s) ×ˢ t)).prod = prod (map (fun (i : α) ↦ prod (map (fun (j : β) ↦ f (i, j)) t)) (a ::ₘ s))

Tactic:
simp_all
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
σ : α → Type u_4
l₁ : List α
l₂ : (a : α) → List (σ a)
rw :
  Eq (α := Multiset ((a : α) × σ a))
    ((↑l₁ : Multiset α).bind fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (↑(l₂ a) : Multiset (σ a)))
    ((↑l₁ : Multiset α).bind fun (a : α) ↦
      (↑(List.map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) : Multiset ((a : α) × σ a)))
⊢ ((↑l₁ : Multiset α).sigma (σ := σ) fun (a : α) ↦ (↑(l₂ a) : Multiset (σ a))) =
    (↑(l₁.sigma (σ := σ) l₂) : Multiset ((a : α) × σ a))

Tactic:
rw [Multiset.sigma, List.sigma, ← coe_bind]

Premises used: Multiset.coe_bind, List.sigma, Multiset.sigma