case h
ι : Type ?u.29694
α : Type u_1
β : Type ?u.29700
γ : Type ?u.29703
inst✝¹ : CommMonoid α
s t : Multiset α
a✝ : α
m : Multiset ι
f g : ι → α
inst✝ : DecidableEq α
a : α
h✝ : ∀ (a' : α), a' ≠ a → a' ∈ s → a' = 1
l : List α
h : ∀ (a' : α), a' ≠ a → a' ∈ Quotient.mk (List.isSetoid α) l → a' = 1
⊢ prod (Quotient.mk (List.isSetoid α) l) = a ^ count a (Quotient.mk (List.isSetoid α) l)
ι : Type ?u.29694
α : Type u_1
β : Type ?u.29700
γ : Type ?u.29703
inst✝¹ : CommMonoid α
s t : Multiset α
a✝ : α
m : Multiset ι
f g : ι → α
inst✝ : DecidableEq α
a : α
h : ∀ (a' : α), a' ≠ a → a' ∈ s → a' = 1
⊢ prod s = a ^ count a s
induction' s using Quotient.inductionOn with l
no goals
case h
ι : Type ?u.29694
α : Type u_1
β : Type ?u.29700
γ : Type ?u.29703
inst✝¹ : CommMonoid α
s t : Multiset α
a✝ : α
m : Multiset ι
f g : ι → α
inst✝ : DecidableEq α
a : α
h✝ : ∀ (a' : α), a' ≠ a → a' ∈ s → a' = 1
l : List α
h : ∀ (a' : α), a' ≠ a → a' ∈ Quotient.mk (List.isSetoid α) l → a' = 1
⊢ prod (Quotient.mk (List.isSetoid α) l) = a ^ count a (Quotient.mk (List.isSetoid α) l)
simp [List.prod_eq_pow_single a h]