no goals
ι : Type ?u.76244
α : Type u_3
β : Type u_1
γ : Type u_2
inst✝ : CommMonoid α
s t : Multiset α
a : α
m✝ : Multiset ι
f✝ g : ι → α
m : Multiset β
n : Multiset γ
f : β → γ → α
⊢ prod (map (fun a => prod (map (fun b => f a b) n)) 0) = prod (map (fun b => prod (map (fun a => f a b) 0)) n)
simp
no goals
ι : Type ?u.76244
α : Type u_3
β : Type u_1
γ : Type u_2
inst✝ : CommMonoid α
s t : Multiset α
a✝ : α
m✝¹ : Multiset ι
f✝ g : ι → α
m✝ : Multiset β
n : Multiset γ
f : β → γ → α
a : β
m : Multiset β
ih : prod (map (fun a => prod (map (fun b => f a b) n)) m) = prod (map (fun b => prod (map (fun a => f a b) m)) n)
⊢ prod (map (fun a => prod (map (fun b => f a b) n)) (a ::ₘ m)) =
    prod (map (fun b => prod (map (fun a => f a b) (a ::ₘ m))) n)
simp [ih]