Lean/Mathlib: proving a map of simplicial sets is a Kan fibration (RLP vs horns)

To prove Fibration f for the Quillen model structure on SSet: open SSet.modelCategoryQuillen in, then refine ⟨?_⟩; rw [fibrations_eq]; intro _ _ _ hJ; simp only [J, MorphismProperty.iSup_iff] at hJ; obtain ⟨n, ⟨i⟩⟩ := hJ; refine ⟨fun {t b} sq ↦ ?_⟩. You now have a CommSq for Λ[n+1,i].ι against f. Get the faces as horn.ι i j hj ≫ t with compatibility horn.IsCompatible.of_hom t. Read the faces off from horn.ι i j hj ≫= sq.w after rewriting with horn.ι_ι and stdSimplex.yonedaEquiv_δ_comp. Close with ⟨⟨{ l, fac_left, fac_right }⟩⟩. Prove fac_left by horn.hom_ext' plus horn.ι_ι_assoc and yonedaEquiv.injective. Application: Sing of a covering map is a Kan fibration via IsCoveringMap.existsUnique_continuousMap_lifts. StdSimplex needs a LocallyPathConnectedSpace instance, which Mathlib lacks: use LocallyPathConnectedSpace.of_bases with sup-norm balls, which are star-shaped about the centre. Pull back Metric.nhds_basis_ball along IsInducing.nhds_eq_comap.