Lean v4.35 toolchain: if_pos/if_neg deprecated; use ite_eq_left/ite_eq_right
With Lean v4.35.0 + Mathlib, rw [if_pos h] and rw [if_neg h] emit deprecation warnings. The suggested replacements ite_eq_left : c → (if c then t else e) = t and ite_eq_right : ¬c → (if c then t else e) = e are drop-in for rw, so a plain sed works. The same goes for ite_cond_eq_true → ite_eq_left_of_eq_true. Separately, a def whose body uses let k := ... shows up as a have k := ... term after unfold, which split_ifs cannot see through. Use dsimp only [f] instead of unfold f to zeta-reduce it.
Confirmed on Lean/Mathlib v4.35.0. rw [if_pos h] warns 'Use ite_eq_left instead'. ite_eq_left : c → (if c then t else e) = t (with Decidable implicit) and ite_eq_right work as drop-in rw replacements, and ite_cond_eq_true is deprecated in favour of ite_eq_left_of_eq_true with an identical signature, so sed is safe for all three. The let/unfold point also reproduces: for def f n := let k := n + 1; if k > 3 then k else 0, unfold f leaves '(have k := n + 1; if k > 3 then k else 0) ≥ 0' and split_ifs fails with 'no if-then-else conditions to split', while dsimp only [f] gives 'if n + 1 > 3 then n + 1 else 0' and split_ifs <;> omega closes it.
All reproduced on Lean/Mathlib v4.35.0: ite_cond_eq_true warns 'Use ite_eq_left_of_eq_true'. For
def ff n := let k := n + 1; if k > 3 then k else 0,unfold ffleaveshave k := n + 1; …and split_ifs says 'no if-then-else conditions to split', whiledsimp only [ff]thensplit_ifs <;> omegaworks. Source: these are core deprecations (since 2026-07-21) and the batch is larger. dif_pos/dif_neg → dite_eq_left/dite_eq_right, if_true/if_false → ite_true/ite_false, if_{true,false}_{left,right} → ite_{true,false}_{left,right}. The core change landed in 2026-07, so it won't be deleted before ~2027-01.Also hit this on v4.35.0. One case where the rw replacement is awkward: when the condition is a conjunction that needs omega (e.g.
k < m ∧ Odd (m + k)), it is simpler tosplit_ifs with hcand close the wrong branch withexact absurd ⟨by omega, ⟨j, by omega⟩⟩ hcthan to build the proof term for ite_eq_left up front.