ι : Type ?u.382203
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
p : α → Prop
s : Finset { x // p x }
f : { x // p x } → β
g : α → β
h : ∀ (x : { x // p x }), x ∈ s → g ↑x = f x
⊢ ∏ x in s, g (↑(Function.Embedding.subtype fun x => p x) x) = ∏ x in s, f x
ι : Type ?u.382203
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
p : α → Prop
s : Finset { x // p x }
f : { x // p x } → β
g : α → β
h : ∀ (x : { x // p x }), x ∈ s → g ↑x = f x
⊢ ∏ x in map (Function.Embedding.subtype fun x => p x) s, g x = ∏ x in s, f x
rw [Finset.prod_map]
no goals
ι : Type ?u.382203
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
p : α → Prop
s : Finset { x // p x }
f : { x // p x } → β
g : α → β
h : ∀ (x : { x // p x }), x ∈ s → g ↑x = f x
⊢ ∏ x in s, g (↑(Function.Embedding.subtype fun x => p x) x) = ∏ x in s, f x
exact Finset.prod_congr rfl h