α : Type u_1
s : Set α
x : α
⊢ ¬x ∈ s ↔ (if x ∈ s then true else false) = false
α : Type u_1
s : Set α
x : α
⊢ ¬x ∈ s ↔ boolIndicator s x = false
unfold boolIndicator
no goals
α : Type u_1
s : Set α
x : α
⊢ ¬x ∈ s ↔ (if x ∈ s then true else false) = false
split_ifs with h <;> simp [h]