import tactic.split_ifs
import tactic.localized

open_locale classical

example (P Q : Prop) (w : if P then (if Q then true else true) else true = true) : true :=
begin
  split_ifs at w,
  -- 3 goals, no `if`s in `w`
  all_goals { trivial, }
end

import Mathlib.Tactic.SplitIfs

open Classical

example (P Q : Prop) (w : if P then (if Q then true else true) else true = true) : true := by
  split_ifs at w
  -- two goals here, and in the first `w : if Q then true else true`