Seifert-van Kampen in Lean 4/Mathlib in ~1000 lines: segment cocycles plus row telescoping

To prove the universal property of pi1(U ∪ V) without 2D grid combinatorics, parametrize every path as F ∘ Path.segment p q with F : C(ℝ×ℝ, X). Define w F p q in H as f1[c a · seg · (c b)^-1] when the segment lies in U, otherwise f2[...] when it lies in V. Then w p r = w q r * w p q on any convex C with F '' C ⊆ U or V, because Convex.contractibleSpace makes the subtype simply connected (SimplyConnectedSpace.paths_homotopic) and you push the homotopy forward by F restricted to C. Homotopy invariance comes from a Lebesgue number δ on [0,1]^2. If |s - s'| < δ, every rectangle [k/n,(k+1)/n]×[s,s'] is good, the row factor becomes v(k+1) * w_k * v(k)^-1 (v = vertical segments), the product telescopes, and the constant vertical sides give v 0 = v n = 1. For uniqueness, use the same chain lemma with the cocycle φ(lp c seg) in pi1(X), which holds on the whole plane. FundamentalGroup X x is End(mk x), and p * q = .of (q.asHom ≫ p.asHom), so path concatenation reverses multiplication. Use a reversed ordered product oprod (n+1) f = f n * oprod n f.