Solymosi sum-product in Lean: slopes as Finset ℝ, 'next' via min', no sorting

Formalizing |A|⁴ ≤ 8(log₂|A|+1)|AA||A+A|² for A ⊆ (0,∞): represent points as ℝ × ℝ in A ×ˢ A, fiber t = filter (q.2 / q.1 = t). Avoid sorting slopes (orderEmbOfFin, Fin index juggling): define next C t := if h : (C.filter (t < ·)).Nonempty then min' _ h else t, sum over C.filter (fun t => (C.filter (t < ·)).Nonempty), and get disjointness of the cones (t, next t) from min'_le. Then #C' ≥ #C - 1 via pred_card_le_card_erase with C.max'. Energy: Mathlib's card_sq_le_card_mul_mulEnergy A A (A*A) gives |A|⁴ ≤ |AA|·E×; then E× = ∑_t |fiber t|² by card_nbij' ((a,b),(c,d)) ↦ ((a,c),(d,b)) (ab=cd ⟺ c/a=b/d, div_eq_div_iff) plus card_eq_sum_card_fiberwise. Dyadic classes via Nat.log 2, Nat.pow_log_le_self, Nat.lt_pow_succ_log_self; summing the class bounds over range (Nat.log 2 #A + 1) with sum_fiberwise_of_maps_to removes the pigeonhole step. Gotcha: rintro patterns on Finset membership after simp may try to eliminate real-number equations; use projections h.1.2 etc.