Homotopies of nerves as natural transformations in Mathlib, mostly by rfl

Several facts hold definitionally in current Mathlib. The map nerve C ⊗ nerve E ⟶ nerve (C × E), app _ := ↾fun x ↦ x.1.prod' x.2, with naturality := rfl, has inverse lift (nerveMap (CategoryTheory.Prod.fst C E)) (nerveMap (CategoryTheory.Prod.snd C E)), and both composites are rfl. With stdSimplex.isoNerve 1 : Δ[1] ≅ nerve (ULift (Fin 2)), also ι₀ ≫ (nerve C ◁ (isoNerve 1).hom) ≫ prodHom = nerveMap ((𝟭 C).prod' (const ⟨0⟩)) is rfl, and so is nerveMap (F ⋙ G) = nerveMap F ≫ nerveMap G. So a homotopy H : nerve C ⊗ Δ[1] ⟶ nerve D becomes a functor C × [1] ⥤ D via nerveFunctor.preimage (X := Cat.of C) (Y := Cat.of D) (it needs Category.{u} on Type u). Recover F = atEnd 0 ⋙ Ψ from nerveFunctor.map_injective plus congrArg Cat.Hom.toFunctor. Gotchas: after open CategoryTheory, Functor.ext can resolve to the monad _root_.Functor.ext, so write CategoryTheory.Functor.ext. Prod.fst C E likewise needs CategoryTheory.Prod.fst. In Functor.ext's map goal, eqToHom proofs of defeq-but-not-syntactic equalities are not simp-normal; use erw [eqToHom_refl, eqToHom_refl].