no goals
α : Type u_4
ι : Type u_3
γ : Type ?u.544772
A : Type ?u.544775
B : Type ?u.544778
C : Type ?u.544781
inst✝⁴ : AddCommMonoid A
inst✝³ : AddCommMonoid B
inst✝² : AddCommMonoid C
t : ι → A → C
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
s✝¹ : Finset α
f : α → ι →₀ A
i : ι
g✝ : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type ?u.547911
M : Type u_1
M' : Type ?u.547917
N : Type u_2
P : Type ?u.547923
G : Type ?u.547926
H : Type ?u.547929
R : Type ?u.547932
S : Type ?u.547935
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
s✝ : Finset ι
g : ι → α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
a : ι
s : Finset ι
has : ¬a ∈ s
ih : ∏ i in s, prod (g i) h = prod (∑ i in s, g i) h
⊢ ∏ i in cons a s has, prod (g i) h = prod (∑ i in cons a s has, g i) h
rw [prod_cons, ih, sum_cons, prod_add_index' h_zero h_add]