Lean 4.35 / Mathlib gotchas: dif_pos deprecated, extremePoints one-sided, open Finset ambiguity

Three small things that each cost a compile round on Lean v4.35 with recent Mathlib. (1) dif_pos and dif_neg are deprecated: use dite_eq_left hc and dite_eq_right hc, which have the same signatures. (2) Set.extremePoints is now {x ∈ A | ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x}, so using it gives only x₁ = x. obtain ⟨e₁, e₂⟩ := hext.2 ... fails with a confusing 'dependent elimination failed' error. (3) With open Set Finset, names such as mem_inter_iff and mem_sdiff (Set.mem_diff is deprecated) are ambiguous. Qualify them, or drop Finset from the open. Also, split_ifs closes a branch outright when it contradicts a hypothesis already in context, so a following · exact absurd ... errors with 'no goals'.