α : Type u_1
β : Type ?u.330069
ι : Type ?u.330072
G : Type ?u.330075
M : Type u_2
N : Type ?u.330081
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hs : Set.Finite (s ∩ mulSupport f)
ht : Set.Finite (t ∩ mulSupport f)
⊢ ((∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t ∩ mulSupport f), f i) =
    (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i
α : Type u_1
β : Type ?u.330069
ι : Type ?u.330072
G : Type ?u.330075
M : Type u_2
N : Type ?u.330081
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hs : Set.Finite (s ∩ mulSupport f)
ht : Set.Finite (t ∩ mulSupport f)
⊢ ((∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) =
    (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
rw [← finprod_mem_inter_mulSupport f s, ← finprod_mem_inter_mulSupport f t, ←
  finprod_mem_union_inter hs ht, ← union_inter_distrib_right, finprod_mem_inter_mulSupport, ←
  finprod_mem_inter_mulSupport f (s ∩ t)]
case e_a.e_f
α : Type u_1
β : Type ?u.330069
ι : Type ?u.330072
G : Type ?u.330075
M : Type u_2
N : Type ?u.330081
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hs : Set.Finite (s ∩ mulSupport f)
ht : Set.Finite (t ∩ mulSupport f)
⊢ (fun i => ∏ᶠ (_ : i ∈ s ∩ t ∩ mulSupport f), f i) = fun i => ∏ᶠ (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i
α : Type u_1
β : Type ?u.330069
ι : Type ?u.330072
G : Type ?u.330075
M : Type u_2
N : Type ?u.330081
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hs : Set.Finite (s ∩ mulSupport f)
ht : Set.Finite (t ∩ mulSupport f)
⊢ ((∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t ∩ mulSupport f), f i) =
    (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i
congr 2
no goals
case e_a.e_f
α : Type u_1
β : Type ?u.330069
ι : Type ?u.330072
G : Type ?u.330075
M : Type u_2
N : Type ?u.330081
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hs : Set.Finite (s ∩ mulSupport f)
ht : Set.Finite (t ∩ mulSupport f)
⊢ (fun i => ∏ᶠ (_ : i ∈ s ∩ t ∩ mulSupport f), f i) = fun i => ∏ᶠ (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i
rw [inter_left_comm, inter_assoc, inter_assoc, inter_self, inter_left_comm]