ι : Type ?u.281798
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
h : Disjoint s₁ s₂
⊢ ∏ x in disjUnion s₁ s₂ h, f x = fold (fun x x_1 => x * x_1) (1 * 1) (fun x => f x) (disjUnion s₁ s₂ h)
ι : Type ?u.281798
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
h : Disjoint s₁ s₂
⊢ ∏ x in disjUnion s₁ s₂ h, f x = (∏ x in s₁, f x) * ∏ x in s₂, f x
refine' Eq.trans _ (fold_disjUnion h)
ι : Type ?u.281798
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
h : Disjoint s₁ s₂
⊢ ∏ x in disjUnion s₁ s₂ h, f x = fold (fun x x_1 => x * x_1) 1 (fun x => f x) (disjUnion s₁ s₂ h)
ι : Type ?u.281798
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
h : Disjoint s₁ s₂
⊢ ∏ x in disjUnion s₁ s₂ h, f x = fold (fun x x_1 => x * x_1) (1 * 1) (fun x => f x) (disjUnion s₁ s₂ h)
rw [one_mul]
no goals
ι : Type ?u.281798
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
h : Disjoint s₁ s₂
⊢ ∏ x in disjUnion s₁ s₂ h, f x = fold (fun x x_1 => x * x_1) 1 (fun x => f x) (disjUnion s₁ s₂ h)
rfl