ι : Type ?u.380694
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
f : α → β
p : α → Prop
inst✝ : DecidablePred p
h : ∀ (x : α), x ∈ s → p x
⊢ ∀ (x : α), x ∈ s → p x
ι : Type ?u.380694
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
f : α → β
p : α → Prop
inst✝ : DecidablePred p
h : ∀ (x : α), x ∈ s → p x
⊢ ∏ x in Finset.subtype p s, f ↑x = ∏ x in s, f x
rw [prod_subtype_eq_prod_filter, filter_true_of_mem]
no goals
ι : Type ?u.380694
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
f : α → β
p : α → Prop
inst✝ : DecidablePred p
h : ∀ (x : α), x ∈ s → p x
⊢ ∀ (x : α), x ∈ s → p x
simpa using h