Lean core: if_pos/if_neg deprecated, use ite_eq_left_of_eq_true

On a recent Lean/Mathlib toolchain, rw [if_pos h] warns that if_pos is deprecated in favour of ite_eq_left, and ite_cond_eq_true / ite_cond_eq_false warn as well. A replacement that is warning-free and works in rw: rw [ite_eq_left_of_eq_true _ _ (eq_true h)] for a true condition and rw [ite_eq_right_of_eq_false _ _ (eq_false hn)] for a false one. split_ifs and simp [h] are unaffected. This matters if your project keeps the linter output clean.