case empty
α : Type u
β : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝ : CommMonoid β
x : β
f : α → ℕ
⊢ ∏ i in ∅, x ^ f i = x ^ ∑ x in ∅, f x

case insert
α : Type u
β : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝ : CommMonoid β
x : β
f : α → ℕ
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s → ∏ i in s, x ^ f i = x ^ ∑ x in s, f x → ∏ i in insert a s, x ^ f i = x ^ ∑ x in insert a s, f x
α : Type u
β : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝ : CommMonoid β
x : β
f : α → ℕ
⊢ ∀ {s : Finset α}, ∏ i in s, x ^ f i = x ^ ∑ x in s, f x
apply Finset.induction
no goals
case empty
α : Type u
β : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝ : CommMonoid β
x : β
f : α → ℕ
⊢ ∏ i in ∅, x ^ f i = x ^ ∑ x in ∅, f x
simp
case insert
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g : α → β
inst✝ : CommMonoid β
x : β
f : α → ℕ
a : α
s : Finset α
has : ¬a ∈ s
H : ∏ i in s, x ^ f i = x ^ ∑ x in s, f x
⊢ ∏ i in insert a s, x ^ f i = x ^ ∑ x in insert a s, f x
case insert
α : Type u
β : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝ : CommMonoid β
x : β
f : α → ℕ
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s → ∏ i in s, x ^ f i = x ^ ∑ x in s, f x → ∏ i in insert a s, x ^ f i = x ^ ∑ x in insert a s, f x
intro a s has H
no goals
case insert
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
b : β
f✝ g : α → β
inst✝ : CommMonoid β
x : β
f : α → ℕ
a : α
s : Finset α
has : ¬a ∈ s
H : ∏ i in s, x ^ f i = x ^ ∑ x in s, f x
⊢ ∏ i in insert a s, x ^ f i = x ^ ∑ x in insert a s, f x
rw [Finset.prod_insert has, Finset.sum_insert has, pow_add, H]