case intro
α : Type u_1
β : Type ?u.326633
ι : Type ?u.326636
G : Type ?u.326639
M : Type u_2
N : Type ?u.326645
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
t : Set α
ht : Set.Finite t
s : Finset α
⊢ ((∏ᶠ (i : α) (_ : i ∈ ↑s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑s ∩ t), f i) =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
α : Type u_1
β : Type ?u.326633
ι : Type ?u.326636
G : Type ?u.326639
M : Type u_2
N : Type ?u.326645
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hs : Set.Finite s
ht : Set.Finite t
⊢ ((∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) =
    (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
lift s to Finset α using hs
case intro.intro
α : Type u_1
β : Type ?u.326633
ι : Type ?u.326636
G : Type ?u.326639
M : Type u_2
N : Type ?u.326645
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Finset α
⊢ ((∏ᶠ (i : α) (_ : i ∈ ↑s ∪ ↑t), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑s ∩ ↑t), f i) =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑t), f i
case intro
α : Type u_1
β : Type ?u.326633
ι : Type ?u.326636
G : Type ?u.326639
M : Type u_2
N : Type ?u.326645
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
t : Set α
ht : Set.Finite t
s : Finset α
⊢ ((∏ᶠ (i : α) (_ : i ∈ ↑s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑s ∩ t), f i) =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
lift t to Finset α using ht
no goals
case intro.intro
α : Type u_1
β : Type ?u.326633
ι : Type ?u.326636
G : Type ?u.326639
M : Type u_2
N : Type ?u.326645
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Finset α
⊢ ((∏ᶠ (i : α) (_ : i ∈ ↑s ∪ ↑t), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑s ∩ ↑t), f i) =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑t), f i
classical
  rw [← Finset.coe_union, ← Finset.coe_inter]
  simp only [finprod_mem_coe_finset, Finset.prod_union_inter]
case intro.intro
α : Type u_1
β : Type ?u.326633
ι : Type ?u.326636
G : Type ?u.326639
M : Type u_2
N : Type ?u.326645
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Finset α
⊢ ((∏ᶠ (i : α) (_ : i ∈ ↑(s ∪ t)), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑(s ∩ t)), f i) =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑t), f i
case intro.intro
α : Type u_1
β : Type ?u.326633
ι : Type ?u.326636
G : Type ?u.326639
M : Type u_2
N : Type ?u.326645
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Finset α
⊢ ((∏ᶠ (i : α) (_ : i ∈ ↑s ∪ ↑t), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑s ∩ ↑t), f i) =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑t), f i
rw [← Finset.coe_union, ← Finset.coe_inter]
no goals
case intro.intro
α : Type u_1
β : Type ?u.326633
ι : Type ?u.326636
G : Type ?u.326639
M : Type u_2
N : Type ?u.326645
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Finset α
⊢ ((∏ᶠ (i : α) (_ : i ∈ ↑(s ∪ t)), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑(s ∩ t)), f i) =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑t), f i
simp only [finprod_mem_coe_finset, Finset.prod_union_inter]