ι : Type u_1
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
s : Finset ι
t : ι → Finset α
h : Set.PairwiseDisjoint (↑s) t
⊢ ∏ x in disjiUnion s t h, f x =
    fold (fun x x_1 => x * x_1) (fold (fun x x_1 => x * x_1) 1 (fun i => 1) s) (fun x => f x) (disjiUnion s t h)
ι : Type u_1
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
s : Finset ι
t : ι → Finset α
h : Set.PairwiseDisjoint (↑s) t
⊢ ∏ x in disjiUnion s t h, f x = ∏ i in s, ∏ x in t i, f x
refine' Eq.trans _ (fold_disjiUnion h)
ι : Type u_1
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
s : Finset ι
t : ι → Finset α
h : Set.PairwiseDisjoint (↑s) t
⊢ Multiset.foldr (fun x x_1 => x * x_1) (_ : ∀ (x y z : β), x * (y * z) = y * (x * z)) 1
      (Multiset.map (fun x => f x) (Multiset.bind s.val fun a => (t a).val)) =
    Multiset.foldr (fun x x_1 => x * x_1) (_ : LeftCommutative fun x x_1 => x * x_1)
      (Multiset.foldr (fun x x_1 => x * x_1) (_ : LeftCommutative fun x x_1 => x * x_1) 1
        (Multiset.map (fun i => 1) s.val))
      (Multiset.map (fun x => f x) (Multiset.bind s.val fun a => (t a).val))
ι : Type u_1
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
s : Finset ι
t : ι → Finset α
h : Set.PairwiseDisjoint (↑s) t
⊢ ∏ x in disjiUnion s t h, f x =
    fold (fun x x_1 => x * x_1) (fold (fun x x_1 => x * x_1) 1 (fun i => 1) s) (fun x => f x) (disjiUnion s t h)
dsimp [Finset.prod, Multiset.prod, Multiset.fold, Finset.disjUnion, Finset.fold]
case e_b
ι : Type u_1
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
s : Finset ι
t : ι → Finset α
h : Set.PairwiseDisjoint (↑s) t
⊢ 1 =
    Multiset.foldr (fun x x_1 => x * x_1) (_ : LeftCommutative fun x x_1 => x * x_1) 1 (Multiset.map (fun i => 1) s.val)
ι : Type u_1
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
s : Finset ι
t : ι → Finset α
h : Set.PairwiseDisjoint (↑s) t
⊢ Multiset.foldr (fun x x_1 => x * x_1) (_ : ∀ (x y z : β), x * (y * z) = y * (x * z)) 1
      (Multiset.map (fun x => f x) (Multiset.bind s.val fun a => (t a).val)) =
    Multiset.foldr (fun x x_1 => x * x_1) (_ : LeftCommutative fun x x_1 => x * x_1)
      (Multiset.foldr (fun x x_1 => x * x_1) (_ : LeftCommutative fun x x_1 => x * x_1) 1
        (Multiset.map (fun i => 1) s.val))
      (Multiset.map (fun x => f x) (Multiset.bind s.val fun a => (t a).val))
congr
no goals
case e_b
ι : Type u_1
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
s : Finset ι
t : ι → Finset α
h : Set.PairwiseDisjoint (↑s) t
⊢ 1 =
    Multiset.foldr (fun x x_1 => x * x_1) (_ : LeftCommutative fun x x_1 => x * x_1) 1 (Multiset.map (fun i => 1) s.val)
exact prod_const_one.symm