[GOAL]
α : Type u_1
s : Multiset (Multiset α)
a₀ a₁ : Multiset α
x✝ pi : Multiset (Multiset α)
⊢ HEq (bind a₀ fun a => map (cons a) (bind a₁ fun a => map (cons a) pi))
    (bind a₁ fun a => map (cons a) (bind a₀ fun a => map (cons a) pi))
[PROOFSTEP]
simp [map_bind, bind_bind a₀ a₁, cons_swap]
[GOAL]
α : Type u_1
a : List α
l : List (List α)
⊢ Sections ↑(List.map (fun l => ↑l) (a :: l)) = ↑(List.map (fun l => ↑l) (List.sections (a :: l)))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
a : List α
l : List (List α)
⊢ Sections ↑(↑a :: List.map (fun l => ↑l) l) =
    ↑(List.map (fun l => ↑l) (List.bind (List.sections l) fun s => List.map (fun a => a :: s) a))
[PROOFSTEP]
rw [← cons_coe, sections_cons, bind_map_comm, coe_sections l]
[GOAL]
α : Type u_1
a : List α
l : List (List α)
⊢ (bind ↑(List.map (fun l => ↑l) (List.sections l)) fun b => map (fun a => a ::ₘ b) ↑a) =
    ↑(List.map (fun l => ↑l) (List.bind (List.sections l) fun s => List.map (fun a => a :: s) a))
[PROOFSTEP]
simp [List.sections, (· ∘ ·), List.bind]
[GOAL]
α : Type u_1
s t : Multiset (Multiset α)
⊢ Sections (0 + t) = bind (Sections 0) fun m => map ((fun x x_1 => x + x_1) m) (Sections t)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
s✝ t : Multiset (Multiset α)
a : Multiset α
s : Multiset (Multiset α)
ih : Sections (s + t) = bind (Sections s) fun m => map ((fun x x_1 => x + x_1) m) (Sections t)
⊢ Sections (a ::ₘ s + t) = bind (Sections (a ::ₘ s)) fun m => map ((fun x x_1 => x + x_1) m) (Sections t)
[PROOFSTEP]
simp [ih, bind_assoc, map_bind, bind_map]
[GOAL]
α : Type u_1
s : Multiset (Multiset α)
⊢ ∀ {a : Multiset α}, a ∈ Sections s ↔ Rel (fun s a => a ∈ s) s a
[PROOFSTEP]
induction s using Multiset.induction_on
[GOAL]
case empty
α : Type u_1
⊢ ∀ {a : Multiset α}, a ∈ Sections 0 ↔ Rel (fun s a => a ∈ s) 0 a
case cons
α : Type u_1
a✝¹ : Multiset α
s✝ : Multiset (Multiset α)
a✝ : ∀ {a : Multiset α}, a ∈ Sections s✝ ↔ Rel (fun s a => a ∈ s) s✝ a
⊢ ∀ {a : Multiset α}, a ∈ Sections (a✝¹ ::ₘ s✝) ↔ Rel (fun s a => a ∈ s) (a✝¹ ::ₘ s✝) a
[PROOFSTEP]
case empty => simp
[GOAL]
α : Type u_1
⊢ ∀ {a : Multiset α}, a ∈ Sections 0 ↔ Rel (fun s a => a ∈ s) 0 a
[PROOFSTEP]
case empty => simp
[GOAL]
α : Type u_1
⊢ ∀ {a : Multiset α}, a ∈ Sections 0 ↔ Rel (fun s a => a ∈ s) 0 a
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
a✝¹ : Multiset α
s✝ : Multiset (Multiset α)
a✝ : ∀ {a : Multiset α}, a ∈ Sections s✝ ↔ Rel (fun s a => a ∈ s) s✝ a
⊢ ∀ {a : Multiset α}, a ∈ Sections (a✝¹ ::ₘ s✝) ↔ Rel (fun s a => a ∈ s) (a✝¹ ::ₘ s✝) a
[PROOFSTEP]
case cons a a' ih => simp [ih, rel_cons_left, eq_comm]
[GOAL]
α : Type u_1
a : Multiset α
a' : Multiset (Multiset α)
ih : ∀ {a : Multiset α}, a ∈ Sections a' ↔ Rel (fun s a => a ∈ s) a' a
⊢ ∀ {a_1 : Multiset α}, a_1 ∈ Sections (a ::ₘ a') ↔ Rel (fun s a => a ∈ s) (a ::ₘ a') a_1
[PROOFSTEP]
case cons a a' ih => simp [ih, rel_cons_left, eq_comm]
[GOAL]
α : Type u_1
a : Multiset α
a' : Multiset (Multiset α)
ih : ∀ {a : Multiset α}, a ∈ Sections a' ↔ Rel (fun s a => a ∈ s) a' a
⊢ ∀ {a_1 : Multiset α}, a_1 ∈ Sections (a ::ₘ a') ↔ Rel (fun s a => a ∈ s) (a ::ₘ a') a_1
[PROOFSTEP]
simp [ih, rel_cons_left, eq_comm]
[GOAL]
α : Type u_1
s : Multiset (Multiset α)
⊢ ↑card (Sections 0) = prod (map (↑card) 0)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
s : Multiset (Multiset α)
⊢ ∀ ⦃a : Multiset α⦄ {s : Multiset (Multiset α)},
    ↑card (Sections s) = prod (map (↑card) s) → ↑card (Sections (a ::ₘ s)) = prod (map (↑card) (a ::ₘ s))
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
s : Multiset (Multiset α)
⊢ prod (map sum 0) = sum (map prod (Sections 0))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
s✝ : Multiset (Multiset α)
a : Multiset α
s : Multiset (Multiset α)
ih : prod (map sum s) = sum (map prod (Sections s))
⊢ prod (map sum (a ::ₘ s)) = sum (map prod (Sections (a ::ₘ s)))
[PROOFSTEP]
simp [ih, map_bind, sum_map_mul_left, sum_map_mul_right]
