Custom cases

Stream: new members

[Gareth Ma]

Hi. I have the following code:

example {p : ℚ[X]} (h : p = (3 / 2) * X ^ 2 + 1) : p.support = {0, 2} :=
begin
  rw finset.ext_iff,
  intro a, -- a ∈ p.support ↔ a ∈ {0, 2}
end

And I would like to prove the goal by applying cases, splitting on whether a ∈ {0, 2} or not. How can I do this?
(My plan afterwards it to split the polynomial into sum of many monomials, then p.coeff n = sum (pi.coeff n), which is 0 if n is not in {0, 2}.

[Kevin Buzzard]

by_cases h : a \in {0,2}

[Kevin Buzzard]

But there's little point splitting on this because it's one of the sides of the iff. Just do split.