[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
s : Finset α
⊢ Nodup ↑(sort r s)
[PROOFSTEP]
rw [sort_eq]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
s : Finset α
⊢ Nodup s.val
[PROOFSTEP]
exact s.2
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
s : Finset α
⊢ sort r s ~ toList s
[PROOFSTEP]
rw [← Multiset.coe_eq_coe]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
s : Finset α
⊢ ↑(sort r s) = ↑(toList s)
[PROOFSTEP]
simp only [coe_toList, sort_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : 0 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
⊢ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) 0 h = min' s H
[PROOFSTEP]
let l := s.sort (· ≤ ·)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : 0 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
l : List α := sort (fun x x_1 => x ≤ x_1) s
⊢ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) 0 h = min' s H
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : 0 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
l : List α := sort (fun x x_1 => x ≤ x_1) s
⊢ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) 0 h ≤ min' s H
[PROOFSTEP]
have : s.min' H ∈ l := (Finset.mem_sort (α := α) (· ≤ ·)).mpr (s.min'_mem H)
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : 0 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
l : List α := sort (fun x x_1 => x ≤ x_1) s
this : min' s H ∈ l
⊢ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) 0 h ≤ min' s H
[PROOFSTEP]
obtain ⟨i, hi⟩ : ∃ i, l.get i = s.min' H := List.mem_iff_get.1 this
[GOAL]
case a.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : 0 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
l : List α := sort (fun x x_1 => x ≤ x_1) s
this : min' s H ∈ l
i : Fin (List.length l)
hi : List.get l i = min' s H
⊢ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) 0 h ≤ min' s H
[PROOFSTEP]
rw [← hi]
[GOAL]
case a.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : 0 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
l : List α := sort (fun x x_1 => x ≤ x_1) s
this : min' s H ∈ l
i : Fin (List.length l)
hi : List.get l i = min' s H
⊢ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) 0 h ≤ List.get l i
[PROOFSTEP]
exact (s.sort_sorted (· ≤ ·)).rel_nthLe_of_le _ _ (Nat.zero_le i)
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : 0 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
l : List α := sort (fun x x_1 => x ≤ x_1) s
⊢ min' s H ≤ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) 0 h
[PROOFSTEP]
have : l.get ⟨0, h⟩ ∈ s := (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.get_mem l 0 h)
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : 0 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
l : List α := sort (fun x x_1 => x ≤ x_1) s
this : List.get l { val := 0, isLt := h } ∈ s
⊢ min' s H ≤ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) 0 h
[PROOFSTEP]
exact s.min'_le _ this
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : 0 < List.length (sort (fun x x_1 => x ≤ x_1) s)
⊢ 0 < card s
[PROOFSTEP]
rwa [length_sort] at h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : Finset.Nonempty s
⊢ 0 < List.length (sort (fun x x_1 => x ≤ x_1) s)
[PROOFSTEP]
rw [length_sort]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : Finset.Nonempty s
⊢ 0 < card s
[PROOFSTEP]
exact card_pos.2 h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : List.length (sort (fun x x_1 => x ≤ x_1) s) - 1 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
⊢ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) (List.length (sort (fun x x_1 => x ≤ x_1) s) - 1) h = max' s H
[PROOFSTEP]
let l := s.sort (· ≤ ·)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : List.length (sort (fun x x_1 => x ≤ x_1) s) - 1 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
l : List α := sort (fun x x_1 => x ≤ x_1) s
⊢ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) (List.length (sort (fun x x_1 => x ≤ x_1) s) - 1) h = max' s H
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : List.length (sort (fun x x_1 => x ≤ x_1) s) - 1 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
l : List α := sort (fun x x_1 => x ≤ x_1) s
⊢ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) (List.length (sort (fun x x_1 => x ≤ x_1) s) - 1) h ≤ max' s H
[PROOFSTEP]
have : l.get ⟨(s.sort (· ≤ ·)).length - 1, h⟩ ∈ s := (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.get_mem l _ h)
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : List.length (sort (fun x x_1 => x ≤ x_1) s) - 1 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
l : List α := sort (fun x x_1 => x ≤ x_1) s
this : List.get l { val := List.length (sort (fun x x_1 => x ≤ x_1) s) - 1, isLt := h } ∈ s
⊢ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) (List.length (sort (fun x x_1 => x ≤ x_1) s) - 1) h ≤ max' s H
[PROOFSTEP]
exact s.le_max' _ this
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : List.length (sort (fun x x_1 => x ≤ x_1) s) - 1 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
l : List α := sort (fun x x_1 => x ≤ x_1) s
⊢ max' s H ≤ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) (List.length (sort (fun x x_1 => x ≤ x_1) s) - 1) h
[PROOFSTEP]
have : s.max' H ∈ l := (Finset.mem_sort (α := α) (· ≤ ·)).mpr (s.max'_mem H)
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : List.length (sort (fun x x_1 => x ≤ x_1) s) - 1 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
l : List α := sort (fun x x_1 => x ≤ x_1) s
this : max' s H ∈ l
⊢ max' s H ≤ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) (List.length (sort (fun x x_1 => x ≤ x_1) s) - 1) h
[PROOFSTEP]
obtain ⟨i, hi⟩ : ∃ i, l.get i = s.max' H := List.mem_iff_get.1 this
[GOAL]
case a.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : List.length (sort (fun x x_1 => x ≤ x_1) s) - 1 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
l : List α := sort (fun x x_1 => x ≤ x_1) s
this : max' s H ∈ l
i : Fin (List.length l)
hi : List.get l i = max' s H
⊢ max' s H ≤ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) (List.length (sort (fun x x_1 => x ≤ x_1) s) - 1) h
[PROOFSTEP]
rw [← hi]
[GOAL]
case a.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : List.length (sort (fun x x_1 => x ≤ x_1) s) - 1 < List.length (sort (fun x x_1 => x ≤ x_1) s)
H : Finset.Nonempty s
l : List α := sort (fun x x_1 => x ≤ x_1) s
this : max' s H ∈ l
i : Fin (List.length l)
hi : List.get l i = max' s H
⊢ List.get l i ≤ List.nthLe (sort (fun x x_1 => x ≤ x_1) s) (List.length (sort (fun x x_1 => x ≤ x_1) s) - 1) h
[PROOFSTEP]
exact (s.sort_sorted (· ≤ ·)).rel_nthLe_of_le _ _ (Nat.le_pred_of_lt i.prop)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : List.length (sort (fun x x_1 => x ≤ x_1) s) - 1 < List.length (sort (fun x x_1 => x ≤ x_1) s)
⊢ Finset.Nonempty s
[PROOFSTEP]
rw [length_sort] at h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : card s - 1 < card s
⊢ Finset.Nonempty s
[PROOFSTEP]
exact card_pos.1 (lt_of_le_of_lt bot_le h)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : Finset.Nonempty s
⊢ List.length (sort (fun x x_1 => x ≤ x_1) s) - 1 < List.length (sort (fun x x_1 => x ≤ x_1) s)
[PROOFSTEP]
simpa using Nat.sub_lt (card_pos.mpr h) zero_lt_one
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
i : Fin k
⊢ ↑i < List.length (sort (fun x x_1 => x ≤ x_1) s)
[PROOFSTEP]
rw [length_sort, h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
i : Fin k
⊢ ↑i < k
[PROOFSTEP]
exact i.2
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
⊢ Set.range ↑(orderEmbOfFin s h) = ↑s
[PROOFSTEP]
simp only [orderEmbOfFin, Set.range_comp ((↑) : _ → α) (s.orderIsoOfFin h), RelEmbedding.coe_trans, Set.image_univ,
  Finset.orderEmbOfFin, RelIso.range_eq, OrderEmbedding.subtype_apply, OrderIso.coe_toOrderEmbedding, eq_self_iff_true,
  Subtype.range_coe_subtype, Finset.setOf_mem, Finset.coe_inj]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
hz : 0 < k
⊢ ↑(orderEmbOfFin s h) { val := 0, isLt := hz } = min' s (_ : Finset.Nonempty s)
[PROOFSTEP]
simp only [orderEmbOfFin_apply, Fin.val_mk, sorted_zero_eq_min']
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
hz : 0 < k
⊢ ↑(orderEmbOfFin s h) { val := k - 1, isLt := (_ : k - 1 < k) } = max' s (_ : Finset.Nonempty s)
[PROOFSTEP]
simp [orderEmbOfFin_apply, max'_eq_sorted_last, h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a : α
i : Fin 1
⊢ ↑(orderEmbOfFin {a} (_ : card {a} = 1)) i = a
[PROOFSTEP]
rw [Subsingleton.elim i ⟨0, zero_lt_one⟩, orderEmbOfFin_zero _ zero_lt_one, min'_singleton]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ f = ↑(orderEmbOfFin s h)
[PROOFSTEP]
apply Fin.strictMono_unique hmono (s.orderEmbOfFin h).strictMono
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ Set.range f = Set.range ↑(orderEmbOfFin s h)
[PROOFSTEP]
rw [range_orderEmbOfFin, ← Set.image_univ, ← coe_univ, ← coe_image, coe_inj]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ image f univ = s
[PROOFSTEP]
refine' eq_of_subset_of_card_le (fun x hx => _) _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
x : α
hx : x ∈ image f univ
⊢ x ∈ s
[PROOFSTEP]
rcases mem_image.1 hx with ⟨x, _, rfl⟩
[GOAL]
case refine'_1.intro.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
x : Fin k
left✝ : x ∈ univ
hx : f x ∈ image f univ
⊢ f x ∈ s
[PROOFSTEP]
exact hfs x
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : card s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ card s ≤ card (image f univ)
[PROOFSTEP]
rw [h, card_image_of_injective _ hmono.injective, card_univ, Fintype.card_fin]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
k l : ℕ
s : Finset α
i : Fin k
j : Fin l
h : card s = k
h' : card s = l
⊢ ↑(orderEmbOfFin s h) i = ↑(orderEmbOfFin s h') j ↔ ↑i = ↑j
[PROOFSTEP]
substs k l
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
i j : Fin (card s)
⊢ ↑(orderEmbOfFin s (_ : card s = card s)) i = ↑(orderEmbOfFin s (_ : card s = card s)) j ↔ ↑i = ↑j
[PROOFSTEP]
exact (s.orderEmbOfFin rfl).eq_iff_eq.trans Fin.ext_iff
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : k ≤ card s
a : Fin k
⊢ ↑(orderEmbOfCardLe s h) a ∈ s
[PROOFSTEP]
simp only [orderEmbOfCardLe, RelEmbedding.coe_trans, Finset.orderEmbOfFin_mem, Function.comp_apply]


[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
l : List α
comm : Set.Pairwise {x | x ∈ ↑l} fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ noncommFoldr f (↑l) comm b = List.foldr f b l
[PROOFSTEP]
simp only [noncommFoldr, coe_foldr, coe_attach, List.attach, Function.comp]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
l : List α
comm : Set.Pairwise {x | x ∈ ↑l} fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ List.foldr (fun x => f ↑x) b (List.pmap Subtype.mk l (_ : ∀ (x : α), x ∈ l → x ∈ l)) = List.foldr f b l
[PROOFSTEP]
rw [← List.foldr_map]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
l : List α
comm : Set.Pairwise {x | x ∈ ↑l} fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ List.foldr f b (List.map (fun x => ↑x) (List.pmap Subtype.mk l (_ : ∀ (x : α), x ∈ l → x ∈ l))) = List.foldr f b l
[PROOFSTEP]
simp [List.map_pmap, List.pmap_eq_map]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
s : Multiset α
a : α
h : Set.Pairwise {x | x ∈ a ::ₘ s} fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
h' : Set.Pairwise {x | x ∈ s} fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ noncommFoldr f (a ::ₘ s) h b = f a (noncommFoldr f s h' b)
[PROOFSTEP]
induction s using Quotient.inductionOn
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
a : α
b : β
a✝ : List α
h : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) a✝} fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
h' : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid α) a✝} fun x y => ∀ (b : β), f x (f y b) = f y (f x b)
⊢ noncommFoldr f (a ::ₘ Quotient.mk (List.isSetoid α) a✝) h b =
    f a (noncommFoldr f (Quotient.mk (List.isSetoid α) a✝) h' b)
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
s : Multiset α
h : LeftCommutative f
b : β
⊢ noncommFoldr f s
      (_ : ∀ (x : α), x ∈ {x | x ∈ s} → ∀ (y : α), y ∈ {x | x ∈ s} → x ≠ y → ∀ (b : β), f x (f y b) = f y (f x b)) b =
    foldr f h b s
[PROOFSTEP]
induction s using Quotient.inductionOn
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
h : LeftCommutative f
b : β
a✝ : List α
⊢ noncommFoldr f (Quotient.mk (List.isSetoid α) a✝)
      (_ :
        ∀ (x : α),
          x ∈ {x | x ∈ Quotient.mk (List.isSetoid α) a✝} →
            ∀ (y : α), y ∈ {x | x ∈ Quotient.mk (List.isSetoid α) a✝} → x ≠ y → ∀ (b : β), f x (f y b) = f y (f x b))
      b =
    foldr f h b (Quotient.mk (List.isSetoid α) a✝)
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
assoc : IsAssociative α op
s : Multiset α
comm : Set.Pairwise {x | x ∈ s} fun x y => op x y = op y x
x : α
hx : x ∈ {x | x ∈ s}
y : α
hy : y ∈ {x | x ∈ s}
h : x ≠ y
b : α
⊢ op x (op y b) = op y (op x b)
[PROOFSTEP]
rw [← assoc.assoc, comm hx hy h, assoc.assoc]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
assoc : IsAssociative α op
l : List α
comm : Set.Pairwise {x | x ∈ ↑l} fun x y => op x y = op y x
a : α
⊢ noncommFold op (↑l) comm a = List.foldr op a l
[PROOFSTEP]
simp [noncommFold]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
assoc : IsAssociative α op
s : Multiset α
a : α
h : Set.Pairwise {x | x ∈ a ::ₘ s} fun x y => op x y = op y x
h' : Set.Pairwise {x | x ∈ s} fun x y => op x y = op y x
x : α
⊢ noncommFold op (a ::ₘ s) h x = op a (noncommFold op s h' x)
[PROOFSTEP]
induction s using Quotient.inductionOn
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
assoc : IsAssociative α op
a x : α
a✝ : List α
h : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) a✝} fun x y => op x y = op y x
h' : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid α) a✝} fun x y => op x y = op y x
⊢ noncommFold op (a ::ₘ Quotient.mk (List.isSetoid α) a✝) h x =
    op a (noncommFold op (Quotient.mk (List.isSetoid α) a✝) h' x)
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
assoc : IsAssociative α op
s : Multiset α
inst✝ : IsCommutative α op
a : α
⊢ noncommFold op s (_ : ∀ (x : α), x ∈ {x | x ∈ s} → ∀ (y : α), y ∈ {x | x ∈ s} → x ≠ y → op x y = op y x) a =
    fold op a s
[PROOFSTEP]
induction s using Quotient.inductionOn
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
assoc : IsAssociative α op
inst✝ : IsCommutative α op
a : α
a✝ : List α
⊢ noncommFold op (Quotient.mk (List.isSetoid α) a✝)
      (_ :
        ∀ (x : α),
          x ∈ {x | x ∈ Quotient.mk (List.isSetoid α) a✝} →
            ∀ (y : α), y ∈ {x | x ∈ Quotient.mk (List.isSetoid α) a✝} → x ≠ y → op x y = op y x)
      a =
    fold op a (Quotient.mk (List.isSetoid α) a✝)
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
l : List α
comm : Set.Pairwise {x | x ∈ ↑l} Commute
⊢ noncommProd (↑l) comm = List.prod l
[PROOFSTEP]
rw [noncommProd]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
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
[PROOFSTEP]
simp only [noncommFold_coe]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
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
[PROOFSTEP]
induction' l with hd tl hl
[GOAL]
case nil
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
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 []
[PROOFSTEP]
simp
[GOAL]
case cons
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
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)
[PROOFSTEP]
rw [List.prod_cons, List.foldr, hl]
[GOAL]
case cons
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
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
[PROOFSTEP]
intro x hx y hy
[GOAL]
case cons
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
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
[PROOFSTEP]
exact comm (List.mem_cons_of_mem _ hx) (List.mem_cons_of_mem _ hy)
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s : Multiset α
a : α
comm : Set.Pairwise {x | x ∈ a ::ₘ s} Commute
⊢ noncommProd (a ::ₘ s) comm = a * noncommProd s (_ : Set.Pairwise {x | x ∈ s} Commute)
[PROOFSTEP]
induction s using Quotient.inductionOn
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
a : α
a✝ : List α
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) a✝} Commute
⊢ noncommProd (a ::ₘ Quotient.mk (List.isSetoid α) a✝) comm =
    a *
      noncommProd (Quotient.mk (List.isSetoid α) a✝)
        (_ : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid α) a✝} Commute)
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s : Multiset α
a : α
comm : Set.Pairwise {x | x ∈ a ::ₘ s} Commute
⊢ noncommProd (a ::ₘ s) comm = noncommProd s (_ : Set.Pairwise {x | x ∈ s} Commute) * a
[PROOFSTEP]
induction' s using Quotient.inductionOn with s
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
⊢ noncommProd (a ::ₘ Quotient.mk (List.isSetoid α) s) comm =
    noncommProd (Quotient.mk (List.isSetoid α) s) (_ : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid α) s} Commute) *
      a
[PROOFSTEP]
simp only [quot_mk_to_coe, cons_coe, noncommProd_coe, List.prod_cons]
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
⊢ a * List.prod s = List.prod s * a
[PROOFSTEP]
induction' s with hd tl IH
[GOAL]
case h.nil
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) []} Commute
⊢ a * List.prod [] = List.prod [] * a
[PROOFSTEP]
simp
[GOAL]
case h.cons
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
⊢ a * List.prod (hd :: tl) = List.prod (hd :: tl) * a
[PROOFSTEP]
rw [List.prod_cons, mul_assoc, ← IH, ← mul_assoc, ← mul_assoc]
[GOAL]
case h.cons
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
⊢ a * hd * List.prod tl = hd * a * List.prod tl
[PROOFSTEP]
congr 1
[GOAL]
case h.cons.e_a
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
⊢ a * hd = hd * a
[PROOFSTEP]
apply comm.of_refl
[GOAL]
case h.cons.e_a.a
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
⊢ a ∈ {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)}
[PROOFSTEP]
simp
[GOAL]
case h.cons.e_a.a
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
⊢ hd ∈ {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)}
[PROOFSTEP]
simp
[GOAL]
case h.cons
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
⊢ Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute
[PROOFSTEP]
intro x hx y hy
[GOAL]
case h.cons
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
x : α
hx : x ∈ {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl}
y : α
hy : y ∈ {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl}
⊢ x ≠ y → Commute x y
[PROOFSTEP]
simp only [quot_mk_to_coe, List.mem_cons, mem_coe, cons_coe] at hx hy
[GOAL]
case h.cons
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
hy : y ∈ {x | x = a ∨ x ∈ tl}
⊢ x ≠ y → Commute x y
[PROOFSTEP]
apply comm
[GOAL]
case h.cons.a
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
hy : y ∈ {x | x = a ∨ x ∈ tl}
⊢ x ∈ {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)}
[PROOFSTEP]
cases hx
[GOAL]
case h.cons.a.inl
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
x y : α
hy : y ∈ {x | x = a ∨ x ∈ tl}
h✝ : x = a
⊢ x ∈ {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)}
[PROOFSTEP]
simp [*]
[GOAL]
case h.cons.a.inr
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
x y : α
hy : y ∈ {x | x = a ∨ x ∈ tl}
h✝ : x ∈ tl
⊢ x ∈ {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)}
[PROOFSTEP]
simp [*]
[GOAL]
case h.cons.a
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
hy : y ∈ {x | x = a ∨ x ∈ tl}
⊢ y ∈ {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)}
[PROOFSTEP]
cases hy
[GOAL]
case h.cons.a.inl
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
h✝ : y = a
⊢ y ∈ {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)}
[PROOFSTEP]
simp [*]
[GOAL]
case h.cons.a.inr
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
h✝ : y ∈ tl
⊢ y ∈ {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)}
[PROOFSTEP]
simp [*]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s t : Multiset α
comm : Set.Pairwise {x | x ∈ s + t} Commute
⊢ noncommProd (s + t) comm =
    noncommProd s (_ : Set.Pairwise {x | x ∈ s} Commute) * noncommProd t (_ : Set.Pairwise {x | x ∈ t} Commute)
[PROOFSTEP]
rcases s with ⟨⟩
[GOAL]
case mk
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s t : Multiset α
a✝ : List α
comm : Set.Pairwise {x | x ∈ Quot.mk Setoid.r a✝ + t} Commute
⊢ noncommProd (Quot.mk Setoid.r a✝ + t) comm =
    noncommProd (Quot.mk Setoid.r a✝) (_ : Set.Pairwise {x | x ∈ Quot.mk Setoid.r a✝} Commute) *
      noncommProd t (_ : Set.Pairwise {x | x ∈ t} Commute)
[PROOFSTEP]
rcases t with ⟨⟩
[GOAL]
case mk.mk
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s t : Multiset α
a✝¹ a✝ : List α
comm : Set.Pairwise {x | x ∈ Quot.mk Setoid.r a✝¹ + Quot.mk Setoid.r a✝} Commute
⊢ noncommProd (Quot.mk Setoid.r a✝¹ + Quot.mk Setoid.r a✝) comm =
    noncommProd (Quot.mk Setoid.r a✝¹) (_ : Set.Pairwise {x | x ∈ Quot.mk Setoid.r a✝¹} Commute) *
      noncommProd (Quot.mk Setoid.r a✝) (_ : Set.Pairwise {x | x ∈ Quot.mk Setoid.r a✝} Commute)
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
s : Multiset α
comm : Set.Pairwise {x | x ∈ s} Commute
f : F
⊢ Set.Pairwise {x | x ∈ map (↑f) s} Commute
[PROOFSTEP]
simp only [Multiset.mem_map]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
s : Multiset α
comm : Set.Pairwise {x | x ∈ s} Commute
f : F
⊢ Set.Pairwise {x | ∃ a, a ∈ s ∧ ↑f a = x} Commute
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ _
[GOAL]
case intro.intro.intro.intro
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
s : Multiset α
comm : Set.Pairwise {x | x ∈ s} Commute
f : F
x : α
hx : x ∈ s
y : α
hy : y ∈ s
a✝ : ↑f x ≠ ↑f y
⊢ Commute (↑f x) (↑f y)
[PROOFSTEP]
exact (comm.of_refl hx hy).map f
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
s : Multiset α
comm : Set.Pairwise {x | x ∈ s} Commute
f : F
⊢ ↑f (noncommProd s comm) = noncommProd (map (↑f) s) (_ : Set.Pairwise {x | x ∈ map (↑f) s} Commute)
[PROOFSTEP]
induction s using Quotient.inductionOn
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
f : F
a✝ : List α
comm : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid α) a✝} Commute
⊢ ↑f (noncommProd (Quotient.mk (List.isSetoid α) a✝) comm) =
    noncommProd (map (↑f) (Quotient.mk (List.isSetoid α) a✝))
      (_ : Set.Pairwise {x | x ∈ map (↑f) (Quotient.mk (List.isSetoid α) a✝)} Commute)
[PROOFSTEP]
simpa using map_list_prod f _
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
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
[PROOFSTEP]
induction s using Quotient.inductionOn
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
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✝)
[PROOFSTEP]
simp only [quot_mk_to_coe, noncommProd_coe, coe_card, mem_coe] at *
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
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✝
[PROOFSTEP]
exact List.prod_eq_pow_card _ m h
[GOAL]
F : Type u_1
ι : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
f : α✝ → β → β
op : α✝ → α✝ → α✝
inst✝² : Monoid α✝
inst✝¹ : Monoid β
α : Type u_6
inst✝ : CommMonoid α
s : Multiset α
⊢ noncommProd s (_ : ∀ (x : α), x ∈ {x | x ∈ s} → ∀ (x_2 : α), x_2 ∈ {x | x ∈ s} → x ≠ x_2 → Commute x x_2) = prod s
[PROOFSTEP]
induction s using Quotient.inductionOn
[GOAL]
case h
F : Type u_1
ι : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
f : α✝ → β → β
op : α✝ → α✝ → α✝
inst✝² : Monoid α✝
inst✝¹ : Monoid β
α : Type u_6
inst✝ : CommMonoid α
a✝ : List α
⊢ noncommProd (Quotient.mk (List.isSetoid α) a✝)
      (_ :
        ∀ (x : α),
          x ∈ {x | x ∈ Quotient.mk (List.isSetoid α) a✝} →
            ∀ (x_2 : α), x_2 ∈ {x | x ∈ Quotient.mk (List.isSetoid α) a✝} → x ≠ x_2 → Commute x x_2) =
    prod (Quotient.mk (List.isSetoid α) a✝)
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s : Multiset α
comm : Set.Pairwise {x | x ∈ s} Commute
y : α
h : ∀ (x : α), x ∈ s → Commute y x
⊢ Commute y (noncommProd s comm)
[PROOFSTEP]
induction s using Quotient.inductionOn
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
y : α
a✝ : List α
comm : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid α) a✝} Commute
h : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) a✝ → Commute y x
⊢ Commute y (noncommProd (Quotient.mk (List.isSetoid α) a✝) comm)
[PROOFSTEP]
simp only [quot_mk_to_coe, noncommProd_coe]
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
y : α
a✝ : List α
comm : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid α) a✝} Commute
h : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) a✝ → Commute y x
⊢ Commute y (List.prod a✝)
[PROOFSTEP]
exact Commute.list_prod_right _ _ h
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
⊢ Set.Pairwise {x | x ∈ Multiset.map f s.val} Commute
[PROOFSTEP]
simp_rw [Multiset.mem_map]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
⊢ Set.Pairwise {x | ∃ a, a ∈ s.val ∧ f a = x} Commute
[PROOFSTEP]
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ _
[GOAL]
case intro.intro.intro.intro
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
a : α
ha : a ∈ s.val
b : α
hb : b ∈ s.val
a✝ : f a ≠ f b
⊢ Commute (f a) (f b)
[PROOFSTEP]
exact comm.of_refl ha hb
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ (x : α), x ∈ s₂ → f x = g x
comm : Set.Pairwise ↑s₁ fun a b => Commute (f a) (f b)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ (fun a b => Commute (g a) (g b)) x y
[PROOFSTEP]
dsimp only
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ (x : α), x ∈ s₂ → f x = g x
comm : Set.Pairwise ↑s₁ fun a b => Commute (f a) (f b)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ Commute (g x) (g y)
[PROOFSTEP]
rw [← h₂ _ hx, ← h₂ _ hy]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ (x : α), x ∈ s₂ → f x = g x
comm : Set.Pairwise ↑s₁ fun a b => Commute (f a) (f b)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ Commute (f x) (f y)
[PROOFSTEP]
subst h₁
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ : Finset α
f g : α → β
comm : Set.Pairwise ↑s₁ fun a b => Commute (f a) (f b)
x y : α
h : x ≠ y
h₂ : ∀ (x : α), x ∈ s₁ → f x = g x
hx : x ∈ ↑s₁
hy : y ∈ ↑s₁
⊢ Commute (f x) (f y)
[PROOFSTEP]
exact comm hx hy h
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ (x : α), x ∈ s₂ → f x = g x
comm : Set.Pairwise ↑s₁ fun a b => Commute (f a) (f b)
⊢ noncommProd s₁ f comm =
    noncommProd s₂ g (_ : ∀ (x : α), x ∈ ↑s₂ → ∀ (y : α), y ∈ ↑s₂ → x ≠ y → (fun a b => Commute (g a) (g b)) x y)
[PROOFSTEP]
simp_rw [noncommProd, Multiset.map_congr (congr_arg _ h₁) h₂]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
l : List α
f : α → β
comm : Set.Pairwise ↑(List.toFinset l) fun a b => Commute (f a) (f b)
hl : List.Nodup l
⊢ noncommProd (List.toFinset l) f comm = List.prod (List.map f l)
[PROOFSTEP]
rw [← List.dedup_eq_self] at hl
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
l : List α
f : α → β
comm : Set.Pairwise ↑(List.toFinset l) fun a b => Commute (f a) (f b)
hl✝ : List.Nodup l
hl : List.dedup l = l
⊢ noncommProd (List.toFinset l) f comm = List.prod (List.map f l)
[PROOFSTEP]
simp [noncommProd, hl]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
s : Finset α
a : α
f : α → β
comm : Set.Pairwise ↑(insert a s) fun a b => Commute (f a) (f b)
ha : ¬a ∈ s
⊢ Set.Pairwise {x | x ∈ f a ::ₘ Multiset.map f s.val} Commute
[PROOFSTEP]
convert noncommProd_lemma _ f comm using 3
[GOAL]
case h.e'_2.h.e'_2.h.a
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
s : Finset α
a : α
f : α → β
comm : Set.Pairwise ↑(insert a s) fun a b => Commute (f a) (f b)
ha : ¬a ∈ s
x✝ : β
⊢ x✝ ∈ f a ::ₘ Multiset.map f s.val ↔ x✝ ∈ Multiset.map f (insert a s).val
[PROOFSTEP]
simp [@eq_comm _ (f a)]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
s : Finset α
a : α
f : α → β
comm : Set.Pairwise ↑(insert a s) fun a b => Commute (f a) (f b)
ha : ¬a ∈ s
⊢ Multiset.noncommProd (Multiset.map f (insert a s).val)
      (_ : Set.Pairwise {x | x ∈ Multiset.map f (insert a s).val} Commute) =
    Multiset.noncommProd (f a ::ₘ Multiset.map f s.val)
      (_ : Set.Pairwise {x | x ∈ f a ::ₘ Multiset.map f s.val} Commute)
[PROOFSTEP]
{ congr
  rw [insert_val_of_not_mem ha, Multiset.map_cons]
}
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
s : Finset α
a : α
f : α → β
comm : Set.Pairwise ↑(insert a s) fun a b => Commute (f a) (f b)
ha : ¬a ∈ s
⊢ Multiset.noncommProd (Multiset.map f (insert a s).val)
      (_ : Set.Pairwise {x | x ∈ Multiset.map f (insert a s).val} Commute) =
    Multiset.noncommProd (f a ::ₘ Multiset.map f s.val)
      (_ : Set.Pairwise {x | x ∈ f a ::ₘ Multiset.map f s.val} Commute)
[PROOFSTEP]
congr
[GOAL]
case e_s
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
s : Finset α
a : α
f : α → β
comm : Set.Pairwise ↑(insert a s) fun a b => Commute (f a) (f b)
ha : ¬a ∈ s
⊢ Multiset.map f (insert a s).val = f a ::ₘ Multiset.map f s.val
[PROOFSTEP]
rw [insert_val_of_not_mem ha, Multiset.map_cons]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
s : Finset α
a : α
f : α → β
comm : Set.Pairwise ↑(insert a s) fun a b => Commute (f a) (f b)
ha : ¬a ∈ s
⊢ Multiset.noncommProd (f a ::ₘ Multiset.map f s.val)
      (_ : Set.Pairwise {x | x ∈ f a ::ₘ Multiset.map f s.val} Commute) =
    f a * noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b))
[PROOFSTEP]
rw [Multiset.noncommProd_cons, noncommProd]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
s : Finset α
a : α
f : α → β
comm : Set.Pairwise ↑(insert a s) fun a b => Commute (f a) (f b)
ha : ¬a ∈ s
⊢ Set.Pairwise {x | x ∈ f a ::ₘ Multiset.map f s.val} Commute
[PROOFSTEP]
convert noncommProd_lemma _ f comm using 3
[GOAL]
case h.e'_2.h.e'_2.h.a
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
s : Finset α
a : α
f : α → β
comm : Set.Pairwise ↑(insert a s) fun a b => Commute (f a) (f b)
ha : ¬a ∈ s
x✝ : β
⊢ x✝ ∈ f a ::ₘ Multiset.map f s.val ↔ x✝ ∈ Multiset.map f (insert a s).val
[PROOFSTEP]
simp [@eq_comm _ (f a)]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
s : Finset α
a : α
f : α → β
comm : Set.Pairwise ↑(insert a s) fun a b => Commute (f a) (f b)
ha : ¬a ∈ s
⊢ Multiset.noncommProd (Multiset.map f (insert a s).val)
      (_ : Set.Pairwise {x | x ∈ Multiset.map f (insert a s).val} Commute) =
    Multiset.noncommProd (f a ::ₘ Multiset.map f s.val)
      (_ : Set.Pairwise {x | x ∈ f a ::ₘ Multiset.map f s.val} Commute)
[PROOFSTEP]
{ congr
  rw [insert_val_of_not_mem ha, Multiset.map_cons]
}
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
s : Finset α
a : α
f : α → β
comm : Set.Pairwise ↑(insert a s) fun a b => Commute (f a) (f b)
ha : ¬a ∈ s
⊢ Multiset.noncommProd (Multiset.map f (insert a s).val)
      (_ : Set.Pairwise {x | x ∈ Multiset.map f (insert a s).val} Commute) =
    Multiset.noncommProd (f a ::ₘ Multiset.map f s.val)
      (_ : Set.Pairwise {x | x ∈ f a ::ₘ Multiset.map f s.val} Commute)
[PROOFSTEP]
congr
[GOAL]
case e_s
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
s : Finset α
a : α
f : α → β
comm : Set.Pairwise ↑(insert a s) fun a b => Commute (f a) (f b)
ha : ¬a ∈ s
⊢ Multiset.map f (insert a s).val = f a ::ₘ Multiset.map f s.val
[PROOFSTEP]
rw [insert_val_of_not_mem ha, Multiset.map_cons]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
s : Finset α
a : α
f : α → β
comm : Set.Pairwise ↑(insert a s) fun a b => Commute (f a) (f b)
ha : ¬a ∈ s
⊢ Multiset.noncommProd (f a ::ₘ Multiset.map f s.val)
      (_ : Set.Pairwise {x | x ∈ f a ::ₘ Multiset.map f s.val} Commute) =
    noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) * f a
[PROOFSTEP]
rw [Multiset.noncommProd_cons', noncommProd]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
a : α
f : α → β
⊢ Set.Pairwise ↑{a} fun a b => Commute (f a) (f b)
[PROOFSTEP]
norm_cast
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
a : α
f : α → β
⊢ Set.Pairwise {a} fun a b => Commute (f a) (f b)
[PROOFSTEP]
exact Set.pairwise_singleton _ _
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : MonoidHomClass F β γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
g : F
⊢ ↑g (noncommProd s f comm) =
    noncommProd s (fun i => ↑g (f i))
      (_ : ∀ (x : α), x ∈ ↑s → ∀ (y : α), y ∈ ↑s → x ≠ y → Commute (↑g (f x)) (↑g (f y)))
[PROOFSTEP]
simp [noncommProd, Multiset.noncommProd_map]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
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
[PROOFSTEP]
rw [noncommProd, Multiset.noncommProd_eq_pow_card _ _ m]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
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_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
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
[PROOFSTEP]
simp only [Finset.card_def, Multiset.card_map]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
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
[PROOFSTEP]
simpa using h
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
y : β
h : ∀ (x : α), x ∈ s → Commute y (f x)
⊢ Commute y (noncommProd s f comm)
[PROOFSTEP]
apply Multiset.noncommProd_commute
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
y : β
h : ∀ (x : α), x ∈ s → Commute y (f x)
⊢ ∀ (x : β), x ∈ Multiset.map f s.val → Commute y x
[PROOFSTEP]
intro y
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
y✝ : β
h : ∀ (x : α), x ∈ s → Commute y✝ (f x)
y : β
⊢ y ∈ Multiset.map f s.val → Commute y✝ y
[PROOFSTEP]
rw [Multiset.mem_map]
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
y✝ : β
h : ∀ (x : α), x ∈ s → Commute y✝ (f x)
y : β
⊢ (∃ a, a ∈ s.val ∧ f a = y) → Commute y✝ y
[PROOFSTEP]
rintro ⟨x, ⟨hx, rfl⟩⟩
[GOAL]
case h.intro.intro
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
y : β
h : ∀ (x : α), x ∈ s → Commute y (f x)
x : α
hx : x ∈ s.val
⊢ Commute y (f x)
[PROOFSTEP]
exact h x hx
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β✝ : Type u_4
γ : Type u_5
f✝ : α → β✝ → β✝
op : α → α → α
inst✝² : Monoid β✝
inst✝¹ : Monoid γ
β : Type u_6
inst✝ : CommMonoid β
s : Finset α
f : α → β
⊢ noncommProd s f (_ : ∀ (x : α), x ∈ ↑s → ∀ (x_2 : α), x_2 ∈ ↑s → x ≠ x_2 → Commute (f x) (f x_2)) = Finset.prod s f
[PROOFSTEP]
classical
induction' s using Finset.induction_on with a s ha IH
· simp
· simp [ha, IH]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β✝ : Type u_4
γ : Type u_5
f✝ : α → β✝ → β✝
op : α → α → α
inst✝² : Monoid β✝
inst✝¹ : Monoid γ
β : Type u_6
inst✝ : CommMonoid β
s : Finset α
f : α → β
⊢ noncommProd s f (_ : ∀ (x : α), x ∈ ↑s → ∀ (x_2 : α), x_2 ∈ ↑s → x ≠ x_2 → Commute (f x) (f x_2)) = Finset.prod s f
[PROOFSTEP]
induction' s using Finset.induction_on with a s ha IH
[GOAL]
case empty
F : Type u_1
ι : Type u_2
α : Type u_3
β✝ : Type u_4
γ : Type u_5
f✝ : α → β✝ → β✝
op : α → α → α
inst✝² : Monoid β✝
inst✝¹ : Monoid γ
β : Type u_6
inst✝ : CommMonoid β
f : α → β
⊢ noncommProd ∅ f (_ : ∀ (x : α), x ∈ ↑∅ → ∀ (x_2 : α), x_2 ∈ ↑∅ → x ≠ x_2 → Commute (f x) (f x_2)) = Finset.prod ∅ f
[PROOFSTEP]
simp
[GOAL]
case insert
F : Type u_1
ι : Type u_2
α : Type u_3
β✝ : Type u_4
γ : Type u_5
f✝ : α → β✝ → β✝
op : α → α → α
inst✝² : Monoid β✝
inst✝¹ : Monoid γ
β : Type u_6
inst✝ : CommMonoid β
f : α → β
a : α
s : Finset α
ha : ¬a ∈ s
IH : noncommProd s f (_ : ∀ (x : α), x ∈ ↑s → ∀ (x_2 : α), x_2 ∈ ↑s → x ≠ x_2 → Commute (f x) (f x_2)) = Finset.prod s f
⊢ noncommProd (insert a s) f
      (_ : ∀ (x : α), x ∈ ↑(insert a s) → ∀ (x_2 : α), x_2 ∈ ↑(insert a s) → x ≠ x_2 → Commute (f x) (f x_2)) =
    Finset.prod (insert a s) f
[PROOFSTEP]
simp [ha, IH]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
f : α → β
comm : Set.Pairwise {x | x ∈ s ∪ t} fun a b => Commute (f a) (f b)
⊢ noncommProd (s ∪ t) f comm =
    noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) *
      noncommProd t f (_ : Set.Pairwise ↑t fun a b => Commute (f a) (f b))
[PROOFSTEP]
obtain ⟨sl, sl', rfl⟩ := exists_list_nodup_eq s
[GOAL]
case intro.intro
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
t : Finset α
f : α → β
sl : List α
sl' : List.Nodup sl
h : Disjoint (List.toFinset sl) t
comm : Set.Pairwise {x | x ∈ List.toFinset sl ∪ t} fun a b => Commute (f a) (f b)
⊢ noncommProd (List.toFinset sl ∪ t) f comm =
    noncommProd (List.toFinset sl) f (_ : Set.Pairwise ↑(List.toFinset sl) fun a b => Commute (f a) (f b)) *
      noncommProd t f (_ : Set.Pairwise ↑t fun a b => Commute (f a) (f b))
[PROOFSTEP]
obtain ⟨tl, tl', rfl⟩ := exists_list_nodup_eq t
[GOAL]
case intro.intro.intro.intro
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
f : α → β
sl : List α
sl' : List.Nodup sl
tl : List α
tl' : List.Nodup tl
h : Disjoint (List.toFinset sl) (List.toFinset tl)
comm : Set.Pairwise {x | x ∈ List.toFinset sl ∪ List.toFinset tl} fun a b => Commute (f a) (f b)
⊢ noncommProd (List.toFinset sl ∪ List.toFinset tl) f comm =
    noncommProd (List.toFinset sl) f (_ : Set.Pairwise ↑(List.toFinset sl) fun a b => Commute (f a) (f b)) *
      noncommProd (List.toFinset tl) f (_ : Set.Pairwise ↑(List.toFinset tl) fun a b => Commute (f a) (f b))
[PROOFSTEP]
rw [List.disjoint_toFinset_iff_disjoint] at h
[GOAL]
case intro.intro.intro.intro
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
f : α → β
sl : List α
sl' : List.Nodup sl
tl : List α
tl' : List.Nodup tl
h : List.Disjoint sl tl
comm : Set.Pairwise {x | x ∈ List.toFinset sl ∪ List.toFinset tl} fun a b => Commute (f a) (f b)
⊢ noncommProd (List.toFinset sl ∪ List.toFinset tl) f comm =
    noncommProd (List.toFinset sl) f (_ : Set.Pairwise ↑(List.toFinset sl) fun a b => Commute (f a) (f b)) *
      noncommProd (List.toFinset tl) f (_ : Set.Pairwise ↑(List.toFinset tl) fun a b => Commute (f a) (f b))
[PROOFSTEP]
calc
  noncommProd (List.toFinset sl ∪ List.toFinset tl) f comm =
      noncommProd ⟨↑(sl ++ tl), Multiset.coe_nodup.2 (sl'.append tl' h)⟩ f (by convert comm; simp [Set.ext_iff]) :=
    noncommProd_congr (by ext; simp) (by simp) _
  _ =
      noncommProd (List.toFinset sl) f (comm.mono <| coe_subset.2 <| subset_union_left _ _) *
        noncommProd (List.toFinset tl) f (comm.mono <| coe_subset.2 <| subset_union_right _ _) :=
    by simp [noncommProd, List.dedup_eq_self.2 sl', List.dedup_eq_self.2 tl', h]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
f : α → β
sl : List α
sl' : List.Nodup sl
tl : List α
tl' : List.Nodup tl
h : List.Disjoint sl tl
comm : Set.Pairwise {x | x ∈ List.toFinset sl ∪ List.toFinset tl} fun a b => Commute (f a) (f b)
⊢ Set.Pairwise ↑{ val := ↑(sl ++ tl), nodup := (_ : Multiset.Nodup ↑(sl ++ tl)) } fun a b => Commute (f a) (f b)
[PROOFSTEP]
convert comm
[GOAL]
case h.e'_2
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
f : α → β
sl : List α
sl' : List.Nodup sl
tl : List α
tl' : List.Nodup tl
h : List.Disjoint sl tl
comm : Set.Pairwise {x | x ∈ List.toFinset sl ∪ List.toFinset tl} fun a b => Commute (f a) (f b)
⊢ ↑{ val := ↑(sl ++ tl), nodup := (_ : Multiset.Nodup ↑(sl ++ tl)) } = {x | x ∈ List.toFinset sl ∪ List.toFinset tl}
[PROOFSTEP]
simp [Set.ext_iff]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
f : α → β
sl : List α
sl' : List.Nodup sl
tl : List α
tl' : List.Nodup tl
h : List.Disjoint sl tl
comm : Set.Pairwise {x | x ∈ List.toFinset sl ∪ List.toFinset tl} fun a b => Commute (f a) (f b)
⊢ List.toFinset sl ∪ List.toFinset tl = { val := ↑(sl ++ tl), nodup := (_ : Multiset.Nodup ↑(sl ++ tl)) }
[PROOFSTEP]
ext
[GOAL]
case a
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
f : α → β
sl : List α
sl' : List.Nodup sl
tl : List α
tl' : List.Nodup tl
h : List.Disjoint sl tl
comm : Set.Pairwise {x | x ∈ List.toFinset sl ∪ List.toFinset tl} fun a b => Commute (f a) (f b)
a✝ : α
⊢ a✝ ∈ List.toFinset sl ∪ List.toFinset tl ↔ a✝ ∈ { val := ↑(sl ++ tl), nodup := (_ : Multiset.Nodup ↑(sl ++ tl)) }
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
f : α → β
sl : List α
sl' : List.Nodup sl
tl : List α
tl' : List.Nodup tl
h : List.Disjoint sl tl
comm : Set.Pairwise {x | x ∈ List.toFinset sl ∪ List.toFinset tl} fun a b => Commute (f a) (f b)
⊢ ∀ (x : α), x ∈ { val := ↑(sl ++ tl), nodup := (_ : Multiset.Nodup ↑(sl ++ tl)) } → f x = f x
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
f : α → β
sl : List α
sl' : List.Nodup sl
tl : List α
tl' : List.Nodup tl
h : List.Disjoint sl tl
comm : Set.Pairwise {x | x ∈ List.toFinset sl ∪ List.toFinset tl} fun a b => Commute (f a) (f b)
⊢ noncommProd { val := ↑(sl ++ tl), nodup := (_ : Multiset.Nodup ↑(sl ++ tl)) } f
      (_ :
        Set.Pairwise ↑{ val := ↑(sl ++ tl), nodup := (_ : Multiset.Nodup ↑(sl ++ tl)) } fun a b =>
          Commute (f a) (f b)) =
    noncommProd (List.toFinset sl) f (_ : Set.Pairwise ↑(List.toFinset sl) fun a b => Commute (f a) (f b)) *
      noncommProd (List.toFinset tl) f (_ : Set.Pairwise ↑(List.toFinset tl) fun a b => Commute (f a) (f b))
[PROOFSTEP]
simp [noncommProd, List.dedup_eq_self.2 sl', List.dedup_eq_self.2 tl', h]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f g : α → β
comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)
⊢ Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)
[PROOFSTEP]
intro x hx y hy h
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f g : α → β
comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute ((f * g) x) ((f * g) y)
[PROOFSTEP]
apply Commute.mul_left
[GOAL]
case hac
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f g : α → β
comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (f x) ((f * g) y)
[PROOFSTEP]
apply Commute.mul_right
[GOAL]
case hbc
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f g : α → β
comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) ((f * g) y)
[PROOFSTEP]
apply Commute.mul_right
[GOAL]
case hac.hab
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f g : α → β
comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (f x) (f y)
[PROOFSTEP]
exact comm_ff.of_refl hx hy
[GOAL]
case hac.hac
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f g : α → β
comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (f x) (g y)
[PROOFSTEP]
exact (comm_gf hy hx h.symm).symm
[GOAL]
case hbc.hab
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f g : α → β
comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) (f y)
[PROOFSTEP]
exact comm_gf hx hy h
[GOAL]
case hbc.hac
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f g : α → β
comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) (g y)
[PROOFSTEP]
exact comm_gg.of_refl hx hy
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f g : α → β
comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)
⊢ noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f comm_ff * noncommProd s g comm_gg
[PROOFSTEP]
classical
induction' s using Finset.induction_on with x s hnmem ih
· simp
simp only [Finset.noncommProd_insert_of_not_mem _ _ _ _ hnmem]
specialize
  ih (comm_ff.mono fun _ => mem_insert_of_mem) (comm_gg.mono fun _ => mem_insert_of_mem)
    (comm_gf.mono fun _ => mem_insert_of_mem)
rw [ih, Pi.mul_apply]
simp only [mul_assoc]
congr 1
simp only [← mul_assoc]
congr 1
refine' noncommProd_commute _ _ _ _ fun y hy => _
exact comm_gf (mem_insert_self x s) (mem_insert_of_mem hy) (ne_of_mem_of_not_mem hy hnmem).symm
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f g : α → β
comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)
⊢ noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f comm_ff * noncommProd s g comm_gg
[PROOFSTEP]
induction' s using Finset.induction_on with x s hnmem ih
[GOAL]
case empty
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f g : α → β
comm_ff✝ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)
comm_gg✝ : Set.Pairwise ↑s fun x y => Commute (g x) (g y)
comm_gf✝ : Set.Pairwise ↑s fun x y => Commute (g x) (f y)
comm_ff : Set.Pairwise ↑∅ fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑∅ fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑∅ fun x y => Commute (g x) (f y)
⊢ noncommProd ∅ (f * g) (_ : Set.Pairwise ↑∅ fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd ∅ f comm_ff * noncommProd ∅ g comm_gg
[PROOFSTEP]
simp
[GOAL]
case insert
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s✝ : Finset α
f g : α → β
comm_ff✝ : Set.Pairwise ↑s✝ fun x y => Commute (f x) (f y)
comm_gg✝ : Set.Pairwise ↑s✝ fun x y => Commute (g x) (g y)
comm_gf✝ : Set.Pairwise ↑s✝ fun x y => Commute (g x) (f y)
x : α
s : Finset α
hnmem : ¬x ∈ s
ih :
  ∀ (comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y))
    (comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
    (comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)),
    noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
      noncommProd s f comm_ff * noncommProd s g comm_gg
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
⊢ noncommProd (insert x s) (f * g) (_ : Set.Pairwise ↑(insert x s) fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd (insert x s) f comm_ff * noncommProd (insert x s) g comm_gg
[PROOFSTEP]
simp only [Finset.noncommProd_insert_of_not_mem _ _ _ _ hnmem]
[GOAL]
case insert
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s✝ : Finset α
f g : α → β
comm_ff✝ : Set.Pairwise ↑s✝ fun x y => Commute (f x) (f y)
comm_gg✝ : Set.Pairwise ↑s✝ fun x y => Commute (g x) (g y)
comm_gf✝ : Set.Pairwise ↑s✝ fun x y => Commute (g x) (f y)
x : α
s : Finset α
hnmem : ¬x ∈ s
ih :
  ∀ (comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y))
    (comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
    (comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)),
    noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
      noncommProd s f comm_ff * noncommProd s g comm_gg
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
⊢ (f * g) x * noncommProd s (f * g) (_ : Set.Pairwise ↑s fun a b => Commute ((f * g) a) ((f * g) b)) =
    f x * noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) *
      (g x * noncommProd s g (_ : Set.Pairwise ↑s fun a b => Commute (g a) (g b)))
[PROOFSTEP]
specialize
  ih (comm_ff.mono fun _ => mem_insert_of_mem) (comm_gg.mono fun _ => mem_insert_of_mem)
    (comm_gf.mono fun _ => mem_insert_of_mem)
[GOAL]
case insert
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s✝ : Finset α
f g : α → β
comm_ff✝ : Set.Pairwise ↑s✝ fun x y => Commute (f x) (f y)
comm_gg✝ : Set.Pairwise ↑s✝ fun x y => Commute (g x) (g y)
comm_gf✝ : Set.Pairwise ↑s✝ fun x y => Commute (g x) (f y)
x : α
s : Finset α
hnmem : ¬x ∈ s
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
ih :
  noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
⊢ (f * g) x * noncommProd s (f * g) (_ : Set.Pairwise ↑s fun a b => Commute ((f * g) a) ((f * g) b)) =
    f x * noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) *
      (g x * noncommProd s g (_ : Set.Pairwise ↑s fun a b => Commute (g a) (g b)))
[PROOFSTEP]
rw [ih, Pi.mul_apply]
[GOAL]
case insert
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s✝ : Finset α
f g : α → β
comm_ff✝ : Set.Pairwise ↑s✝ fun x y => Commute (f x) (f y)
comm_gg✝ : Set.Pairwise ↑s✝ fun x y => Commute (g x) (g y)
comm_gf✝ : Set.Pairwise ↑s✝ fun x y => Commute (g x) (f y)
x : α
s : Finset α
hnmem : ¬x ∈ s
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
ih :
  noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
⊢ f x * g x *
      (noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
        noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))) =
    f x * noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) *
      (g x * noncommProd s g (_ : Set.Pairwise ↑s fun a b => Commute (g a) (g b)))
[PROOFSTEP]
simp only [mul_assoc]
[GOAL]
case insert
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s✝ : Finset α
f g : α → β
comm_ff✝ : Set.Pairwise ↑s✝ fun x y => Commute (f x) (f y)
comm_gg✝ : Set.Pairwise ↑s✝ fun x y => Commute (g x) (g y)
comm_gf✝ : Set.Pairwise ↑s✝ fun x y => Commute (g x) (f y)
x : α
s : Finset α
hnmem : ¬x ∈ s
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
ih :
  noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
⊢ f x *
      (g x *
        (noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
          noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y)))) =
    f x *
      (noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
        (g x * noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))))
[PROOFSTEP]
congr 1
[GOAL]
case insert.e_a
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s✝ : Finset α
f g : α → β
comm_ff✝ : Set.Pairwise ↑s✝ fun x y => Commute (f x) (f y)
comm_gg✝ : Set.Pairwise ↑s✝ fun x y => Commute (g x) (g y)
comm_gf✝ : Set.Pairwise ↑s✝ fun x y => Commute (g x) (f y)
x : α
s : Finset α
hnmem : ¬x ∈ s
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
ih :
  noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
⊢ g x *
      (noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
        noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      (g x * noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y)))
[PROOFSTEP]
simp only [← mul_assoc]
[GOAL]
case insert.e_a
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s✝ : Finset α
f g : α → β
comm_ff✝ : Set.Pairwise ↑s✝ fun x y => Commute (f x) (f y)
comm_gg✝ : Set.Pairwise ↑s✝ fun x y => Commute (g x) (g y)
comm_gf✝ : Set.Pairwise ↑s✝ fun x y => Commute (g x) (f y)
x : α
s : Finset α
hnmem : ¬x ∈ s
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
ih :
  noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
⊢ g x * noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) * g x *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
[PROOFSTEP]
congr 1
[GOAL]
case insert.e_a.e_a
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s✝ : Finset α
f g : α → β
comm_ff✝ : Set.Pairwise ↑s✝ fun x y => Commute (f x) (f y)
comm_gg✝ : Set.Pairwise ↑s✝ fun x y => Commute (g x) (g y)
comm_gf✝ : Set.Pairwise ↑s✝ fun x y => Commute (g x) (f y)
x : α
s : Finset α
hnmem : ¬x ∈ s
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
ih :
  noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
⊢ g x * noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) * g x
[PROOFSTEP]
refine' noncommProd_commute _ _ _ _ fun y hy => _
[GOAL]
case insert.e_a.e_a
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s✝ : Finset α
f g : α → β
comm_ff✝ : Set.Pairwise ↑s✝ fun x y => Commute (f x) (f y)
comm_gg✝ : Set.Pairwise ↑s✝ fun x y => Commute (g x) (g y)
comm_gf✝ : Set.Pairwise ↑s✝ fun x y => Commute (g x) (f y)
x : α
s : Finset α
hnmem : ¬x ∈ s
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
ih :
  noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
y : α
hy : y ∈ s
⊢ Commute (g x) (f y)
[PROOFSTEP]
exact comm_gf (mem_insert_self x s) (mem_insert_of_mem hy) (ne_of_mem_of_not_mem hy hnmem).symm
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
⊢ noncommProd univ (fun i => Pi.mulSingle i (x i))
      (_ :
        ∀ (i : ι), i ∈ ↑univ → ∀ (j : ι), j ∈ ↑univ → i ≠ j → Commute (Pi.mulSingle i (x i)) (Pi.mulSingle j (x j))) =
    x
[PROOFSTEP]
ext i
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ noncommProd univ (fun i => Pi.mulSingle i (x i))
      (_ : ∀ (i : ι), i ∈ ↑univ → ∀ (j : ι), j ∈ ↑univ → i ≠ j → Commute (Pi.mulSingle i (x i)) (Pi.mulSingle j (x j)))
      i =
    x i
[PROOFSTEP]
apply (univ.noncommProd_map (fun i => MonoidHom.single M i (x i)) _ (Pi.evalMonoidHom M i)).trans
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ noncommProd univ (fun i_1 => ↑(Pi.evalMonoidHom M i) (↑(MonoidHom.single M i_1) (x i_1)))
      (_ :
        ∀ (x_1 : ι),
          x_1 ∈ ↑univ →
            ∀ (y : ι),
              y ∈ ↑univ →
                x_1 ≠ y →
                  Commute (↑(Pi.evalMonoidHom M i) (↑(MonoidHom.single M x_1) (x x_1)))
                    (↑(Pi.evalMonoidHom M i) (↑(MonoidHom.single M y) (x y)))) =
    x i
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ Set.Pairwise ↑univ fun a b =>
    Commute ((fun i => ↑(MonoidHom.single M i) (x i)) a) ((fun i => ↑(MonoidHom.single M i) (x i)) b)
[PROOFSTEP]
refine' (noncommProd_congr (insert_erase (mem_univ i)).symm _ _).trans _
[GOAL]
case h.refine'_1
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ Set.Pairwise ↑univ fun a b =>
    Commute ((fun i => ↑(MonoidHom.single M i) (x i)) a) ((fun i => ↑(MonoidHom.single M i) (x i)) b)
[PROOFSTEP]
intro i _ j _ _
[GOAL]
case h.refine'_1
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i✝ i : ι
a✝² : i ∈ ↑univ
j : ι
a✝¹ : j ∈ ↑univ
a✝ : i ≠ j
⊢ Commute ((fun i => ↑(MonoidHom.single M i) (x i)) i) ((fun i => ↑(MonoidHom.single M i) (x i)) j)
[PROOFSTEP]
exact Pi.mulSingle_apply_commute x i j
[GOAL]
case h.refine'_2
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ι →
    (fun x => M i)
      (noncommProd univ (fun i => ↑(MonoidHom.single M i) (x i))
        (_ :
          ∀ ⦃i : ι⦄, i ∈ ↑univ → ∀ ⦃j : ι⦄, j ∈ ↑univ → i ≠ j → Commute (Pi.mulSingle i (x i)) (Pi.mulSingle j (x j))))
[PROOFSTEP]
intro j
[GOAL]
case h.refine'_2
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
⊢ (fun x => M i)
    (noncommProd univ (fun i => ↑(MonoidHom.single M i) (x i))
      (_ : ∀ ⦃i : ι⦄, i ∈ ↑univ → ∀ ⦃j : ι⦄, j ∈ ↑univ → i ≠ j → Commute (Pi.mulSingle i (x i)) (Pi.mulSingle j (x j))))
[PROOFSTEP]
exact Pi.mulSingle j (x j) i
[GOAL]
case h.refine'_3
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ (x_1 : ι),
    x_1 ∈ insert i (erase univ i) →
      ↑(Pi.evalMonoidHom M i) (↑(MonoidHom.single M x_1) (x x_1)) = Pi.mulSingle x_1 (x x_1) i
[PROOFSTEP]
intro j _
[GOAL]
case h.refine'_3
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
a✝ : j ∈ insert i (erase univ i)
⊢ ↑(Pi.evalMonoidHom M i) (↑(MonoidHom.single M j) (x j)) = Pi.mulSingle j (x j) i
[PROOFSTEP]
dsimp
[GOAL]
case h.refine'_4
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ noncommProd (insert i (erase univ i)) (fun j => Pi.mulSingle j (x j) i)
      (_ :
        ∀ (x_1 : ι),
          x_1 ∈ ↑(insert i (erase univ i)) →
            ∀ (y : ι),
              y ∈ ↑(insert i (erase univ i)) →
                x_1 ≠ y → (fun a b => Commute (Pi.mulSingle a (x a) i) (Pi.mulSingle b (x b) i)) x_1 y) =
    x i
[PROOFSTEP]
rw [noncommProd_insert_of_not_mem _ _ _ _ (not_mem_erase _ _), noncommProd_eq_pow_card (univ.erase i), one_pow, mul_one]
[GOAL]
case h.refine'_4
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ Pi.mulSingle i (x i) i = x i
case h.refine'_4.h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ (x_1 : ι), x_1 ∈ erase univ i → Pi.mulSingle x_1 (x x_1) i = 1
[PROOFSTEP]
simp
[GOAL]
case h.refine'_4.h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ (x_1 : ι), x_1 ∈ erase univ i → Pi.mulSingle x_1 (x x_1) i = 1
[PROOFSTEP]
intro j hj
[GOAL]
case h.refine'_4.h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
hj : j ∈ erase univ i
⊢ Pi.mulSingle j (x j) i = 1
[PROOFSTEP]
simp at hj
[GOAL]
case h.refine'_4.h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
hj : ¬j = i
⊢ Pi.mulSingle j (x j) i = 1
[PROOFSTEP]
simp [Pi.mulSingle, Function.update]
[GOAL]
case h.refine'_4.h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
hj : ¬j = i
⊢ ∀ (h : i = j), (_ : j = i) ▸ x j = 1
[PROOFSTEP]
intro h
[GOAL]
case h.refine'_4.h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
hj : ¬j = i
h : i = j
⊢ (_ : j = i) ▸ x j = 1
[PROOFSTEP]
simp [*] at *
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), ↑f (Pi.mulSingle i x) = ↑g (Pi.mulSingle i x)
⊢ f = g
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), ↑f (Pi.mulSingle i x) = ↑g (Pi.mulSingle i x)
val✝ : Fintype ι
⊢ f = g
[PROOFSTEP]
ext x
[GOAL]
case intro.h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), ↑f (Pi.mulSingle i x) = ↑g (Pi.mulSingle i x)
val✝ : Fintype ι
x : (i : ι) → M i
⊢ ↑f x = ↑g x
[PROOFSTEP]
rw [← noncommProd_mul_single x, univ.noncommProd_map, univ.noncommProd_map]
[GOAL]
case intro.h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), ↑f (Pi.mulSingle i x) = ↑g (Pi.mulSingle i x)
val✝ : Fintype ι
x : (i : ι) → M i
⊢ noncommProd univ (fun i => ↑f (Pi.mulSingle i (x i)))
      (_ :
        ∀ (x_1 : ι),
          x_1 ∈ ↑univ →
            ∀ (y : ι), y ∈ ↑univ → x_1 ≠ y → Commute (↑f (Pi.mulSingle x_1 (x x_1))) (↑f (Pi.mulSingle y (x y)))) =
    noncommProd univ (fun i => ↑g (Pi.mulSingle i (x i)))
      (_ :
        ∀ (x_1 : ι),
          x_1 ∈ ↑univ →
            ∀ (y : ι), y ∈ ↑univ → x_1 ≠ y → Commute (↑g (Pi.mulSingle x_1 (x x_1))) (↑g (Pi.mulSingle y (x y))))
[PROOFSTEP]
congr 1 with i
[GOAL]
case intro.h.e_f.h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), ↑f (Pi.mulSingle i x) = ↑g (Pi.mulSingle i x)
val✝ : Fintype ι
x : (i : ι) → M i
i : ι
⊢ ↑f (Pi.mulSingle i (x i)) = ↑g (Pi.mulSingle i (x i))
[PROOFSTEP]
exact h i (x i)