ι : Type ?u.787616
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel Setoid.r
x : α
_hx : x ∈ s
⊢ ∏ y in filter (fun x_1 => Quotient.mk R x_1 = Quotient.mk'' x) s, f y =
    ∏ x in filter (fun c' => Quotient.mk'' c' = Quotient.mk'' x) s, f x
ι : Type ?u.787616
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel Setoid.r
⊢ ∏ x in s, f x = ∏ xbar in image Quotient.mk'' s, ∏ y in filter (fun x => Quotient.mk R x = xbar) s, f y
refine' (Finset.prod_image' f fun x _hx => _).symm
no goals
ι : Type ?u.787616
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel Setoid.r
x : α
_hx : x ∈ s
⊢ ∏ y in filter (fun x_1 => Quotient.mk R x_1 = Quotient.mk'' x) s, f y =
    ∏ x in filter (fun c' => Quotient.mk'' c' = Quotient.mk'' x) s, f x
rfl