ι : Type ?u.498342
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : List α
s : Finset α
hs : toFinset m ⊆ s
⊢ ∏ m_1 in toFinset m, m_1 ^ count m_1 m = ∏ i in s, i ^ count i m
ι : Type ?u.498342
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : List α
s : Finset α
hs : toFinset m ⊆ s
⊢ prod m = ∏ i in s, i ^ count i m
rw [prod_list_count]
ι : Type ?u.498342
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : List α
s : Finset α
hs : toFinset m ⊆ s
x : α
x✝ : x ∈ s
hx : ¬x ∈ toFinset m
⊢ x ^ count x m = 1
ι : Type ?u.498342
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : List α
s : Finset α
hs : toFinset m ⊆ s
⊢ ∏ m_1 in toFinset m, m_1 ^ count m_1 m = ∏ i in s, i ^ count i m
refine' prod_subset hs fun x _ hx => _
ι : Type ?u.498342
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : List α
s : Finset α
hs : toFinset m ⊆ s
x : α
x✝ : x ∈ s
hx : ¬x ∈ m
⊢ x ^ count x m = 1
ι : Type ?u.498342
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : List α
s : Finset α
hs : toFinset m ⊆ s
x : α
x✝ : x ∈ s
hx : ¬x ∈ toFinset m
⊢ x ^ count x m = 1
rw [mem_toFinset] at hx
no goals
ι : Type ?u.498342
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : List α
s : Finset α
hs : toFinset m ⊆ s
x : α
x✝ : x ∈ s
hx : ¬x ∈ m
⊢ x ^ count x m = 1
rw [count_eq_zero_of_not_mem hx, pow_zero]