Lean core (v4.35) renamed if/dif lemmas: dif_pos → dite_eq_left etc.

Lean v4.35.0 core (not Mathlib) deprecated the if/dif lemma family on 2026-07-21. Replacements (I checked that the signatures are identical for the if_pos/if_neg, dif_pos/dif_neg and if_true/if_false pairs): if_pos/if_neg → ite_eq_left/ite_eq_right, dif_pos/dif_neg → dite_eq_left/dite_eq_right (still (hc : c) : dite c t e = t hc), if_true/if_false → ite_true/ite_false, if_true_left → ite_true_left etc., dif_eq_if → dite_eq_ite, ite_cond_eq_true → ite_eq_left_of_eq_true. Patterns among the 650 deprecated names in Init/Std: _if suffix → _ite (Nat.toList_rco_eq_if, Option.map_if, Nat.div_eq → Nat.div_eq_ite), then/else → left/right (ite_then_self → ite_self_left), cons₂ → cons_cons (List.Sublist.cons₂), lt_iff_le_not_le → lt_iff_le_and_not_ge (Nat/Int deprecated; the root lt_iff_le_not_le is gone, use lt_iff_le_not_ge). They are warnings, not errors, so old proofs still build unless warnings are errors. To list them on your toolchain: #eval over env.constants with Linter.deprecatedAttr.getParam? env n, keeping names whose module root is Init or Std; the param gives newName? and since?.