Subcubic Brooks theorem: ColouringGlue

Part of the proof that a finite subcubic K₄-free graph is three-colourable.

theorem BrooksSubcubic.colorable_glue_at_vertex {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (A B : Finset V) (x : V) (hcover : A ∪ B = Finset.univ) (hxA : x ∈ A) (hxB : x ∈ B) (hcross : ∀ u ∈ A, ∀ w ∈ B, u ≠ x → w ≠ x → ¬G.Adj u w) (hA : (SimpleGraph.induce (↑A) G).Colorable 3) (hB : (SimpleGraph.induce (↑B) G).Colorable 3) : G.Colorable 3

Glue lemma at a cut vertex. If A and B cover V, x belongs to both, no G-edge joins A∖{x} to B∖{x}, and both induced subgraphs G[A], G[B] are 3-colourable, then G is 3-colourable. Proof: pick colourings cA, cB; recolour B by the transposition swap (cB x) (cA x) so both agree at x; glue with A taking priority. Every edge lies inside A or inside B — a cross edge would violate the no-cross hypothesis — so the glued map inherits properness, and the alignment at x handles the boundary.