α : Type u_1
ι : Type ?u.18979
γ : Type ?u.18982
A : Type ?u.18985
B : Type ?u.18988
C : Type ?u.18991
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.22121
M : Type u_2
M' : Type ?u.22127
N : Type u_3
P : Type ?u.22133
G : Type ?u.22136
H : Type ?u.22139
R : Type ?u.22142
S : Type ?u.22145
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : α →₀ M
s : Finset α
hs : f.support ⊆ s
g : α → M → N
h : ∀ (i : α), i ∈ s → g i 0 = 1
x : α
hxs : x ∈ s
hx : ¬x ∈ f.support
⊢ ↑f x = 0
α : Type u_1
ι : Type ?u.18979
γ : Type ?u.18982
A : Type ?u.18985
B : Type ?u.18988
C : Type ?u.18991
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.22121
M : Type u_2
M' : Type ?u.22127
N : Type u_3
P : Type ?u.22133
G : Type ?u.22136
H : Type ?u.22139
R : Type ?u.22142
S : Type ?u.22145
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : α →₀ M
s : Finset α
hs : f.support ⊆ s
g : α → M → N
h : ∀ (i : α), i ∈ s → g i 0 = 1
⊢ prod f g = ∏ x in s, g x (↑f x)
refine Finset.prod_subset hs fun x hxs hx => h x hxs ▸ (congr_arg (g x) ?_)
no goals
α : Type u_1
ι : Type ?u.18979
γ : Type ?u.18982
A : Type ?u.18985
B : Type ?u.18988
C : Type ?u.18991
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.22121
M : Type u_2
M' : Type ?u.22127
N : Type u_3
P : Type ?u.22133
G : Type ?u.22136
H : Type ?u.22139
R : Type ?u.22142
S : Type ?u.22145
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : α →₀ M
s : Finset α
hs : f.support ⊆ s
g : α → M → N
h : ∀ (i : α), i ∈ s → g i 0 = 1
x : α
hxs : x ∈ s
hx : ¬x ∈ f.support
⊢ ↑f x = 0
exact not_mem_support_iff.1 hx