try something else

.

src/Init/SimpLemmas.lean

@@ -66,6 +66,12 @@ theorem ite_congr {x y u v : α} {s : Decidable b} [Decidable c]
   | inl h => rw [if_pos h]; subst b; rw [if_pos h]; exact h₂ h
   | inr h => rw [if_neg h]; subst b; rw [if_neg h]; exact h₃ h
 
+-- Specialisation of `ite_congr` only descending into the condition,
+-- not the branches. We use this in `split_ifs`.
+theorem ite_congr_cond {s : Decidable b} [Decidable c]
+    (h : b = c) : ite b x y = ite c x y := by
+  simp [h]
+
 theorem Eq.mpr_prop {p q : Prop} (h₁ : p = q) (h₂ : q)  : p  := h₁ ▸ h₂
 theorem Eq.mpr_not  {p q : Prop} (h₁ : p = q) (h₂ : ¬q) : ¬p := h₁ ▸ h₂
 

src/Lean/Meta/Tactic/SplitIf.lean

@@ -19,12 +19,15 @@ builtin_initialize ext : LazyInitExtension MetaM Simp.Context ←
     s ← s.addConst ``dif_neg
     return {
       simpTheorems  := #[s]
-      congrTheorems := (← getSimpCongrTheorems)
+      -- We don't use the default `congr` lemmas here,
+      -- as this can result in unwanted simplification of the branches of `if` statements.
+      -- We only use `ite_congr_cond`, to descend into the condition.
+      congrTheorems := addSimpCongrTheoremEntry {} (← mkSimpCongrTheorem ``ite_congr_cond 1000)
       config        := { Simp.neutralConfig with dsimp := false }
     }
 
 /--
-  Default `Simp.Context` for `simpIf` methods. It contains all congruence theorems, but
+  Default `Simp.Context` for `simpIf` methods. It contains no congruence theorems, and
   just the rewriting rules for reducing `if` expressions. -/
 def getSimpContext : MetaM Simp.Context :=
   ext.get

tests/lean/3245.lean

@@ -0,0 +1,6 @@
+example (b1 b2 : Bool) :
+  (if b1 then 0 else (if b2 then 0 else if b2 then 42 else 0)) = 0 := by
+  split
+  · rfl
+  trace_state
+  · split <;> rfl

tests/lean/3245.lean.expected.out

@@ -0,0 +1,4 @@
+case inr
+b1 b2 : Bool
+h✝ : ¬b1 = true
+⊢ (if b2 = true then 0 else if b2 = true then 42 else 0) = 0