no goals
k : Type u₁
G : Type u₂
R : Type ?u.1506427
ι : Type ui
inst✝¹ : CommSemiring k
inst✝ : CommMonoid G
s✝ : Finset ι
a✝ : ι → G
b : ι → k
a : ι
s : Finset ι
has : ¬a ∈ s
ih : ∏ i in s, single (a✝ i) (b i) = single (∏ i in s, a✝ i) (∏ i in s, b i)
⊢ ∏ i in cons a s has, single (a✝ i) (b i) = single (∏ i in cons a s has, a✝ i) (∏ i in cons a s has, b i)
rw [prod_cons has, ih, single_mul_single, prod_cons has, prod_cons has]