## Stream: new members

### Topic: equality/inequality in subtype

#### Heather Macbeth (Dec 29 2020 at 17:53):

What is the idiomatic way to do something like this?

import data.set.basic

example {E : Type*} (s : set E) (a : E) (b : s) (ha : a ∈ s) (h : ↑b ≠ a) : b ≠ ⟨a, ha⟩ :=
sorry


I can think of a couple of ways:

import data.set.basic

example {E : Type*} (s : set E) (a : E) (b : s) (ha : a ∈ s) (h : ↑b ≠ a) : b ≠ ⟨a, ha⟩ :=
begin
intros h',
apply h,
rw h',
refl,
end

example {E : Type*} (s : set E) (a : E) (b : s) (ha : a ∈ s) (h : ↑b ≠ a) : b ≠ ⟨a, ha⟩ :=
begin
intros h',
apply h,
cases h',
refl,
end


but I feel like it ought to be a one-liner?

#### Kevin Buzzard (Dec 29 2020 at 17:59):

mt jumps you a step:

example {E : Type*} (s : set E) (a : E) (b : s) (ha : a ∈ s) (h : ↑b ≠ a) : b ≠ ⟨a, ha⟩ :=
mt begin intro h2, rw h2, refl end h


but there's still that rewrite.

#### Kevin Buzzard (Dec 29 2020 at 18:00):

example {E : Type*} (s : set E) (a : E) (b : s) (ha : a ∈ s) (h : ↑b ≠ a) : b ≠ ⟨a, ha⟩ :=
mt (by {rintro rfl, refl}) h


#### Patrick Massot (Dec 29 2020 at 18:01):

by {  rintro ⟨h, rfl⟩, exact h rfl }


#### Patrick Massot (Dec 29 2020 at 18:01):

Oh Kevin had the same cheating idea.

#### Kevin Buzzard (Dec 29 2020 at 18:02):

rintro rfl is a really good way to hide rewrites

#### Patrick Massot (Dec 29 2020 at 18:02):

(hiding the rw in rintro)

:big_smile:

#### Patrick Massot (Dec 29 2020 at 18:02):

And none of this is really answering the initial question.

#### Heather Macbeth (Dec 29 2020 at 18:03):

Patrick Massot said:

by {  rintro ⟨h, rfl⟩, exact h rfl }


I like this one, I think it's good enough. But I was hoping that there was something slick, like maybe a fancy use of norm_cast.

#### Kenny Lau (Dec 29 2020 at 18:03):

import data.set.basic

lemma idiomatic {E : Type*} (s : set E) (a : E) (b : s) (ha : a ∈ s) (h : ↑b ≠ a) : b ≠ ⟨a, ha⟩ :=
subtype.ne_of_val_ne h


#### Patrick Massot (Dec 29 2020 at 18:04):

Using an already proven lemma is always the ultimate cheating.

#### Heather Macbeth (Dec 29 2020 at 18:05):

Somehow library_search doesn't find that for me?

#### Patrick Massot (Dec 29 2020 at 18:05):

It may be because of the negation bug in library_search

#### Eric Wieser (Dec 29 2020 at 22:31):

docs#subtype.ne_of_val_ne is defeq but not syntactically eq, which is probably why library_search is of no help

Last updated: Dec 20 2023 at 11:08 UTC