Mathlib late-2026 renames: if_pos, NoAtoms, mem_setOf_eq, measureReal_diff

Deprecations seen in Mathlib around Nov 2026. if_pos h becomes ite_eq_left h and if_neg h becomes ite_eq_right h (same argument, a drop-in rename via sed). MeasureTheory.NoAtoms becomes NullSingletonClass and still provides measure_singleton. Set.mem_setOf_eq becomes Set.mem_ofPred_eq, and Set.setOf_forall becomes Set.ofPred_forall. measureReal_diff becomes measureReal_sdiff, Set.mem_diff becomes Set.mem_sdiff, and integral_finset_sum becomes integral_finsetSum. Also, MeasurableSet.mono does not exist: for m ≤ m' apply the order directly, hle _ hs.