case h
F : Type ?u.111005
ι : Type ?u.111008
α : Type u_1
β : Type ?u.111014
γ : Type ?u.111017
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
m : α
a✝ : List α
comm : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid α) a✝} Commute
h : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) a✝ → x = m
⊢ noncommProd (Quotient.mk (List.isSetoid α) a✝) comm = m ^ ↑card (Quotient.mk (List.isSetoid α) a✝)
F : Type ?u.111005
ι : Type ?u.111008
α : Type u_1
β : Type ?u.111014
γ : Type ?u.111017
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s : Multiset α
comm : Set.Pairwise {x | x ∈ s} Commute
m : α
h : ∀ (x : α), x ∈ s → x = m
⊢ noncommProd s comm = m ^ ↑card s
induction s using Quotient.inductionOn
case h
F : Type ?u.111005
ι : Type ?u.111008
α : Type u_1
β : Type ?u.111014
γ : Type ?u.111017
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
m : α
a✝ : List α
comm : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid α) a✝} Commute
h : ∀ (x : α), x ∈ a✝ → x = m
⊢ List.prod a✝ = m ^ List.length a✝
case h
F : Type ?u.111005
ι : Type ?u.111008
α : Type u_1
β : Type ?u.111014
γ : Type ?u.111017
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
m : α
a✝ : List α
comm : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid α) a✝} Commute
h : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) a✝ → x = m
⊢ noncommProd (Quotient.mk (List.isSetoid α) a✝) comm = m ^ ↑card (Quotient.mk (List.isSetoid α) a✝)
simp only [quot_mk_to_coe, noncommProd_coe, coe_card, mem_coe] at *
no goals
case h
F : Type ?u.111005
ι : Type ?u.111008
α : Type u_1
β : Type ?u.111014
γ : Type ?u.111017
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
m : α
a✝ : List α
comm : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid α) a✝} Commute
h : ∀ (x : α), x ∈ a✝ → x = m
⊢ List.prod a✝ = m ^ List.length a✝
exact List.prod_eq_pow_card _ m h