ι : Type ?u.308476
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α ⊕ γ → β
⊢ (∏ x in s, f (↑Function.Embedding.inl x)) * ∏ x in t, f (↑Function.Embedding.inr x) =
    (∏ x in s, f (Sum.inl x)) * ∏ x in t, f (Sum.inr x)
ι : Type ?u.308476
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α ⊕ γ → β
⊢ ∏ x in disjSum s t, f x = (∏ x in s, f (Sum.inl x)) * ∏ x in t, f (Sum.inr x)
rw [← map_inl_disjUnion_map_inr, prod_disjUnion, prod_map, prod_map]
no goals
ι : Type ?u.308476
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α ⊕ γ → β
⊢ (∏ x in s, f (↑Function.Embedding.inl x)) * ∏ x in t, f (↑Function.Embedding.inr x) =
    (∏ x in s, f (Sum.inl x)) * ∏ x in t, f (Sum.inr x)
rfl