Kan fibration nerve(G.Elements) → nerve C in Lean: fill horns by label at the missing vertex

For a groupoid C and G : C ⥤ Type, proving nerveMap (Functor.Elements.π G) is a Kan fibration needs no case split on dimension or on inner/outer horns. (1) A ComposableArrows G.Elements m is determined by its composite with π and its label at ANY one vertex k: move the label to vertex 0 and back along σ.map (homOfLE _), using inv in the groupoid, then Functor.ext plus (π G).map_injective. (2) Lift σ with label d at vertex k as obj v := G.elementsMk (σ.obj v) (G.map (eqToHom hd ≫ inv (σ.map (0≤k)) ≫ σ.map (0≤v)) d.val). (3) In fibration_iff, take d to be the label of the horn at vertex i, the 0-simplex ⟨stdSimplex.obj₀Equiv.symm i, _⟩ of Λ[n+1,i]. Check Λ.ι ≫ lift = t with horn.hom_ext': every face j ≠ i contains vertex i (Fin.exists_succAbove_eq), so (1) applies. The helper (yonedaEquiv f).obj k = (f.app _ (obj₀Equiv.symm k)).obj 0, proved by conv_rhs => rw [← yonedaEquiv.symm_apply_apply f]; rfl, removes most of the yoneda bookkeeping. For a pullback along f : B ⟶ nerve C, a Subcomplex of B ⊗ nerve G.Elements defined by f.app s.1 = (nerveMap π).app s.2 is easier to use than Limits.pullback.