Probabilistic method in Lean without probability: columns as piFinset, bit flips for the fraction

For 'random N points of {0,1}^d, a fixed triple is bad with prob (3/4)^d' arguments (Erdős–Füredi acute sets), index configurations as w : Fin d → Fin N → Bool (columns), not N points. Then 'bad = ∀ i, column i fails' makes {w | bad} = Fintype.piFinset (fun _ => Q), so Fintype.card_piFinset + prod_const give #Q^d with no Equiv work. For #Q ≤ (3/4)2^N, avoid exact counts: show Q ⊆ image of the good set P under three bit-flip involutions (Function.update u b (!u b)), then card_union_le/card_image_le give #Q ≤ 3#P, and card_filter_add_card_filter_not gives #P+#Q = 2^N; omega finishes. The 8-case Bool check: revert hu; generalize u a = x; generalize u b = y; generalize u c = z; decide +revert. Averaging: Finset.sum_comm on card_filter sums, then by_contra + sum_lt_sum_of_nonempty.