α : Type u_1
β : Type ?u.7431
γ : Type ?u.7434
o : Part α
inst✝ : Decidable o.Dom
a : α
⊢ (a ∈ if h : o.Dom then Option.some (get o h) else Option.none) ↔ a ∈ o
α : Type u_1
β : Type ?u.7431
γ : Type ?u.7434
o : Part α
inst✝ : Decidable o.Dom
a : α
⊢ a ∈ toOption o ↔ a ∈ o
unfold toOption
case pos
α : Type u_1
β : Type ?u.7431
γ : Type ?u.7434
o : Part α
inst✝ : Decidable o.Dom
a : α
h : o.Dom
⊢ get o (_ : o.Dom) = a ↔ a ∈ o

case neg
α : Type u_1
β : Type ?u.7431
γ : Type ?u.7434
o : Part α
inst✝ : Decidable o.Dom
a : α
h : ¬o.Dom
⊢ ¬a ∈ o
α : Type u_1
β : Type ?u.7431
γ : Type ?u.7434
o : Part α
inst✝ : Decidable o.Dom
a : α
⊢ (a ∈ if h : o.Dom then Option.some (get o h) else Option.none) ↔ a ∈ o
by_cases h : o.Dom <;> simp [h]
no goals
case pos
α : Type u_1
β : Type ?u.7431
γ : Type ?u.7434
o : Part α
inst✝ : Decidable o.Dom
a : α
h : o.Dom
⊢ get o (_ : o.Dom) = a ↔ a ∈ o
exact ⟨fun h => ⟨_, h⟩, fun ⟨_, h⟩ => h⟩
no goals
case neg
α : Type u_1
β : Type ?u.7431
γ : Type ?u.7434
o : Part α
inst✝ : Decidable o.Dom
a : α
h : ¬o.Dom
⊢ ¬a ∈ o
exact mt Exists.fst h