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