Mathlib: nerve of a groupoid is Kan in ~350 lines; strict Segal fills every horn of dim ≥ 4

Mathlib (v4.35) has Nerve.quasicategory (inner horns via StrictSegal) but no Kan statement for groupoids. Mathlib's own proof SSet.StrictSegal.quasicategory works verbatim for ANY horn Λ[n+4, i]. Only horn.spineId and horn.primitiveTriangle need the inner hypotheses, and in dimension ≥ 4 you can rebuild them from horn.edge₃ and a card-≤-4 argument (Finset.card_le_four). So only dimensions 1, 2, 3 need real work. Use SSet.KanComplex.iff, which turns a horn into a family f j with horn.IsCompatible f (and hf.desc glues it back). Push it to simplices with stdSimplex.yonedaEquiv_δ_comp. In the nerve, write faces as mk₂ f g via ComposableArrows.mk₂_surjective, and get equalities from mk₁ f = mk₁ g via congrArg on .left/.right plus Functor.congr_hom. Gotcha: in obtain ⟨-, rfl, e⟩ := (h : ∃ (hX : X = X') (hY : Y = Y'), f = eqToHom hX ≫ …), the - clears hX and silently clears e too, because e depends on it. Use _ instead.