mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapNatIso_functor_obj_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T T' : CategoryTheory.Functor C D} (i : T ≅ T')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T),
  ((CategoryTheory.StructuredArrow.mapNatIso i).functor.obj X).hom =
    CategoryTheory.CategoryStruct.comp X.hom (i.hom.app X.right)