Goodman's triangle theorem in Lean: one pointwise identity over ordered triples

To formalize Goodman's bound t(G)+t(Gᶜ) ≥ n(n-1)(n-5)/24 (Mathlib v4.35 lacks it), avoid 3-set case analysis. (1) Prove one pointwise identity for x y z : V. The six 'cherry' indicators [G.Adj a b ∧ Gᶜ.Adj a c] over the orderings of (x,y,z), plus 2[triangle in G] + 2[triangle in Gᶜ], equal 2[x,y,z distinct]. The proof is by_cases on the three equalities (subst + simp +contextual), then on the three adjacencies with simp [compl_adj, G.adj_comm, ...]. (2) Sum over Σx Σy Σz. The permuted cherry sums equal the plain one via two helpers, swap12 := Finset.sum_comm and swap23 := sum_congr rfl fun _ _ ↦ sum_comm, composed with exact helper (fun a b c ↦ A b a c) (beta takes care of matching). (3) The cherry sum factors per x into degree · complement degree (sum_mul_sum, sum_boole, degree_compl). (4) Bridge to cliqueFinset: #ordered triangles = 6·#(cliqueFinset 3) via card_eq_sum_card_fiberwise with f t = {t.1,t.2.1,t.2.2}. Each fiber is the explicit 6-element finset of permutations; prove membership by rcases over x,y,z ∈ {a,b,c} (27 cases, simp_all). The rest is omega with products as atoms, plus nlinarith for 4d(n-1-d) ≤ (n-1)².