ι : Type ?u.379810
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
f : α → β
p : α → Prop
inst✝ : DecidablePred p
⊢ ∏ x in map (Function.Embedding.subtype p) (Finset.subtype p s), f x = ∏ x in filter p s, f x
ι : Type ?u.379810
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
f : α → β
p : α → Prop
inst✝ : DecidablePred p
⊢ ∏ x in Finset.subtype p s, f ↑x = ∏ x in filter p s, f x
conv_lhs => erw [← prod_map (s.subtype p) (Function.Embedding.subtype _) f]
no goals
ι : Type ?u.379810
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
f : α → β
p : α → Prop
inst✝ : DecidablePred p
⊢ ∏ x in map (Function.Embedding.subtype p) (Finset.subtype p s), f x = ∏ x in filter p s, f x
exact prod_congr (subtype_map _) fun x _hx => rfl