F : Type ?u.176728
ι : Type ?u.176731
α : Type u_1
β : Type u_2
γ : Type ?u.176740
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
m : β
h : ∀ (x : α), x ∈ s → f x = m
⊢ m ^ ↑Multiset.card (Multiset.map f s.val) = m ^ card s

F : Type ?u.176728
ι : Type ?u.176731
α : Type u_1
β : Type u_2
γ : Type ?u.176740
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
m : β
h : ∀ (x : α), x ∈ s → f x = m
⊢ ∀ (x : β), x ∈ Multiset.map f s.val → x = m
F : Type ?u.176728
ι : Type ?u.176731
α : Type u_1
β : Type u_2
γ : Type ?u.176740
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
m : β
h : ∀ (x : α), x ∈ s → f x = m
⊢ noncommProd s f comm = m ^ card s
rw [noncommProd, Multiset.noncommProd_eq_pow_card _ _ m]
F : Type ?u.176728
ι : Type ?u.176731
α : Type u_1
β : Type u_2
γ : Type ?u.176740
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
m : β
h : ∀ (x : α), x ∈ s → f x = m
⊢ ∀ (x : β), x ∈ Multiset.map f s.val → x = m
F : Type ?u.176728
ι : Type ?u.176731
α : Type u_1
β : Type u_2
γ : Type ?u.176740
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
m : β
h : ∀ (x : α), x ∈ s → f x = m
⊢ m ^ ↑Multiset.card (Multiset.map f s.val) = m ^ card s

F : Type ?u.176728
ι : Type ?u.176731
α : Type u_1
β : Type u_2
γ : Type ?u.176740
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
m : β
h : ∀ (x : α), x ∈ s → f x = m
⊢ ∀ (x : β), x ∈ Multiset.map f s.val → x = m
simp only [Finset.card_def, Multiset.card_map]
no goals
F : Type ?u.176728
ι : Type ?u.176731
α : Type u_1
β : Type u_2
γ : Type ?u.176740
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
m : β
h : ∀ (x : α), x ∈ s → f x = m
⊢ ∀ (x : β), x ∈ Multiset.map f s.val → x = m
simpa using h