case mp
α : Type u_1
β : Type ?u.5585
γ : Type ?u.5588
o : Part α
⊢ o ≠ none → ∃ x, o = some x

case mpr
α : Type u_1
β : Type ?u.5585
γ : Type ?u.5588
o : Part α
⊢ (∃ x, o = some x) → o ≠ none
α : Type u_1
β : Type ?u.5585
γ : Type ?u.5588
o : Part α
⊢ o ≠ none ↔ ∃ x, o = some x
constructor
case mp
α : Type u_1
β : Type ?u.5585
γ : Type ?u.5588
o : Part α
⊢ o.Dom → ∃ x, o = some x
case mp
α : Type u_1
β : Type ?u.5585
γ : Type ?u.5588
o : Part α
⊢ o ≠ none → ∃ x, o = some x
rw [Ne, eq_none_iff', not_not]
no goals
case mp
α : Type u_1
β : Type ?u.5585
γ : Type ?u.5588
o : Part α
⊢ o.Dom → ∃ x, o = some x
exact fun h => ⟨o.get h, eq_some_iff.2 (get_mem h)⟩
case mpr.intro
α : Type u_1
β : Type ?u.5585
γ : Type ?u.5588
x : α
⊢ some x ≠ none
case mpr
α : Type u_1
β : Type ?u.5585
γ : Type ?u.5588
o : Part α
⊢ (∃ x, o = some x) → o ≠ none
rintro ⟨x, rfl⟩
no goals
case mpr.intro
α : Type u_1
β : Type ?u.5585
γ : Type ?u.5588
x : α
⊢ some x ≠ none
apply some_ne_none