case intro
α : Type u_2
β : Type ?u.365704
ι : Type u_1
G : Type ?u.365710
M : Type u_3
N : Type ?u.365716
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
inst✝ : Finite ι
t : ι → Set α
h : Pairwise (Disjoint on t)
ht : ∀ (i : ι), Set.Finite (t i)
val✝ : Fintype ι
⊢ (∏ᶠ (a : α) (_ : a ∈ ⋃ (i : ι), t i), f a) = ∏ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a
α : Type u_2
β : Type ?u.365704
ι : Type u_1
G : Type ?u.365710
M : Type u_3
N : Type ?u.365716
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
inst✝ : Finite ι
t : ι → Set α
h : Pairwise (Disjoint on t)
ht : ∀ (i : ι), Set.Finite (t i)
⊢ (∏ᶠ (a : α) (_ : a ∈ ⋃ (i : ι), t i), f a) = ∏ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a
cases nonempty_fintype ι
case intro.intro
α : Type u_2
β : Type ?u.365704
ι : Type u_1
G : Type ?u.365710
M : Type u_3
N : Type ?u.365716
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i => ↑(t i))
⊢ (∏ᶠ (a : α) (_ : a ∈ ⋃ (i : ι), (fun i => ↑(t i)) i), f a) = ∏ᶠ (i : ι) (a : α) (_ : a ∈ (fun i => ↑(t i)) i), f a
case intro
α : Type u_2
β : Type ?u.365704
ι : Type u_1
G : Type ?u.365710
M : Type u_3
N : Type ?u.365716
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
inst✝ : Finite ι
t : ι → Set α
h : Pairwise (Disjoint on t)
ht : ∀ (i : ι), Set.Finite (t i)
val✝ : Fintype ι
⊢ (∏ᶠ (a : α) (_ : a ∈ ⋃ (i : ι), t i), f a) = ∏ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a
lift t to ι → Finset α using ht
case intro.intro
α : Type u_2
β : Type ?u.365704
ι : Type u_1
G : Type ?u.365710
M : Type u_3
N : Type ?u.365716
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i => ↑(t i))
⊢ ∏ x : ι, ∏ i in t x, f i = ∏ᶠ (i : ι) (a : α) (_ : a ∈ (fun i => ↑(t i)) i), f a

case intro.intro
α : Type u_2
β : Type ?u.365704
ι : Type u_1
G : Type ?u.365710
M : Type u_3
N : Type ?u.365716
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i => ↑(t i))
⊢ PairwiseDisjoint ↑Finset.univ fun x => t x
case intro.intro
α : Type u_2
β : Type ?u.365704
ι : Type u_1
G : Type ?u.365710
M : Type u_3
N : Type ?u.365716
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i => ↑(t i))
⊢ (∏ᶠ (a : α) (_ : a ∈ ⋃ (i : ι), (fun i => ↑(t i)) i), f a) = ∏ᶠ (i : ι) (a : α) (_ : a ∈ (fun i => ↑(t i)) i), f a
rw [← biUnion_univ, ← Finset.coe_univ, ← Finset.coe_biUnion, finprod_mem_coe_finset,
  Finset.prod_biUnion]
no goals
case intro.intro
α : Type u_2
β : Type ?u.365704
ι : Type u_1
G : Type ?u.365710
M : Type u_3
N : Type ?u.365716
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i => ↑(t i))
⊢ ∏ x : ι, ∏ i in t x, f i = ∏ᶠ (i : ι) (a : α) (_ : a ∈ (fun i => ↑(t i)) i), f a
simp only [finprod_mem_coe_finset, finprod_eq_prod_of_fintype]
no goals
case intro.intro
α : Type u_2
β : Type ?u.365704
ι : Type u_1
G : Type ?u.365710
M : Type u_3
N : Type ?u.365716
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i => ↑(t i))
⊢ PairwiseDisjoint ↑Finset.univ fun x => t x
exact fun x _ y _ hxy => Finset.disjoint_coe.1 (h hxy)