option golf puzzle

Stream: general

[Kevin Buzzard]

I ran into this in the middle of a tactic mode proof and it took me an annoying number of lines:

import data.set.basic

example (α : Type) (S : set (option α)) (hS : S ≠ ∅) (h : none ∉ S) :
(coe ⁻¹' S : set α) ≠ ∅ :=
begin
  intro h1,
  apply hS,
  ext x,
  cases x, simpa using h,
  show x ∈ (coe ⁻¹' S : set α) ↔ _,
  rw h1,
  refl
end

Can I use some automation here? (or any other way of reducing the line-count) [hmm: set.ne_empty_iff_exists_mem looks helpful. ] [update: I'm about to do this myself now]

[Kevin Buzzard]

import data.set.basic

example (α : Type) (S : set (option α)) (hS : S ≠ ∅) (h : none ∉ S) :
(coe ⁻¹' S : set α) ≠ ∅ :=
begin
  rcases (set.exists_mem_of_ne_empty hS) with ⟨⟨⟩|a, ha⟩, contradiction,
  rw set.ne_empty_iff_exists_mem,
  exact ⟨a, ha⟩,
end

This is probably preferable. I was barking up the wrong tree thinking about automation perhaps (unless there's some one line automation proof)

[Patrick Massot]

example (α : Type) (S : set (option α)) (hS : S ≠ ∅) (h : none ∉ S) :
(coe ⁻¹' S : set α) ≠ ∅ :=
begin
  rw set.ne_empty_iff_exists_mem at *,
  rcases hS with ⟨_| _, _⟩ ; tauto
end

[Kevin Buzzard]

Thanks for this Patrick. I am doing some abstract nonsense with lattices and I suspect I am underusing tauto.

[Kevin Buzzard]

Hmm...I am suddenly not sure if I'm allowed to import tauto in order/complete_lattice.lean...

[Patrick Massot]

In any case, we don't want to read the proof of that lemma, so you could as well use an unreadable proof term (preferably hand-crafted rather that copy-pasted from tauto).

[Mario Carneiro]

I like kevin's second proof best. Short and no advanced dependencies

[Patrick Massot]

My message was in the context of Kevin's question: "can we automate this?". I still think a proof term is probably the most relevant proof here.

[Kevin Buzzard]

You're probably right for this example but in the PR I'm in tactic mode because I've just done split_ifs and it's somehow hard to exit -- or at least I feel it is. I'm always happy to hear about ways I can improve my code-writing, for me the goal has always been to prove the theorem and who cares if it's pretty, but I am slowly beginning to care more about the code I'm writing.