[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : List α
L : List (List α)
⊢ join ↑(List.map ofList (l :: L)) = ↑(List.join (l :: L))
[PROOFSTEP]
simp only [join, List.map, coe_sum, List.sum_cons, List.join, ← coe_add, ← coe_join L]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
S : Multiset (Multiset α)
⊢ a ∈ join 0 ↔ ∃ s, s ∈ 0 ∧ a ∈ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
S : Multiset (Multiset α)
⊢ ∀ ⦃a_1 : Multiset α⦄ {s : Multiset (Multiset α)},
    (a ∈ join s ↔ ∃ s_1, s_1 ∈ s ∧ a ∈ s_1) → (a ∈ join (a_1 ::ₘ s) ↔ ∃ s_1, s_1 ∈ a_1 ::ₘ s ∧ a ∈ s_1)
[PROOFSTEP]
simp (config := { contextual := true }) [or_and_right, exists_or]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
S : Multiset (Multiset α)
⊢ ↑card (join 0) = sum (map (↑card) 0)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
S : Multiset (Multiset α)
⊢ ∀ ⦃a : Multiset α⦄ {s : Multiset (Multiset α)},
    ↑card (join s) = sum (map (↑card) s) → ↑card (join (a ::ₘ s)) = sum (map (↑card) (a ::ₘ s))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
h : Rel (Rel r) s t
⊢ Rel r (join s) (join t)
[PROOFSTEP]
induction h
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
⊢ Rel r (join 0) (join 0)
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
a✝² : Multiset α
b✝ : Multiset β
as✝ : Multiset (Multiset α)
bs✝ : Multiset (Multiset β)
a✝¹ : Rel r a✝² b✝
a✝ : Rel (Rel r) as✝ bs✝
a_ih✝ : Rel r (join as✝) (join bs✝)
⊢ Rel r (join (a✝² ::ₘ as✝)) (join (b✝ ::ₘ bs✝))
[PROOFSTEP]
case zero => simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
⊢ Rel r (join 0) (join 0)
[PROOFSTEP]
case zero => simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
⊢ Rel r (join 0) (join 0)
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
a✝² : Multiset α
b✝ : Multiset β
as✝ : Multiset (Multiset α)
bs✝ : Multiset (Multiset β)
a✝¹ : Rel r a✝² b✝
a✝ : Rel (Rel r) as✝ bs✝
a_ih✝ : Rel r (join as✝) (join bs✝)
⊢ Rel r (join (a✝² ::ₘ as✝)) (join (b✝ ::ₘ bs✝))
[PROOFSTEP]
case cons a b s t hab hst ih => simpa using hab.add ih
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
s✝ : Multiset (Multiset α)
t✝ : Multiset (Multiset β)
a : Multiset α
b : Multiset β
s : Multiset (Multiset α)
t : Multiset (Multiset β)
hab : Rel r a b
hst : Rel (Rel r) s t
ih : Rel r (join s) (join t)
⊢ Rel r (join (a ::ₘ s)) (join (b ::ₘ t))
[PROOFSTEP]
case cons a b s t hab hst ih => simpa using hab.add ih
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
s✝ : Multiset (Multiset α)
t✝ : Multiset (Multiset β)
a : Multiset α
b : Multiset β
s : Multiset (Multiset α)
t : Multiset (Multiset β)
hab : Rel r a b
hst : Rel (Rel r) s t
ih : Rel r (join s) (join t)
⊢ Rel r (join (a ::ₘ s)) (join (b ::ₘ t))
[PROOFSTEP]
simpa using hab.add ih
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
l : List α
f : α → List β
⊢ (bind ↑l fun a => ↑(f a)) = ↑(List.bind l f)
[PROOFSTEP]
rw [List.bind, ← coe_join, List.map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
l : List α
f : α → List β
⊢ (bind ↑l fun a => ↑(f a)) = join ↑(List.map (ofList ∘ f) l)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f g : α → Multiset β
⊢ bind (a ::ₘ s) f = f a + bind s f
[PROOFSTEP]
simp [bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f g : α → Multiset β
⊢ bind {a} f = f a
[PROOFSTEP]
simp [bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f g : α → Multiset β
⊢ bind (s + t) f = bind s f + bind t f
[PROOFSTEP]
simp [bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f g : α → Multiset β
⊢ (bind s fun x => 0) = 0
[PROOFSTEP]
simp [bind, join, nsmul_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f g : α → Multiset β
⊢ (bind s fun a => f a + g a) = bind s f + bind s g
[PROOFSTEP]
simp [bind, join]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g✝ : α → Multiset β
f : α → β
g : α → Multiset β
⊢ (bind 0 fun a => f a ::ₘ g a) = map f 0 + bind 0 g
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g✝ : α → Multiset β
f : α → β
g : α → Multiset β
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    (bind s fun a => f a ::ₘ g a) = map f s + bind s g →
      (bind (a ::ₘ s) fun a => f a ::ₘ g a) = map f (a ::ₘ s) + bind (a ::ₘ s) g
[PROOFSTEP]
simp (config := { contextual := true }) [add_comm, add_left_comm, add_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
f : α → β
⊢ (bind 0 fun x => {f x}) = map f 0
[PROOFSTEP]
rw [zero_bind, map_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
f : α → β
⊢ ∀ ⦃a : α⦄ {s : Multiset α}, (bind s fun x => {f x}) = map f s → (bind (a ::ₘ s) fun x => {f x}) = map f (a ::ₘ s)
[PROOFSTEP]
simp [singleton_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s✝ t : Multiset α
f✝ g : α → Multiset β
b : β
s : Multiset α
f : α → Multiset β
⊢ b ∈ bind s f ↔ ∃ a, a ∈ s ∧ b ∈ f a
[PROOFSTEP]
simp [bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f g : α → Multiset β
⊢ ↑card (bind s f) = sum (map (↑card ∘ f) s)
[PROOFSTEP]
simp [bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g✝ f g : α → Multiset β
m : Multiset α
⊢ (∀ (a : α), a ∈ m → f a = g a) → bind m f = bind m g
[PROOFSTEP]
simp (config := { contextual := true }) [bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
β' : Type u_2
m : Multiset α
f : α → Multiset β
f' : α → Multiset β'
h : β = β'
hf : ∀ (a : α), a ∈ m → HEq (f a) (f' a)
⊢ HEq (bind m f) (bind m f')
[PROOFSTEP]
subst h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
f f' : α → Multiset β
hf : ∀ (a : α), a ∈ m → HEq (f a) (f' a)
⊢ HEq (bind m f) (bind m f')
[PROOFSTEP]
simp only [heq_eq_eq] at hf 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
f f' : α → Multiset β
hf : ∀ (a : α), a ∈ m → f a = f' a
⊢ HEq (bind m f) (bind m f')
[PROOFSTEP]
simp [bind_congr hf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
n : α → Multiset β
f : β → γ
⊢ map f (bind 0 n) = bind 0 fun a => map f (n a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
n : α → Multiset β
f : β → γ
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    (map f (bind s n) = bind s fun a => map f (n a)) → map f (bind (a ::ₘ s) n) = bind (a ::ₘ s) fun a => map f (n a)
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
n : β → Multiset γ
f : α → β
⊢ bind (map f 0) n = bind 0 fun a => n (f a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
n : β → Multiset γ
f : α → β
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    (bind (map f s) n = bind s fun a => n (f a)) → bind (map f (a ::ₘ s)) n = bind (a ::ₘ s) fun a => n (f a)
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s✝ t : Multiset α
f✝ g✝ : α → Multiset β
s : Multiset α
f : α → Multiset β
g : β → Multiset γ
⊢ bind (bind 0 f) g = bind 0 fun a => bind (f a) g
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s✝ t : Multiset α
f✝ g✝ : α → Multiset β
s : Multiset α
f : α → Multiset β
g : β → Multiset γ
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    (bind (bind s f) g = bind s fun a => bind (f a) g) →
      bind (bind (a ::ₘ s) f) g = bind (a ::ₘ s) fun a => bind (f a) g
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
n : Multiset β
f : α → β → Multiset γ
⊢ (bind 0 fun a => bind n fun b => f a b) = bind n fun b => bind 0 fun a => f a b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
n : Multiset β
f : α → β → Multiset γ
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    ((bind s fun a => bind n fun b => f a b) = bind n fun b => bind s fun a => f a b) →
      (bind (a ::ₘ s) fun a => bind n fun b => f a b) = bind n fun b => bind (a ::ₘ s) fun a => f a b
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
n : Multiset β
f : α → β → γ
⊢ (bind 0 fun a => map (fun b => f a b) n) = bind n fun b => map (fun a => f a b) 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
n : Multiset β
f : α → β → γ
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    ((bind s fun a => map (fun b => f a b) n) = bind n fun b => map (fun a => f a b) s) →
      (bind (a ::ₘ s) fun a => map (fun b => f a b) n) = bind n fun b => map (fun a => f a b) (a ::ₘ s)
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s✝ t✝ : Multiset α
f g : α → Multiset β
inst✝ : CommMonoid β
s : Multiset α
t : α → Multiset β
⊢ prod (bind 0 t) = prod (map (fun a => prod (t a)) 0)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ : α
s✝¹ t✝ : Multiset α
f g : α → Multiset β
inst✝ : CommMonoid β
s✝ : Multiset α
t : α → Multiset β
a : α
s : Multiset α
ih : prod (bind s t) = prod (map (fun a => prod (t a)) s)
⊢ prod (bind (a ::ₘ s) t) = prod (map (fun a => prod (t a)) (a ::ₘ s))
[PROOFSTEP]
simp [ih, cons_bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s✝ t✝ : Multiset α
f✝ g✝ : α → Multiset β
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel p (bind s f) (bind t g)
[PROOFSTEP]
apply rel_join
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s✝ t✝ : Multiset α
f✝ g✝ : α → Multiset β
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel (Rel p) (map f s) (map g t)
[PROOFSTEP]
rw [rel_map]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s✝ t✝ : Multiset α
f✝ g✝ : α → Multiset β
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
[PROOFSTEP]
exact hst.mono fun a _ b _ hr => h hr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ : α
s t : Multiset α
f✝ g : α → Multiset β
inst✝ : DecidableEq α
m : Multiset β
f : β → Multiset α
a : α
⊢ count a (sum (map f 0)) = sum (map (fun b => count a (f b)) 0)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ : α
s t : Multiset α
f✝ g : α → Multiset β
inst✝ : DecidableEq α
m : Multiset β
f : β → Multiset α
a : α
⊢ ∀ ⦃a_1 : β⦄ {s : Multiset β},
    count a (sum (map f s)) = sum (map (fun b => count a (f b)) s) →
      count a (sum (map f (a_1 ::ₘ s))) = sum (map (fun b => count a (f b)) (a_1 ::ₘ s))
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
a : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_5
β : Type u_6
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
⊢ f x ≤ bind S f
[PROOFSTEP]
classical
rw [le_iff_count]
intro a
rw [count_bind]
apply le_sum_of_mem
rw [mem_map]
exact ⟨x, hx, rfl⟩
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
a : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_5
β : Type u_6
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
⊢ f x ≤ bind S f
[PROOFSTEP]
rw [le_iff_count]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
a : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_5
β : Type u_6
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
⊢ ∀ (a : β), count a (f x) ≤ count a (bind S f)
[PROOFSTEP]
intro a
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
a✝ : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_5
β : Type u_6
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
⊢ count a (f x) ≤ count a (bind S f)
[PROOFSTEP]
rw [count_bind]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
a✝ : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_5
β : Type u_6
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
⊢ count a (f x) ≤ sum (map (fun b => count a (f b)) S)
[PROOFSTEP]
apply le_sum_of_mem
[GOAL]
case h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
a✝ : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_5
β : Type u_6
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
⊢ count a (f x) ∈ map (fun b => count a (f b)) S
[PROOFSTEP]
rw [mem_map]
[GOAL]
case h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
a✝ : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_5
β : Type u_6
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
⊢ ∃ a_1, a_1 ∈ S ∧ count a (f a_1) = count a (f x)
[PROOFSTEP]
exact ⟨x, hx, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
b : β
s : Multiset α
t : Multiset β
l₁ : List α
l₂ : List β
⊢ ↑l₁ ×ˢ ↑l₂ = ↑(l₁ ×ˢ l₂)
[PROOFSTEP]
dsimp only [SProd.sprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
b : β
s : Multiset α
t : Multiset β
l₁ : List α
l₂ : List β
⊢ product ↑l₁ ↑l₂ = ↑(List.product l₁ l₂)
[PROOFSTEP]
rw [product, List.product, ← coe_bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
b : β
s : Multiset α
t : Multiset β
l₁ : List α
l₂ : List β
⊢ (bind ↑l₁ fun a => map (Prod.mk a) ↑l₂) = bind ↑l₁ fun a => ↑(List.map (Prod.mk a) l₂)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
b : β
s : Multiset α
t : Multiset β
⊢ (a ::ₘ s) ×ˢ t = map (Prod.mk a) t + s ×ˢ t
[PROOFSTEP]
simp [SProd.sprod, product]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
b : β
s : Multiset α
t : Multiset β
⊢ s ×ˢ 0 = 0
[PROOFSTEP]
simp [SProd.sprod, product]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
b : β
s : Multiset α
t : Multiset β
⊢ s ×ˢ (b ::ₘ t) = map (fun a => (a, b)) s + s ×ˢ t
[PROOFSTEP]
simp [SProd.sprod, product]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
b : β
s : Multiset α
t : Multiset β
⊢ {a} ×ˢ {b} = {(a, b)}
[PROOFSTEP]
simp only [SProd.sprod, product, bind_singleton, map_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
b : β
s✝ : Multiset α
t✝ : Multiset β
s t : Multiset α
u : Multiset β
⊢ (s + t) ×ˢ u = s ×ˢ u + t ×ˢ u
[PROOFSTEP]
simp [SProd.sprod, product]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ : α
b : β
s✝¹ : Multiset α
t✝ : Multiset β
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
t u : Multiset β
⊢ (a ::ₘ s) ×ˢ (t + u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u
[PROOFSTEP]
rw [cons_product, IH]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ : α
b : β
s✝¹ : Multiset α
t✝ : Multiset β
s✝ : 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
[PROOFSTEP]
simp [add_comm, add_left_comm, add_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ : α
b✝ : β
s✝ : Multiset α
t✝ : Multiset β
s : Multiset α
t : Multiset β
a : α
b : β
⊢ (a, b) ∈ product s t ↔ (a, b).fst ∈ s ∧ (a, b).snd ∈ t
[PROOFSTEP]
simp [product, and_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
b : β
s : Multiset α
t : Multiset β
⊢ ↑card (s ×ˢ t) = ↑card s * ↑card t
[PROOFSTEP]
simp [SProd.sprod, product]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : α → Type u_5
a : α
s : Multiset α
t : (a : α) → Multiset (σ a)
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ (Multiset.sigma ↑l₁ fun a => ↑(l₂ a)) = ↑(List.sigma l₁ l₂)
[PROOFSTEP]
rw [Multiset.sigma, List.sigma, ← coe_bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : α → Type u_5
a : α
s : Multiset α
t : (a : α) → Multiset (σ a)
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ (bind ↑l₁ fun a => map (Sigma.mk a) ↑(l₂ a)) = bind ↑l₁ fun a => ↑(List.map (Sigma.mk a) (l₂ a))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : α → Type u_5
a : α
s : Multiset α
t : (a : α) → Multiset (σ a)
⊢ Multiset.sigma (a ::ₘ s) t = map (Sigma.mk a) (t a) + Multiset.sigma s t
[PROOFSTEP]
simp [Multiset.sigma]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : α → Type u_5
a : α
s✝ : Multiset α
t✝ : (a : α) → Multiset (σ a)
s t : Multiset α
u : (a : α) → Multiset (σ a)
⊢ Multiset.sigma (s + t) u = Multiset.sigma s u + Multiset.sigma t u
[PROOFSTEP]
simp [Multiset.sigma]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : α → Type u_5
a✝ : α
s✝ : Multiset α
t✝ : (a : α) → Multiset (σ a)
a : α
s : Multiset α
IH : ∀ (t u : (a : α) → Multiset (σ a)), (Multiset.sigma s fun a => t a + u a) = Multiset.sigma s t + Multiset.sigma s u
t u : (a : α) → Multiset (σ a)
⊢ (Multiset.sigma (a ::ₘ s) fun a => t a + u a) = Multiset.sigma (a ::ₘ s) t + Multiset.sigma (a ::ₘ s) u
[PROOFSTEP]
rw [cons_sigma, IH]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : α → Type u_5
a✝ : α
s✝ : Multiset α
t✝ : (a : α) → Multiset (σ a)
a : α
s : Multiset α
IH : ∀ (t u : (a : α) → Multiset (σ a)), (Multiset.sigma s fun a => t a + u a) = Multiset.sigma s t + Multiset.sigma s u
t u : (a : α) → Multiset (σ a)
⊢ map (Sigma.mk a) (t a + u a) + ((Multiset.sigma s fun a => t a) + Multiset.sigma s fun a => u a) =
    Multiset.sigma (a ::ₘ s) t + Multiset.sigma (a ::ₘ s) u
[PROOFSTEP]
simp [add_comm, add_left_comm, add_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : α → Type u_5
a✝ : α
s✝ : Multiset α
t✝ : (a : α) → Multiset (σ a)
s : Multiset α
t : (a : α) → Multiset (σ a)
a : α
b : σ a
⊢ { fst := a, snd := b } ∈ Multiset.sigma s t ↔
    { fst := a, snd := b }.fst ∈ s ∧ { fst := a, snd := b }.snd ∈ t { fst := a, snd := b }.fst
[PROOFSTEP]
simp [Multiset.sigma, and_assoc, and_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : α → Type u_5
a : α
s : Multiset α
t : (a : α) → Multiset (σ a)
⊢ ↑card (Multiset.sigma s t) = sum (map (fun a => ↑card (t a)) s)
[PROOFSTEP]
simp [Multiset.sigma, (· ∘ ·)]
