case empty
α : Type u_2
β : Type u_1
f : α → β
n✝ n : ℕ
⊢ powersetLen n (map f 0) = map (map f) (powersetLen n 0)

case cons
α : Type u_2
β : Type u_1
f : α → β
n✝ : ℕ
t : α
s : Multiset α
ih : ∀ (n : ℕ), powersetLen n (map f s) = map (map f) (powersetLen n s)
n : ℕ
⊢ powersetLen n (map f (t ::ₘ s)) = map (map f) (powersetLen n (t ::ₘ s))
α : Type u_2
β : Type u_1
f : α → β
n : ℕ
s : Multiset α
⊢ powersetLen n (map f s) = map (map f) (powersetLen n s)
induction' s using Multiset.induction with t s ih generalizing n
no goals
case empty
α : Type u_2
β : Type u_1
f : α → β
n✝ n : ℕ
⊢ powersetLen n (map f 0) = map (map f) (powersetLen n 0)
cases n <;> simp [powersetLen_zero_left, powersetLen_zero_right]
no goals
case cons
α : Type u_2
β : Type u_1
f : α → β
n✝ : ℕ
t : α
s : Multiset α
ih : ∀ (n : ℕ), powersetLen n (map f s) = map (map f) (powersetLen n s)
n : ℕ
⊢ powersetLen n (map f (t ::ₘ s)) = map (map f) (powersetLen n (t ::ₘ s))
cases n <;> simp [ih, map_comp_cons]