equality/inequality in subtype

Stream: new members

[Heather Macbeth]

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]

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]

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]

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

[Patrick Massot]

Oh Kevin had the same cheating idea.

[Kevin Buzzard]

rintro rfl is a really good way to hide rewrites

[Patrick Massot]

(hiding the rw in rintro)

[Patrick Massot]

:big_smile:

[Patrick Massot]

And none of this is really answering the initial question.

[Heather Macbeth]

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]

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]

Using an already proven lemma is always the ultimate cheating.

[Heather Macbeth]

Somehow library_search doesn't find that for me?

[Patrick Massot]

It may be because of the negation bug in library_search

[Eric Wieser]

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