ι : Type ?u.286983
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
h : Disjoint s₁ s₂
⊢ ∏ x in s₁ ∪ s₂, f x = (∏ x in s₁ ∪ s₂, f x) * ∏ x in ∅, f x
ι : Type ?u.286983
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
h : Disjoint s₁ s₂
⊢ ∏ x in s₁ ∪ s₂, f x = (∏ x in s₁, f x) * ∏ x in s₂, f x
rw [← prod_union_inter, disjoint_iff_inter_eq_empty.mp h]
no goals
ι : Type ?u.286983
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
h : Disjoint s₁ s₂
⊢ ∏ x in s₁ ∪ s₂, f x = (∏ x in s₁ ∪ s₂, f x) * ∏ x in ∅, f x
exact (mul_one _).symm