case inl
ι : Type ?u.870155
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoidWithZero β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h : ∀ (i : α), i ∈ s → p i
⊢ (∏ i in s, if p i then 1 else 0) = 1

case inr
ι : Type ?u.870155
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoidWithZero β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h : ¬∀ (i : α), i ∈ s → p i
⊢ (∏ i in s, if p i then 1 else 0) = 0
ι : Type ?u.870155
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoidWithZero β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
⊢ (∏ i in s, if p i then 1 else 0) = if ∀ (i : α), i ∈ s → p i then 1 else 0
split_ifs with h
case inl.h
ι : Type ?u.870155
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoidWithZero β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h : ∀ (i : α), i ∈ s → p i
⊢ ∀ (x : α), x ∈ s → (if p x then 1 else 0) = 1
case inl
ι : Type ?u.870155
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoidWithZero β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h : ∀ (i : α), i ∈ s → p i
⊢ (∏ i in s, if p i then 1 else 0) = 1
apply prod_eq_one
case inl.h
ι : Type ?u.870155
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoidWithZero β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h : ∀ (i : α), i ∈ s → p i
i : α
hi : i ∈ s
⊢ (if p i then 1 else 0) = 1
case inl.h
ι : Type ?u.870155
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoidWithZero β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h : ∀ (i : α), i ∈ s → p i
⊢ ∀ (x : α), x ∈ s → (if p x then 1 else 0) = 1
intro i hi
no goals
case inl.h
ι : Type ?u.870155
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoidWithZero β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h : ∀ (i : α), i ∈ s → p i
i : α
hi : i ∈ s
⊢ (if p i then 1 else 0) = 1
rw [if_pos (h i hi)]
case inr
ι : Type ?u.870155
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoidWithZero β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h : ∃ i, i ∈ s ∧ ¬p i
⊢ (∏ i in s, if p i then 1 else 0) = 0
case inr
ι : Type ?u.870155
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoidWithZero β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h : ¬∀ (i : α), i ∈ s → p i
⊢ (∏ i in s, if p i then 1 else 0) = 0
push_neg  at h
case inr.intro.intro
ι : Type ?u.870155
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoidWithZero β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
i : α
hi : i ∈ s
hq : ¬p i
⊢ (∏ i in s, if p i then 1 else 0) = 0
case inr
ι : Type ?u.870155
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoidWithZero β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h : ∃ i, i ∈ s ∧ ¬p i
⊢ (∏ i in s, if p i then 1 else 0) = 0
rcases h with ⟨i, hi, hq⟩
case inr.intro.intro
ι : Type ?u.870155
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoidWithZero β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
i : α
hi : i ∈ s
hq : ¬p i
⊢ (if p i then 1 else 0) = 0
case inr.intro.intro
ι : Type ?u.870155
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoidWithZero β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
i : α
hi : i ∈ s
hq : ¬p i
⊢ (∏ i in s, if p i then 1 else 0) = 0
apply prod_eq_zero hi
no goals
case inr.intro.intro
ι : Type ?u.870155
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoidWithZero β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
i : α
hi : i ∈ s
hq : ¬p i
⊢ (if p i then 1 else 0) = 0
rw [if_neg hq]