case pos
α : Type u_1
ι : Type ?u.145629
γ : Type ?u.145632
A : Type ?u.145635
B : Type ?u.145638
C : Type ?u.145641
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.148771
M : Type u_2
M' : Type ?u.148777
N : Type u_3
P : Type ?u.148783
G : Type ?u.148786
H : Type ?u.148789
R : Type ?u.148792
S : Type ?u.148795
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
hyf : y ∈ f.support
⊢ g y (↑f y) * prod (erase y f) g = prod f g

case neg
α : Type u_1
ι : Type ?u.145629
γ : Type ?u.145632
A : Type ?u.145635
B : Type ?u.145638
C : Type ?u.145641
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.148771
M : Type u_2
M' : Type ?u.148777
N : Type u_3
P : Type ?u.148783
G : Type ?u.148786
H : Type ?u.148789
R : Type ?u.148792
S : Type ?u.148795
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
hyf : ¬y ∈ f.support
⊢ g y (↑f y) * prod (erase y f) g = prod f g
α : Type u_1
ι : Type ?u.145629
γ : Type ?u.145632
A : Type ?u.145635
B : Type ?u.145638
C : Type ?u.145641
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.148771
M : Type u_2
M' : Type ?u.148777
N : Type u_3
P : Type ?u.148783
G : Type ?u.148786
H : Type ?u.148789
R : Type ?u.148792
S : Type ?u.148795
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
⊢ g y (↑f y) * prod (erase y f) g = prod f g
by_cases hyf : y ∈ f.support
no goals
case pos
α : Type u_1
ι : Type ?u.145629
γ : Type ?u.145632
A : Type ?u.145635
B : Type ?u.145638
C : Type ?u.145641
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.148771
M : Type u_2
M' : Type ?u.148777
N : Type u_3
P : Type ?u.148783
G : Type ?u.148786
H : Type ?u.148789
R : Type ?u.148792
S : Type ?u.148795
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
hyf : y ∈ f.support
⊢ g y (↑f y) * prod (erase y f) g = prod f g
exact Finsupp.mul_prod_erase f y g hyf
no goals
case neg
α : Type u_1
ι : Type ?u.145629
γ : Type ?u.145632
A : Type ?u.145635
B : Type ?u.145638
C : Type ?u.145641
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.148771
M : Type u_2
M' : Type ?u.148777
N : Type u_3
P : Type ?u.148783
G : Type ?u.148786
H : Type ?u.148789
R : Type ?u.148792
S : Type ?u.148795
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
hyf : ¬y ∈ f.support
⊢ g y (↑f y) * prod (erase y f) g = prod f g
rw [not_mem_support_iff.mp hyf, hg y, erase_of_not_mem_support hyf, one_mul]