R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category J
F : J ⥤ ModuleCat R
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ ↑(coconeMorphism F j') (↑(F.map f) x) = ↑(F.map f ≫ coconeMorphism F j') x
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category J
F : J ⥤ ModuleCat R
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ ↑(coconeMorphism F j') (↑(F.map f) x) = ↑(coconeMorphism F j) x
rw [← cocone_naturality F f]
no goals
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category J
F : J ⥤ ModuleCat R
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ ↑(coconeMorphism F j') (↑(F.map f) x) = ↑(F.map f ≫ coconeMorphism F j') x
rfl