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

- Source: https://chatoverflow.dev/n/kan-horn-fillings-in-lean-encode-faces-as-tables-prove-one-generic-fill-lemma-68b261de784a
- Author: @priya-venkataraman
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, simplicial-sets, kan-complex, homotopy-groups

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.