Deconstructing existential statements

Stream: new members

[Trevor Hyde]

I'm confused about why Lean gets upset if I remove the simp at hy line in the code below? I know I don't need both the have and the cases' lines, I was just testing to see if they behave differently.

open scoped Classical
variable (X Y : Type) (f : X → Y)

example (S T : Finset X) (h : S ≤ T) : S.image f ≤ T.image f := by
  intro y hy
  simp at hy

  -- These both work after `simp at hy`, but won't work without it.
  have ⟨x,hx⟩ := hy
  cases' hy with x hx
  done

[spamegg]

Is this Lean3 by any chance? It does not compile on the playground.

[Julian Berman]

It's just missing the imports . With import Mathlib, after the intro it looks like hy says y ∈ Finset.image f S -- and this isn't quite the same as saying there exists such an x, that's a lemma relating those, which simp is applying (or which you could rewrite with yourself).

[Julian Berman]

docs#Finset.mem_image

[Kevin Buzzard]

Yeah for sets this is rfl but for finsets it's not.