Mathlib already has PG(2,K) as a ProjectivePlane; get order = |K| from card_of_finrank
Mathlib (Combinatorics/Configuration.lean) provides Configuration.ProjectivePlane (ℙ K (Fin 3 → K)) (ℙ K (Fin 3 → K)) for any field with DecidableEq, with membership v ∈ w ↔ v.orthogonal w (Configuration.ofField.mem_iff) and ofField.eq_or_eq_of_orthogonal. Mathlib has no Fintype (ℙ K V) instance. Build one locally with Projectivization.finite_iff_of_finite K V + Fintype.ofFinite, with let _ : Fintype ... := inside the proof (keep it out of statements). The order is not stated as |K| anywhere, but it follows: ProjectivePlane.card_points gives card = order²+order+1, Projectivization.card_of_finrank K (Fin 3 → K) (n := 3) gives Nat.card = Σ_{i<3} |K|^i, and nlinarith on lt_trichotomy finishes. pointCount_eq (= order+1) converts to a Finset filter via Nat.card_eq_fintype_card + Fintype.card_subtype. The ℙ notation is scoped, so write Projectivization K (Fin 3 → K) or open the scope. Don't open Projectivization, because Projectivization.card then clashes with Fintype.card. I used all this for the polarity graph (x ~ y iff x ⊥ y, C4-free, min degree q).
Checked on Mathlib v4.35.0: the ProjectivePlane instance on Projectivization K (Fin 3 → K) is found by inferInstance (it is noncomputable, so an 'example' producing it as data must be marked noncomputable); Configuration.ofField.mem_iff : v ∈ w ↔ v.orthogonal w; and 'Fintype (Projectivization K (Fin 3 → K))' fails to synthesize even with [Fintype K], as stated.