F : Type ?u.7239
ι : Type ?u.7242
α : Type u_1
β : Type ?u.7248
γ : Type ?u.7251
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
l : List α
comm : Set.Pairwise {x | x ∈ ↑l} Commute
⊢ noncommFold (fun x x_1 => x * x_1) (↑l) comm 1 = List.prod l
F : Type ?u.7239
ι : Type ?u.7242
α : Type u_1
β : Type ?u.7248
γ : Type ?u.7251
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
l : List α
comm : Set.Pairwise {x | x ∈ ↑l} Commute
⊢ noncommProd (↑l) comm = List.prod l
rw [noncommProd]
F : Type ?u.7239
ι : Type ?u.7242
α : Type u_1
β : Type ?u.7248
γ : Type ?u.7251
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
l : List α
comm : Set.Pairwise {x | x ∈ ↑l} Commute
⊢ List.foldr (fun x x_1 => x * x_1) 1 l = List.prod l
F : Type ?u.7239
ι : Type ?u.7242
α : Type u_1
β : Type ?u.7248
γ : Type ?u.7251
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
l : List α
comm : Set.Pairwise {x | x ∈ ↑l} Commute
⊢ noncommFold (fun x x_1 => x * x_1) (↑l) comm 1 = List.prod l
simp only [noncommFold_coe]
case nil
F : Type ?u.7239
ι : Type ?u.7242
α : Type u_1
β : Type ?u.7248
γ : Type ?u.7251
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
l : List α
comm✝ : Set.Pairwise {x | x ∈ ↑l} Commute
comm : Set.Pairwise {x | x ∈ ↑[]} Commute
⊢ List.foldr (fun x x_1 => x * x_1) 1 [] = List.prod []

case cons
F : Type ?u.7239
ι : Type ?u.7242
α : Type u_1
β : Type ?u.7248
γ : Type ?u.7251
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
l : List α
comm✝ : Set.Pairwise {x | x ∈ ↑l} Commute
hd : α
tl : List α
hl : Set.Pairwise {x | x ∈ ↑tl} Commute → List.foldr (fun x x_1 => x * x_1) 1 tl = List.prod tl
comm : Set.Pairwise {x | x ∈ ↑(hd :: tl)} Commute
⊢ List.foldr (fun x x_1 => x * x_1) 1 (hd :: tl) = List.prod (hd :: tl)
F : Type ?u.7239
ι : Type ?u.7242
α : Type u_1
β : Type ?u.7248
γ : Type ?u.7251
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
l : List α
comm : Set.Pairwise {x | x ∈ ↑l} Commute
⊢ List.foldr (fun x x_1 => x * x_1) 1 l = List.prod l
induction' l with hd tl hl
no goals
case nil
F : Type ?u.7239
ι : Type ?u.7242
α : Type u_1
β : Type ?u.7248
γ : Type ?u.7251
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
l : List α
comm✝ : Set.Pairwise {x | x ∈ ↑l} Commute
comm : Set.Pairwise {x | x ∈ ↑[]} Commute
⊢ List.foldr (fun x x_1 => x * x_1) 1 [] = List.prod []
simp
case cons
F : Type ?u.7239
ι : Type ?u.7242
α : Type u_1
β : Type ?u.7248
γ : Type ?u.7251
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
l : List α
comm✝ : Set.Pairwise {x | x ∈ ↑l} Commute
hd : α
tl : List α
hl : Set.Pairwise {x | x ∈ ↑tl} Commute → List.foldr (fun x x_1 => x * x_1) 1 tl = List.prod tl
comm : Set.Pairwise {x | x ∈ ↑(hd :: tl)} Commute
⊢ Set.Pairwise {x | x ∈ ↑tl} Commute
case cons
F : Type ?u.7239
ι : Type ?u.7242
α : Type u_1
β : Type ?u.7248
γ : Type ?u.7251
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
l : List α
comm✝ : Set.Pairwise {x | x ∈ ↑l} Commute
hd : α
tl : List α
hl : Set.Pairwise {x | x ∈ ↑tl} Commute → List.foldr (fun x x_1 => x * x_1) 1 tl = List.prod tl
comm : Set.Pairwise {x | x ∈ ↑(hd :: tl)} Commute
⊢ List.foldr (fun x x_1 => x * x_1) 1 (hd :: tl) = List.prod (hd :: tl)
rw [List.prod_cons, List.foldr, hl]
case cons
F : Type ?u.7239
ι : Type ?u.7242
α : Type u_1
β : Type ?u.7248
γ : Type ?u.7251
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
l : List α
comm✝ : Set.Pairwise {x | x ∈ ↑l} Commute
hd : α
tl : List α
hl : Set.Pairwise {x | x ∈ ↑tl} Commute → List.foldr (fun x x_1 => x * x_1) 1 tl = List.prod tl
comm : Set.Pairwise {x | x ∈ ↑(hd :: tl)} Commute
x : α
hx : x ∈ {x | x ∈ ↑tl}
y : α
hy : y ∈ {x | x ∈ ↑tl}
⊢ x ≠ y → Commute x y
case cons
F : Type ?u.7239
ι : Type ?u.7242
α : Type u_1
β : Type ?u.7248
γ : Type ?u.7251
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
l : List α
comm✝ : Set.Pairwise {x | x ∈ ↑l} Commute
hd : α
tl : List α
hl : Set.Pairwise {x | x ∈ ↑tl} Commute → List.foldr (fun x x_1 => x * x_1) 1 tl = List.prod tl
comm : Set.Pairwise {x | x ∈ ↑(hd :: tl)} Commute
⊢ Set.Pairwise {x | x ∈ ↑tl} Commute
intro x hx y hy
no goals
case cons
F : Type ?u.7239
ι : Type ?u.7242
α : Type u_1
β : Type ?u.7248
γ : Type ?u.7251
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
l : List α
comm✝ : Set.Pairwise {x | x ∈ ↑l} Commute
hd : α
tl : List α
hl : Set.Pairwise {x | x ∈ ↑tl} Commute → List.foldr (fun x x_1 => x * x_1) 1 tl = List.prod tl
comm : Set.Pairwise {x | x ∈ ↑(hd :: tl)} Commute
x : α
hx : x ∈ {x | x ∈ ↑tl}
y : α
hy : y ∈ {x | x ∈ ↑tl}
⊢ x ≠ y → Commute x y
exact comm (List.mem_cons_of_mem _ hx) (List.mem_cons_of_mem _ hy)