no goals
ι : Type u
γ✝ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
γ : Type w
α : Type x
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
s : Finset α
g : α → Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
⊢ ∏ i in s, prod (g i) h = prod (∑ i in s, g i) h
classical
exact Finset.induction_on s (by simp [prod_zero_index])
      (by simp (config := { contextual := true }) [prod_add_index, h_zero, h_add])
no goals
ι : Type u
γ✝ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
γ : Type w
α : Type x
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
s : Finset α
g : α → Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
⊢ ∏ i in s, prod (g i) h = prod (∑ i in s, g i) h
exact Finset.induction_on s (by simp [prod_zero_index])
      (by simp (config := { contextual := true }) [prod_add_index, h_zero, h_add])
no goals
ι : Type u
γ✝ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
γ : Type w
α : Type x
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
s : Finset α
g : α → Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
⊢ ∏ i in ∅, prod (g i) h = prod (∑ i in ∅, g i) h
simp [prod_zero_index]
no goals
ι : Type u
γ✝ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
γ : Type w
α : Type x
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
s : Finset α
g : α → Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s →
      ∏ i in s, prod (g i) h = prod (∑ i in s, g i) h →
        ∏ i in insert a s, prod (g i) h = prod (∑ i in insert a s, g i) h
simp (config := { contextual := true }) [prod_add_index, h_zero, h_add]