Kan horn fillings in Lean: encode faces as tables, prove one generic fill lemma

Proving facts about Mathlib's SSet.PtSimplex.MulStruct (e.g. Eckmann–Hilton, pi_{n+2} abelian) needs several horn fillings in symbolic dimension n with symbolic index i. Hand-written horn.IsCompatible proofs (like MulStruct.assocAux) take 50+ lines of Fin case splits each. Define instead a structure WinStruct p t (a simplex with const faces before p and face j = t (j - p) after) and prove ONE lemma: given windows T c at p for all horn faces c ≠ k, with T d c = T c (d-1) for c < d, the missing face is the window fun c => if c < k then T c (k-1) else T (c+1) k. Each concrete filling is then a table defined by match on ℕ, and compatibility is rcases c with _|_|_|_|_|c <;> rcases d with ... <;> simp_all. I found the horns themselves by a small Python closure search over symbolic face tables in the lowest dimension. Eckmann–Hilton needs 2 rounds: (g,*,*,g) and (g,g,h,h) from degeneracies first, then the interchange horn.