no goals
α : Type u_3
ι : Type ?u.27350
γ : Type ?u.27353
A : Type ?u.27356
B : Type ?u.27359
C : Type ?u.27362
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.30492
M : Type u_2
M' : Type ?u.30498
N : Type u_1
P : Type ?u.30504
G : Type ?u.30507
H : Type ?u.30510
R : Type ?u.30513
S : Type ?u.30516
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
a : α
b : M
h : α → M → N
h_zero : h a 0 = 1
⊢ ∏ x in {a}, h x (↑(single a b) x) = h a b
simp