α : Type u_2
β : Type ?u.106435
ι : Type u_1
M : Type u_3
N : Type ?u.106444
inst✝¹ : CommMonoid M
s : Finset ι
f : ι → α → M
t : ι → Set α
g : ι → α
inst✝ : DecidablePred fun i => g i ∈ t i
⊢ (∏ x in Finset.filter (fun i => g i ∈ t i) s, mulIndicator (t x) (f x) (g x)) *
      ∏ x in Finset.filter (fun x => ¬g x ∈ t x) s, mulIndicator (t x) (f x) (g x) =
    ∏ i in Finset.filter (fun i => g i ∈ t i) s, f i (g i)
α : Type u_2
β : Type ?u.106435
ι : Type u_1
M : Type u_3
N : Type ?u.106444
inst✝¹ : CommMonoid M
s : Finset ι
f : ι → α → M
t : ι → Set α
g : ι → α
inst✝ : DecidablePred fun i => g i ∈ t i
⊢ ∏ i in s, mulIndicator (t i) (f i) (g i) = ∏ i in Finset.filter (fun i => g i ∈ t i) s, f i (g i)
refine' (Finset.prod_filter_mul_prod_filter_not s (fun i => g i ∈ t i) _).symm.trans _
α : Type u_2
β : Type ?u.106435
ι : Type u_1
M : Type u_3
N : Type ?u.106444
inst✝¹ : CommMonoid M
s : Finset ι
f : ι → α → M
t : ι → Set α
g : ι → α
inst✝ : DecidablePred fun i => g i ∈ t i
⊢ (∏ x in Finset.filter (fun i => g i ∈ t i) s, mulIndicator (t x) (f x) (g x)) *
      ∏ x in Finset.filter (fun x => ¬g x ∈ t x) s, mulIndicator (t x) (f x) (g x) =
    (∏ i in Finset.filter (fun i => g i ∈ t i) s, f i (g i)) * 1
α : Type u_2
β : Type ?u.106435
ι : Type u_1
M : Type u_3
N : Type ?u.106444
inst✝¹ : CommMonoid M
s : Finset ι
f : ι → α → M
t : ι → Set α
g : ι → α
inst✝ : DecidablePred fun i => g i ∈ t i
⊢ (∏ x in Finset.filter (fun i => g i ∈ t i) s, mulIndicator (t x) (f x) (g x)) *
      ∏ x in Finset.filter (fun x => ¬g x ∈ t x) s, mulIndicator (t x) (f x) (g x) =
    ∏ i in Finset.filter (fun i => g i ∈ t i) s, f i (g i)
refine' Eq.trans _ (mul_one _)