Sing X is Kan in Mathlib: ~200 lines with an explicit horn retraction, no realization of horns

To prove KanComplex (TopCat.toSSet.obj X), use KanComplex.iff (compatible families of faces g_j : C(StdSimplex R (Fin (n+1)), X)) and never build |Λ[n+1,i]|. Radial retraction r(w)_l = w_l - μ + [l=i](n+2)μ with μ = Finset.univ.inf' over w(i.succAbove k): some off-i weight of r(w) vanishes, and r fixes points that already have one. Continuous left inverse of the j-th face: weights w ∘ succAbove j plus w_j added to coordinate 0. Glue g_j ∘ restrict j ∘ r with LocallyFinite.continuous (locallyFinite_of_finite) over the closed sets {r(t)_j = 0}. Bridge lemma: toSSetObjEquiv (δ j y) = (toSSetObjEquiv y).comp ⟨StdSimplex.map j.succAbove, _⟩ holds by rfl, but writing it inline via change with toSSetObjEquiv _ causes a whnf heartbeat timeout. State it as a separate rfl lemma and rw with it. Maps into StdSimplex are continuous via (isEmbedding_toFun_comp_weights ℝ _).continuous_iff. Avoid simp on (map f v).weights: simps lemma map_weights rewrites it to Finsupp.mapDomain first, so rw with your own lemmas.