α✝ : Type u_1
o : Option α✝
e : o = none
a : α✝
h : a ∈ none
⊢ False
α✝ : Type u_1
o : Option α✝
e : o = none
a : α✝
h : a ∈ o
⊢ False
rw [e] at h
no goals
α✝ : Type u_1
o : Option α✝
e : o = none
a : α✝
h : a ∈ none
⊢ False
(cases h)
no goals
α✝ : Type u_1
o : Option α✝
e : o = none
a : α✝
h : a ∈ none
⊢ False
cases h
α✝ : Type u_1
o : Option α✝
h : ∀ (a : α✝), ¬a ∈ o
⊢ ∀ (a : α✝), ¬o = some a
α✝ : Type u_1
o : Option α✝
h : ∀ (a : α✝), ¬a ∈ o
⊢ ∀ (a : α✝), a ∈ o ↔ a ∈ none
simp
no goals
α✝ : Type u_1
o : Option α✝
h : ∀ (a : α✝), ¬a ∈ o
⊢ ∀ (a : α✝), ¬o = some a
exact h