ι : Type ?u.881033
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g : α✝ → β✝
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : CommMonoid β
p : α → Prop
f : α → β
inst✝ : DecidablePred p
s : Finset α := Set.toFinset {x | p x}
⊢ (∏ i : { x // p x }, f ↑i) * ∏ i : { x // ¬p x }, f ↑i = ∏ i : α, f i
ι : Type ?u.881033
β✝ : Type u
α✝ : Type v
γ : Type w
s s₁ s₂ : Finset α✝
a : α✝
f✝ g : α✝ → β✝
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : CommMonoid β
p : α → Prop
f : α → β
inst✝ : DecidablePred p
⊢ (∏ i : { x // p x }, f ↑i) * ∏ i : { x // ¬p x }, f ↑i = ∏ i : α, f i
let s := { x | p x }.toFinset
ι : Type ?u.881033
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g : α✝ → β✝
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : CommMonoid β
p : α → Prop
f : α → β
inst✝ : DecidablePred p
s : Finset α := Set.toFinset {x | p x}
⊢ (∏ a in s, f a) * ∏ a in sᶜ, f a = ∏ i : α, f i

case h
ι : Type ?u.881033
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g : α✝ → β✝
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : CommMonoid β
p : α → Prop
f : α → β
inst✝ : DecidablePred p
s : Finset α := Set.toFinset {x | p x}
⊢ ∀ (x : α), x ∈ sᶜ ↔ ¬p x

case h
ι : Type ?u.881033
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g : α✝ → β✝
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : CommMonoid β
p : α → Prop
f : α → β
inst✝ : DecidablePred p
s : Finset α := Set.toFinset {x | p x}
⊢ ∀ (x : α), x ∈ s ↔ p x
ι : Type ?u.881033
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g : α✝ → β✝
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : CommMonoid β
p : α → Prop
f : α → β
inst✝ : DecidablePred p
s : Finset α := Set.toFinset {x | p x}
⊢ (∏ i : { x // p x }, f ↑i) * ∏ i : { x // ¬p x }, f ↑i = ∏ i : α, f i
rw [← Finset.prod_subtype s, ← Finset.prod_subtype (sᶜ)]
no goals
ι : Type ?u.881033
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g : α✝ → β✝
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : CommMonoid β
p : α → Prop
f : α → β
inst✝ : DecidablePred p
s : Finset α := Set.toFinset {x | p x}
⊢ (∏ a in s, f a) * ∏ a in sᶜ, f a = ∏ i : α, f i
exact Finset.prod_mul_prod_compl _ _
no goals
case h
ι : Type ?u.881033
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g : α✝ → β✝
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : CommMonoid β
p : α → Prop
f : α → β
inst✝ : DecidablePred p
s : Finset α := Set.toFinset {x | p x}
⊢ ∀ (x : α), x ∈ sᶜ ↔ ¬p x
simp
no goals
case h
ι : Type ?u.881033
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g : α✝ → β✝
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : CommMonoid β
p : α → Prop
f : α → β
inst✝ : DecidablePred p
s : Finset α := Set.toFinset {x | p x}
⊢ ∀ (x : α), x ∈ s ↔ p x
simp