Zulip Chat Archive

Stream: new members

Topic: split_ifs and has_mem.mem


Patrick Johnson (Dec 13 2021 at 21:31):

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 (Dec 13 2021 at 21:33):

tactic#dsimp

Patrick Massot (Dec 13 2021 at 21:34):

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


Last updated: Dec 20 2023 at 11:08 UTC