α : Type u_2
β : Type ?u.368420
ι : Type u_1
G : Type ?u.368426
M : Type u_3
N : Type ?u.368432
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
I : Set ι
t : ι → Set α
h : PairwiseDisjoint I t
hI : Set.Finite I
ht : ∀ (i : ι), i ∈ I → Set.Finite (t i)
this : Fintype ↑I
⊢ (∏ᶠ (a : α) (_ : a ∈ ⋃ (x : ι) (_ : x ∈ I), t x), f a) = ∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j
α : Type u_2
β : Type ?u.368420
ι : Type u_1
G : Type ?u.368426
M : Type u_3
N : Type ?u.368432
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
I : Set ι
t : ι → Set α
h : PairwiseDisjoint I t
hI : Set.Finite I
ht : ∀ (i : ι), i ∈ I → Set.Finite (t i)
⊢ (∏ᶠ (a : α) (_ : a ∈ ⋃ (x : ι) (_ : x ∈ I), t x), f a) = ∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j
haveI := hI.fintype
case h
α : Type u_2
β : Type ?u.368420
ι : Type u_1
G : Type ?u.368426
M : Type u_3
N : Type ?u.368432
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
I : Set ι
t : ι → Set α
h : PairwiseDisjoint I t
hI : Set.Finite I
ht : ∀ (i : ι), i ∈ I → Set.Finite (t i)
this : Fintype ↑I
⊢ Pairwise (Disjoint on fun x => t ↑x)

case ht
α : Type u_2
β : Type ?u.368420
ι : Type u_1
G : Type ?u.368426
M : Type u_3
N : Type ?u.368432
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
I : Set ι
t : ι → Set α
h : PairwiseDisjoint I t
hI : Set.Finite I
ht : ∀ (i : ι), i ∈ I → Set.Finite (t i)
this : Fintype ↑I
⊢ ∀ (i : ↑I), Set.Finite (t ↑i)
α : Type u_2
β : Type ?u.368420
ι : Type u_1
G : Type ?u.368426
M : Type u_3
N : Type ?u.368432
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
I : Set ι
t : ι → Set α
h : PairwiseDisjoint I t
hI : Set.Finite I
ht : ∀ (i : ι), i ∈ I → Set.Finite (t i)
this : Fintype ↑I
⊢ (∏ᶠ (a : α) (_ : a ∈ ⋃ (x : ι) (_ : x ∈ I), t x), f a) = ∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j
rw [biUnion_eq_iUnion, finprod_mem_iUnion, ← finprod_set_coe_eq_finprod_mem]
no goals
case h
α : Type u_2
β : Type ?u.368420
ι : Type u_1
G : Type ?u.368426
M : Type u_3
N : Type ?u.368432
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
I : Set ι
t : ι → Set α
h : PairwiseDisjoint I t
hI : Set.Finite I
ht : ∀ (i : ι), i ∈ I → Set.Finite (t i)
this : Fintype ↑I
⊢ Pairwise (Disjoint on fun x => t ↑x)

case ht
α : Type u_2
β : Type ?u.368420
ι : Type u_1
G : Type ?u.368426
M : Type u_3
N : Type ?u.368432
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
I : Set ι
t : ι → Set α
h : PairwiseDisjoint I t
hI : Set.Finite I
ht : ∀ (i : ι), i ∈ I → Set.Finite (t i)
this : Fintype ↑I
⊢ ∀ (i : ↑I), Set.Finite (t ↑i)
exacts [fun x y hxy => h x.2 y.2 (Subtype.coe_injective.ne hxy), fun b => ht b b.2]