## Stream: new members

### Topic: none ≠ some

#### Marcus Rossel (Jan 13 2021 at 08:06):

I have the following goal state and don't know how to continue:

v: value
⊢ ¬none = ↑v


If I understand this correctly, I'm supposed to prove ¬ none = some v. I thought simp would handle that, but it doesn't.
How can I resolve this?

#### Johan Commelin (Jan 13 2021 at 08:20):

@Marcus Rossel there should be a lemma option.some_ne_none. Alternatively, you can close this with option.no_confusion.

#### Johan Commelin (Jan 13 2021 at 08:21):

Have you tried library_search?

#### Marcus Rossel (Jan 13 2021 at 08:25):

Johan Commelin said:

Have you tried library_search?

Yeah, it couldn't come up with anything, which seems odd.

#### Eric Wieser (Jan 13 2021 at 08:27):

What if you change the goal to be expressed using some instead of a coercion?

#### Marcus Rossel (Jan 13 2021 at 08:35):

Eric Wieser said:

What if you change the goal to be expressed using some instead of a coercion?

The coercion was introduced by Lean itself. The proposition where v comes from explicitly uses some v.

#### Kevin Buzzard (Jan 13 2021 at 08:38):

You can use change to change it to some.

#### Marcus Rossel (Jan 13 2021 at 08:48):

Kevin Buzzard said:

You can use change to change it to some.

Like this change ↑v with (some v)? Because that just introduces two subgoals for me:

example {value : Type*} (v : value) :
¬ (none : (option value)) = ↑v :=
begin
change ↑v with (some v),
-- 1: ⊢ ¬none = ↑v
-- 2: ⊢ has_lift_t value (option value)
end


#### Johan Commelin (Jan 13 2021 at 08:49):

change \not none = some v

#### Johan Commelin (Jan 13 2021 at 08:51):

example {value : Type*} (v : value) :
¬ (none : (option value)) = ↑v :=
begin
apply option.no_confusion
end


#### Yakov Pechersky (Jan 13 2021 at 14:52):

Perhaps 'coe_eq_some' should be a simp lemma

#### Johan Commelin (Jan 13 2021 at 14:58):

Hmm, shouldn't the other direction be a simp-lemma?

#### Eric Wieser (Jan 13 2021 at 15:32):

I think we have a lot of simp lemmas that the linter will complain about if some stopped being simp-normal

Last updated: May 08 2021 at 09:11 UTC