finset.erase_singleton_self

Stream: Is there code for X?

[Kenny Lau]

import data.finset

universe u

theorem finset.erase_singleton_self {α : Type u} [decidable_eq α] (x : α) : ({x} : finset α).erase x = ∅ :=
sorry

[Scott Morrison]

theorem finset.erase_singleton_self {α : Type u} [decidable_eq α] (x : α) : ({x} : finset α).erase x = ∅ :=
begin
  ext y,
  split,
  { intro h,
    simp at h,
    contradiction, },
  { rintro ⟨⟩, }
end

it seems it should go in the library, as a @[simp] lemma

[Bryan Gin-ge Chen]

I'm surprised it's not already there!

[Mario Carneiro]

probably the move from insert to singleton was a factor

[Bhavik Mehta]

Not at a computer right now but I think there should be an easier proof using insert_eq and erase_insert?

[Bhavik Mehta]

open finset

theorem finset.erase_singleton_self {α : Type u} [decidable_eq α] (x : α) : ({x} : finset α).erase x = ∅ :=
by rw [← insert_emptyc_eq, erase_insert (not_mem_empty x)]

[Kenny Lau]

[Kenny Lau]

????

[Kenny Lau]

https://github.com/leanprover-community/lean/blob/970d47ce28b1637375a76f490339baffa165fc2c/library/init/core.lean#L404-L409

class is_lawful_singleton (α : Type u) (β : Type v) [has_emptyc β] [has_insert α β]
  [has_singleton α β] :=
(insert_emptyc_eq : ∀ (x : α), (insert x ∅ : β) = {x})

export has_singleton (singleton)
export is_lawful_singleton (insert_emptyc_eq)

[Kenny Lau]

those damn exports