case split on an element of a finset?

Stream: new members

[ROCKY KAMEN-RUBIO]

I feel like there should be an easy way to do this but I can't find it.

import tactic
import data.finset
example {α : Type*} {y y1 y2 : α} {h : y ∈ ({y1, y2} : finset α )} : y = y1 ∨ y = y2 :=
begin
  sorry
end

[Kenny Lau]

just cases on h

[Kenny Lau]

or just finset.mem_insert

[ROCKY KAMEN-RUBIO]

cases h gives me a cases tactic failed, it is not applicable to the given hypothesis error.

import data.finset
import tactic
example {α : Type*} {y y1 y2 : α} {h : y ∈ ({y1, y2} : finset α )} : y = y1 ∨ y = y2 :=
begin
  --rw finset.mem_insert at h,
  cases h,
  sorry,
end

This works for me though

import tactic
import data.finset
example {α : Type*} {y y1 y2 : α} {h : y ∈ ({y1, y2} : finset α )} : y = y1 ∨ y = y2 :=
begin
  rw finset.mem_insert at h,
  cases h,
  {left, exact h},
  rw finset.mem_singleton at h,
  right
end

[Kenny Lau]

well I'm glad you found a way

[Kenny Lau]

fin_cases might help

[Kenny Lau]

oh the statement doesn't even compile because you need decidable_eq for the set notation

[Kenny Lau]

but it still doesn't work

[Kenny Lau]

import data.finset
import tactic

example {α : Type*} [decidable_eq α] {y y1 y2 : α} {h : y ∈ ({y1, y2} : finset α )} : y = y1 ∨ y = y2 :=
begin
  fin_cases h,
  sorry,
end

[Kenny Lau]

@Scott Morrison why doesn't this work?

[Kenny Lau]

cases tactic failed, it is not applicable to the given hypothesis
state:
α : Type ?,
_inst_1 : decidable_eq α,
y y1 y2 : α,
h : y ∈ {y1, y2}
⊢ y = y1 ∨ y = y2

[Scott Morrison]

a bug, I guess! :-) I'm not immediately sure. I can try to look tomorrow.

[Rob Lewis]

I dunno about fin_cases but this should just be simpa using h, right?