α : Type u_1
ι : Type ?u.70555
γ : Type ?u.70558
A : Type ?u.70561
B : Type ?u.70564
C : Type ?u.70567
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.73697
M : Type u_2
M' : Type ?u.73703
N : Type u_3
P : Type ?u.73709
G : Type ?u.73712
H : Type ?u.73715
R : Type ?u.73718
S : Type ?u.73721
inst✝³ : Zero M
inst✝² : Zero M'
inst✝¹ : CommMonoid N
inst✝ : DecidableEq α
f : α →₀ M
a : α
b : α → M → N
⊢ (∏ a_1 in f.support, if a_1 = a then b a_1 (↑f a_1) else 1) = if a ∈ f.support then b a (↑f a) else 1
α : Type u_1
ι : Type ?u.70555
γ : Type ?u.70558
A : Type ?u.70561
B : Type ?u.70564
C : Type ?u.70567
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.73697
M : Type u_2
M' : Type ?u.73703
N : Type u_3
P : Type ?u.73709
G : Type ?u.73712
H : Type ?u.73715
R : Type ?u.73718
S : Type ?u.73721
inst✝³ : Zero M
inst✝² : Zero M'
inst✝¹ : CommMonoid N
inst✝ : DecidableEq α
f : α →₀ M
a : α
b : α → M → N
⊢ (prod f fun x v => if x = a then b x v else 1) = if a ∈ f.support then b a (↑f a) else 1
dsimp [Finsupp.prod]
no goals
α : Type u_1
ι : Type ?u.70555
γ : Type ?u.70558
A : Type ?u.70561
B : Type ?u.70564
C : Type ?u.70567
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.73697
M : Type u_2
M' : Type ?u.73703
N : Type u_3
P : Type ?u.73709
G : Type ?u.73712
H : Type ?u.73715
R : Type ?u.73718
S : Type ?u.73721
inst✝³ : Zero M
inst✝² : Zero M'
inst✝¹ : CommMonoid N
inst✝ : DecidableEq α
f : α →₀ M
a : α
b : α → M → N
⊢ (∏ a_1 in f.support, if a_1 = a then b a_1 (↑f a_1) else 1) = if a ∈ f.support then b a (↑f a) else 1
rw [f.support.prod_ite_eq']