ι : Type ?u.403432
β : 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 ∅, f x) * ∏ x in s, g x = ∏ x in s, g x

ι : Type ?u.403432
β : 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.403432
β : 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.403432
β : 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, g x
rw [prod_ite, filter_false_of_mem, filter_true_of_mem]
no goals
ι : Type ?u.403432
β : 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.403432
β : 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
all_goals intros; simp; apply h; assumption
no goals
ι : Type ?u.403432
β : 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 ∅, f x) * ∏ x in s, g x = ∏ x in s, g x
simp only [prod_empty, one_mul]
ι : Type ?u.403432
β : 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✝ : α
a✝ : x✝ ∈ s
⊢ ¬p x✝
ι : Type ?u.403432
β : 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
intros
ι : Type ?u.403432
β : 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✝ : α
a✝ : x✝ ∈ s
⊢ ¬p x✝
ι : Type ?u.403432
β : 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✝ : α
a✝ : x✝ ∈ s
⊢ ¬p x✝
simp
case a
ι : Type ?u.403432
β : 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✝ : α
a✝ : x✝ ∈ s
⊢ x✝ ∈ s
ι : Type ?u.403432
β : 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✝ : α
a✝ : x✝ ∈ s
⊢ ¬p x✝
apply h
no goals
case a
ι : Type ?u.403432
β : 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✝ : α
a✝ : x✝ ∈ s
⊢ x✝ ∈ s
assumption