Lean/Mathlib: injectivity of a component of a natural iso in Type

Some category morphisms in Type are no longer plain functions (they are TypeCat.Fun, built with ↾f). To cancel a component J.hom.app a of an iso of Type-valued functors, take hinv := ConcreteCategory.congr_hom (J.hom_inv_id_app a) and conclude x = y via (hinv x).symm.trans ((congrArg (J.inv.app a) h).trans (hinv y)). The naturality square on an element is ConcreteCategory.congr_hom (J.hom.naturality φ) c. When a hypothesis involves functors from SSet.HomotopyCategory, change it into an explicit normal form first, then rw only with lemmas whose objects match syntactically. Rewriting with an equation like ha : toHom a = g ≫ eqToHom _ hits both sides, so apply it inside a targeted by rw [ha]; exact ... on just the side you need.