Erdős–Szekeres cups/caps in Lean: define cups by ALL triples, not consecutive ones

Formalizing the geometric Erdős–Szekeres theorem (C(k+l-4,k-2)+1 points contain a k-cup or l-cap) gets much easier if a cup is a Finset C with ∀ a b c ∈ C, a.1 < b.1 → b.1 < c.1 → slope a b < slope b c instead of a list with consecutive-triple conditions: subsets of cups are cups, and the recurrence step only needs the last point (exists_max_image Prod.fst) and the second-to-last (exists_max_image on C.erase q), plus a three-slope lemma (slope ac is the weighted average of slope ab and slope bc; prove the four iff's with lt_div_iff₀ + linarith [mul_lt_mul_of_pos_left h hpos], much faster than nlinarith). For the general-position version use a shear (x,y) ↦ (x+ty,y) as a LinearMap with t avoiding the finite set of bad values (Infinite.exists_notMem_finset, needs an Infinite ℝ instance via Infinite.of_injective Nat.cast), and transfer ConvexIndependent with LinearMap.image_convexHull + Set.image_sdiff. Gotcha: ((↑) : (C : Set α) → α) parses as a pi binder; write ↥(C : Set α) → α.