English
For F,G : C ⥤ D ⥤ E ⥤ E' and α : F ⟶ G, with X₁,Y₁ ∈ C, f : X₁ ⟶ Y₁, and X₂ ∈ D, X₃ ∈ E, the equality ((F.map f).app X₂).app X₃ ≫ ((α.app Y₁).app X₂).app X₃ = ((α.app X₁).app X₂).app X₃ ≫ ((G.map f).app X₂).app X₃ holds.
Русский
Для F,G : C ⥤ D ⥤ E ⥤ E' и α : F ⟶ G, с X₁,Y₁ ∈ C, f : X₁ ⟶ Y₁, X₂ ∈ D, X₃ ∈ E выполняется: ((F.map f).app X₂).app X₃ ≫ ((α.app Y₁).app X₂).app X₃ = ((α.app X₁).app X₂).app X₃ ≫ ((G.map f).app X₂).app X₃.
LaTeX
$$$ ((F.map f).app X_2).app X_3 \; \gg \; ((\alpha.app Y_1).app X_2).app X_3 = ((\alpha.app X_1).app X_2).app X_3 \; \gg \; ((G.map f).app X_2).app X_3. $$$
Lean4
@[reassoc]
theorem naturality_app_app {F G : C ⥤ D ⥤ E ⥤ E'} (α : F ⟶ G) {X₁ Y₁ : C} (f : X₁ ⟶ Y₁) (X₂ : D) (X₃ : E) :
((F.map f).app X₂).app X₃ ≫ ((α.app Y₁).app X₂).app X₃ = ((α.app X₁).app X₂).app X₃ ≫ ((G.map f).app X₂).app X₃ :=
congr_app (NatTrans.naturality_app α X₂ f) X₃
