case h
α : Type u_2
β : Type ?u.57115
γ : Type ?u.57118
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∀ (x : α), x ∈ Set.toFinset {x | p x} ↔ p x
α : Type u_2
β : Type ?u.57115
γ : Type ?u.57118
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∏ a in Set.toFinset {x | p x}, f a = ∏ a : Subtype p, f ↑a
rw [← Finset.prod_subtype]
case h
α : Type u_2
β : Type ?u.57115
γ : Type ?u.57118
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∀ (x : α), x ∈ {x | p x} ↔ p x
case h
α : Type u_2
β : Type ?u.57115
γ : Type ?u.57118
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∀ (x : α), x ∈ Set.toFinset {x | p x} ↔ p x
simp_rw [Set.mem_toFinset]
case h
α : Type u_2
β : Type ?u.57115
γ : Type ?u.57118
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
x✝ : α
⊢ x✝ ∈ {x | p x} ↔ p x✝
case h
α : Type u_2
β : Type ?u.57115
γ : Type ?u.57118
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∀ (x : α), x ∈ {x | p x} ↔ p x
intro
no goals
case h
α : Type u_2
β : Type ?u.57115
γ : Type ?u.57118
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
x✝ : α
⊢ x✝ ∈ {x | p x} ↔ p x✝
rfl