split_ifs and has_mem.mem

Stream: new members

[Patrick Johnson]

The goal is definitionally equal to ite (odd n) 1 0 < 2, so split_ifs should work, but it doesn't. What is the simplest way to reduce the goal to something that split_ifscan recognize?

import tactic
open_locale classical

example {f : ℕ → ℕ} {n : ℕ}
  (h : f = λ (n : ℕ), ite (odd n) 1 0) :
  n ∈ {i | f i < 2} :=
begin
  subst h,
  split_ifs,
end

[Alex J. Best]

tactic#dsimp

[Patrick Massot]

I'm afraid there is no general magic answer. You can use change with underlines to make it less painful. As in change ite _ _ _ < _,