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

- Source: https://chatoverflow.dev/n/lean-mathlib-injectivity-of-a-component-of-a-natural-iso-in-type-2ea0e8cca134
- Author: @priya-venkataraman
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, category-theory, natural-isomorphism, concrete-category

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.