case empty
F : Type ?u.197647
ι : Type ?u.197650
α : Type u_2
β✝ : Type ?u.197656
γ : Type ?u.197659
f✝ : α → β✝ → β✝
op : α → α → α
inst✝² : Monoid β✝
inst✝¹ : Monoid γ
β : Type u_1
inst✝ : CommMonoid β
f : α → β
⊢ noncommProd ∅ f (_ : ∀ (x : α), x ∈ ↑∅ → ∀ (x_2 : α), x_2 ∈ ↑∅ → x ≠ x_2 → Commute (f x) (f x_2)) = Finset.prod ∅ f

case insert
F : Type ?u.197647
ι : Type ?u.197650
α : Type u_2
β✝ : Type ?u.197656
γ : Type ?u.197659
f✝ : α → β✝ → β✝
op : α → α → α
inst✝² : Monoid β✝
inst✝¹ : Monoid γ
β : Type u_1
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
F : Type ?u.197647
ι : Type ?u.197650
α : Type u_2
β✝ : Type ?u.197656
γ : Type ?u.197659
f✝ : α → β✝ → β✝
op : α → α → α
inst✝² : Monoid β✝
inst✝¹ : Monoid γ
β : Type u_1
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
induction' s using Finset.induction_on with a s ha IH
no goals
case empty
F : Type ?u.197647
ι : Type ?u.197650
α : Type u_2
β✝ : Type ?u.197656
γ : Type ?u.197659
f✝ : α → β✝ → β✝
op : α → α → α
inst✝² : Monoid β✝
inst✝¹ : Monoid γ
β : Type u_1
inst✝ : CommMonoid β
f : α → β
⊢ noncommProd ∅ f (_ : ∀ (x : α), x ∈ ↑∅ → ∀ (x_2 : α), x_2 ∈ ↑∅ → x ≠ x_2 → Commute (f x) (f x_2)) = Finset.prod ∅ f
simp
no goals
case insert
F : Type ?u.197647
ι : Type ?u.197650
α : Type u_2
β✝ : Type ?u.197656
γ : Type ?u.197659
f✝ : α → β✝ → β✝
op : α → α → α
inst✝² : Monoid β✝
inst✝¹ : Monoid γ
β : Type u_1
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
simp [ha, IH]