CategoryTheory.presheafHom_map_app

theorem CategoryTheory.presheafHom_map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] {F G : CategoryTheory.Functor Cᵒᵖ A} {X Y Z : C} (f : Z ⟶ Y) (g : Y ⟶ X) (h : Z ⟶ X), CategoryTheory.CategoryStruct.comp f g = h → ∀ (α : (CategoryTheory.presheafHom F G).obj (Opposite.op X)), ((CategoryTheory.presheafHom F G).map g.op α).app (Opposite.op (CategoryTheory.Over.mk f)) = α.app (Opposite.op (CategoryTheory.Over.mk h))

This theorem, `CategoryTheory.presheafHom_map_app`, states a key equational property for the presheaf structure on `presheafHom` in category theory. In essence, given two categories `C` and `A`, functors `F` and `G` from the opposite of `C` to `A`, and three objects `X`, `Y`, and `Z` in `C` with morphisms `f: Z ⟶ Y`, `g: Y ⟶ X`, and `h: Z ⟶ X` such that the composition of `f` and `g` equals `h`, then for all `α` in the object set of `presheafHom` of `F` and `G` with `Opposite.op X`, the application of the morphism map `g.op` to `α` and then applying to `Opposite.op (CategoryTheory.Over.mk f)` produces the same result as applying `α` to `Opposite.op (CategoryTheory.Over.mk h)`. This theorem is advising not to use `dsimp [presheafHom]` to simplify, as it may introduce the need to prove equalities of objects in an `Over` category.

More concisely: For any categories `C` and `A`, functors `F` and `G` from the opposite of `C` to `A`, and presheaf morphisms `α: F.Op X ⟶ G.Op Y` in `presheafHom F G (Opposite.op X)`, if `f: Z ⟶ Y` and `g: Y ⟶ X` are morphisms in `C` with `h: Z ⟶ X` such that `f.op * g = h.op`, then `α.app (Opposite.op (CategoryTheory.Over.mk f)) = α.app (Opposite.op (CategoryTheory.Over.mk h))`.