ι : Type ?u.791147
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : i ∈ s
f : α → β
b : β
⊢ (∏ x in s ∩ {i}, b) * ∏ x in s \ {i}, f x = b * ∏ x in s \ {i}, f x
ι : Type ?u.791147
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : i ∈ s
f : α → β
b : β
⊢ ∏ x in s, Function.update f i b x = b * ∏ x in s \ {i}, f x
rw [update_eq_piecewise, prod_piecewise]
no goals
ι : Type ?u.791147
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : i ∈ s
f : α → β
b : β
⊢ (∏ x in s ∩ {i}, b) * ∏ x in s \ {i}, f x = b * ∏ x in s \ {i}, f x
simp [h]