theorem claim342_grid {α : Type u_1} [Field α] (β : ℝ) (A : Finset α) (B : Finset α) (L : Finset (Line α)) (n : ℕ+) (hB : ↑B.card ≤ 4 * ↑↑n ^ (1 / 2 + 2 * ST_prime_field_eps β)) (h₂ : L.card ≤ ↑n) (nHoriz : ∀ l ∈ L, ¬Line.horiz l) (nh : ↑SG_C₃ * ↑↑n ^ (3 / 2 - SG_eps β) < ↑(Intersections (A ×ˢ B) L).card) : ∃ b₁ ∈ B, ∃ b₂ ∈ B, b₁ ≠ b₂ ∧ ↑(Finset.filter (fun (l : Line α) => (∃ p ∈ A ×ˢ {b₁}, p ∈ l) ∧ ∃ p ∈ A ×ˢ {b₂}, p ∈ l) L).card > ↑SG_C₄ * ↑↑n ^ (1 - SG_eps₂ β)