no goals
α : Type u_1
ι : Type ?u.133454
γ : Type ?u.133457
A : Type ?u.133460
B : Type ?u.133463
C : Type ?u.133466
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.136596
M : Type u_2
M' : Type ?u.136602
N : Type u_3
P : Type ?u.136608
G : Type ?u.136611
H : Type ?u.136614
R : Type ?u.136617
S : Type ?u.136620
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
s : Finset α
f : α → M
g : α → M → N
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
hg : ∀ (a : α), g a 0 = 1
⊢ ∀ (x : α), x ∈ s → ¬x ∈ (onFinset s f hf).support → g x (↑(onFinset s f hf) x) = 1
simp (config := { contextual := true }) [*]