no goals
α : Type u_2
β : Type ?u.475516
γ : Type ?u.475519
ι : Type ?u.475522
M : Type u_3
M' : Type ?u.475528
N : Type u_1
P : Type ?u.475534
G : Type ?u.475537
H : Type ?u.475540
R : Type ?u.475543
S : Type ?u.475546
inst✝¹ : Zero M
p : α → Prop
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
⊢ prod (filter p f) g = ∏ x in (filter p f).support, g x (↑f x)
classical
  refine' Finset.prod_congr rfl fun x hx => _
  rw [support_filter, Finset.mem_filter] at hx
  rw [filter_apply_pos _ _ hx.2]
α : Type u_2
β : Type ?u.475516
γ : Type ?u.475519
ι : Type ?u.475522
M : Type u_3
M' : Type ?u.475528
N : Type u_1
P : Type ?u.475534
G : Type ?u.475537
H : Type ?u.475540
R : Type ?u.475543
S : Type ?u.475546
inst✝¹ : Zero M
p : α → Prop
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
x : α
hx : x ∈ (filter p f).support
⊢ g x (↑(filter p f) x) = g x (↑f x)
α : Type u_2
β : Type ?u.475516
γ : Type ?u.475519
ι : Type ?u.475522
M : Type u_3
M' : Type ?u.475528
N : Type u_1
P : Type ?u.475534
G : Type ?u.475537
H : Type ?u.475540
R : Type ?u.475543
S : Type ?u.475546
inst✝¹ : Zero M
p : α → Prop
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
⊢ prod (filter p f) g = ∏ x in (filter p f).support, g x (↑f x)
refine' Finset.prod_congr rfl fun x hx => _
α : Type u_2
β : Type ?u.475516
γ : Type ?u.475519
ι : Type ?u.475522
M : Type u_3
M' : Type ?u.475528
N : Type u_1
P : Type ?u.475534
G : Type ?u.475537
H : Type ?u.475540
R : Type ?u.475543
S : Type ?u.475546
inst✝¹ : Zero M
p : α → Prop
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
x : α
hx : x ∈ f.support ∧ p x
⊢ g x (↑(filter p f) x) = g x (↑f x)
α : Type u_2
β : Type ?u.475516
γ : Type ?u.475519
ι : Type ?u.475522
M : Type u_3
M' : Type ?u.475528
N : Type u_1
P : Type ?u.475534
G : Type ?u.475537
H : Type ?u.475540
R : Type ?u.475543
S : Type ?u.475546
inst✝¹ : Zero M
p : α → Prop
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
x : α
hx : x ∈ (filter p f).support
⊢ g x (↑(filter p f) x) = g x (↑f x)
rw [support_filter, Finset.mem_filter] at hx
no goals
α : Type u_2
β : Type ?u.475516
γ : Type ?u.475519
ι : Type ?u.475522
M : Type u_3
M' : Type ?u.475528
N : Type u_1
P : Type ?u.475534
G : Type ?u.475537
H : Type ?u.475540
R : Type ?u.475543
S : Type ?u.475546
inst✝¹ : Zero M
p : α → Prop
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
x : α
hx : x ∈ f.support ∧ p x
⊢ g x (↑(filter p f) x) = g x (↑f x)
rw [filter_apply_pos _ _ hx.2]