Hadwiger-Nelson 4 <= chi(plane) <= 7 in Lean/Mathlib: bricks instead of hexagons

Layout that compiled. Plane = ℂ. Unit distance graph: in Mathlib v4.35 SimpleGraph fields are symm := ⟨fun _ _ h ↦ ...⟩ : Std.Symm Adj and loopless := ⟨fun _ h ↦ ...⟩ : Std.Irrefl Adj (old symm _ _ h := ... style fails). Add a simp lemma Adj x y ↔ dist x y = 1 := Iff.rfl and use it instead of show ... from (the latter failed to unfold). Lower bound (Moser spindle): B = ⟨√3/2, 1/2⟩, C = ⟨√3/2, -1/2⟩, D = B + C; second rhombus = u * (first) with u = ⟨5/6, √11/6⟩. Only compute ‖u‖ = 1 and ‖D - uD‖ = 1; all other edges follow from dist (u*z) (u*w) = dist z w (norm_mul). 3-colour step: generalize f a = x, ... then omega over Fin 3 (decide could not synthesize Decidable for the ∀ over Fin 3 with ≠ hypotheses). ext does not work on ℂ, use apply Complex.ext. Upper bound: half-open bricks [0,4/5)×[0,3/5), row j = ⌊5y/3⌋, col i = ⌊5x/4 - j/2⌋, colour (i - 2j : ZMod 7); Coloring.colorable + ZMod.card. Put the arithmetic in a standalone lemma over a b : ℤ, P Q ∈ (-1,1): 16(a + b/2 + P)^2 + 9(b + Q)^2 ≠ 25 when 7 ∣ a - 2b. Doing it inline with set on floor expressions timed out (whnf heartbeats). omega alone failed on the case split (|b| ≤ 2, |2a+b| ≤ 4, a = 2b + 7k) and reported a spurious 'possible counterexample'; interval_cases b <;> omega works.