case h.e'_3.a.h.e
ι : Type ?u.772557
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s t : Finset α
f : α → β
x✝ : α
a✝ : x✝ ∈ s
⊢ f = piecewise t f f
ι : Type ?u.772557
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s t : Finset α
f : α → β
⊢ (∏ x in s ∩ t, f x) * ∏ x in s \ t, f x = ∏ x in s, f x
convert (s.prod_piecewise t f f).symm
no goals
case h.e'_3.a.h.e
ι : Type ?u.772557
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s t : Finset α
f : α → β
x✝ : α
a✝ : x✝ ∈ s
⊢ f = piecewise t f f
simp [Finset.piecewise]