ι : Type ?u.405265
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
p : α → Prop
hp : DecidablePred p
f g : α → β
h : ∀ (x : α), x ∈ s → p x
⊢ (∏ x in s, if ¬p x then g x else f x) = ∏ x in s, f x
ι : Type ?u.405265
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
p : α → Prop
hp : DecidablePred p
f g : α → β
h : ∀ (x : α), x ∈ s → p x
⊢ (∏ x in s, if p x then f x else g x) = ∏ x in s, f x
simp_rw [← ite_not (p _)]
case h
ι : Type ?u.405265
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
p : α → Prop
hp : DecidablePred p
f g : α → β
h : ∀ (x : α), x ∈ s → p x
⊢ ∀ (x : α), x ∈ s → ¬¬p x
ι : Type ?u.405265
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
p : α → Prop
hp : DecidablePred p
f g : α → β
h : ∀ (x : α), x ∈ s → p x
⊢ (∏ x in s, if ¬p x then g x else f x) = ∏ x in s, f x
apply prod_ite_of_false
no goals
case h
ι : Type ?u.405265
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
p : α → Prop
hp : DecidablePred p
f g : α → β
h : ∀ (x : α), x ∈ s → p x
⊢ ∀ (x : α), x ∈ s → ¬¬p x
simpa