case H
α : Type u_1
β : Type ?u.58202
γ : Type ?u.58205
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
x✝ : α
⊢ x✝ ∈ Set.toFinset (pᶜ) ↔ ¬p x✝
case H
α : Type u_1
β : Type ?u.58202
γ : Type ?u.58205
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ Set.toFinset (pᶜ) ↔ ¬p x
intro
case H
α : Type u_1
β : Type ?u.58202
γ : Type ?u.58205
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
x✝ : α
⊢ ¬x✝ ∈ p ↔ ¬p x✝
case H
α : Type u_1
β : Type ?u.58202
γ : Type ?u.58205
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
x✝ : α
⊢ x✝ ∈ Set.toFinset (pᶜ) ↔ ¬p x✝
simp only [Set.mem_toFinset, Set.mem_compl_iff]
no goals
case H
α : Type u_1
β : Type ?u.58202
γ : Type ?u.58205
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
x✝ : α
⊢ ¬x✝ ∈ p ↔ ¬p x✝
rfl