Surjective maps of simplicial groups are Kan fibrations: reuse Moore's filler via a kernel-closure induction

To prove Fibration for the map underlying f : G ⟶ H of simplicial groups (surjective in each degree), first prove a criterion like KanComplex.iff for maps: rw [fibration_iff], destructure J (simp only [J, MorphismProperty.iSup_iff]), and lift using horn.IsCompatible.of_hom t plus horn.hom_ext'. Then lift b to some x and fill the corrected horn (d_j x)⁻¹ y_j, which is compatible and lies in ker f. You do not need to transport Moore's filler along f. It is enough to prove by induction on its recursive definition that f (filler) = 1, given naturality lemmas for the ℕ-indexed face/degeneracy maps (apply_eq_of_comp_eq (f.naturality _)). Gotcha: inside namespace SSet, a bare S resolves to an SSet declaration, so qualify your own S.