Handling `ite`s

Stream: lean4

[Marcus Rossel]

How can I split on an ite in Lean 4?
I have an assumption h : if x then y else z and would like to split into two subgoals.

[Scott Morrison]

import Mathlib.Tactic.Basic

example (P : Prop) [Decidable P] : (if P then 0 else 0) = 0 := by
  by_cases P
  rw [if_pos h]
  rw [if_neg h]

[Scott Morrison]

(I'd like to port split_ifs soonish.)

[Scott Morrison]

You can rw [if_pos h] at w to resolve an if in a hypothesis, of course.