α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
⊢ (a ∈ if a ∈ s then some a else none) ↔ a ∈ s
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
⊢ a ∈ ↑(ofSet s) a ↔ a ∈ s
dsimp [ofSet]
no goals
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
⊢ (a ∈ if a ∈ s then some a else none) ↔ a ∈ s
split_ifs <;> simp [*]