# Documentation

Mathlib.CategoryTheory.ConcreteCategory.Elementwise

In this file we provide various simp lemmas in its elementwise form via Tactic.Elementwise.

@[simp]
theorem CategoryTheory.Limits.limit.lift_π_apply {J : Type u₁} [] {C : Type u} {F : } (c : ) (j : J) [inst : ] (x : ().obj c.pt) :
↑() (↑() x) = ↑(c.app j) x
@[simp]
theorem CategoryTheory.Limits.cokernel.condition_apply {C : Type u} {X : C} {Y : C} (f : X Y) [inst : ] (x : ().obj X) :
↑() (f x) = 0 x
@[simp]
theorem CategoryTheory.Limits.limit.w_apply {J : Type u₁} [] {C : Type u} (F : ) {j : J} {j' : J} (f : j j') [inst : ] (x : ().obj ((().obj ).obj j)) :
↑(F.map f) (↑() x) = ↑() x
@[simp]
theorem CategoryTheory.Limits.colimit.ι_desc_apply {J : Type u₁} [] {C : Type u} {F : } (c : ) (j : J) [inst : ] (x : ().obj (F.obj j)) :
↑() (↑() x) = ↑(c.app j) x
@[simp]
theorem CategoryTheory.Limits.Cone.w_apply {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) {j : J} {j' : J} (f : j j') [inst : ] (x : ().obj ((().obj c.pt).obj j)) :
↑(F.map f) (↑(c.app j) x) = ↑(c.app j') x
@[simp]
theorem CategoryTheory.Limits.colimit.w_apply {J : Type u₁} [] {C : Type u} (F : ) {j : J} {j' : J} (f : j j') [inst : ] (x : ().obj (F.obj j)) :
↑() (↑(F.map f) x) = ↑() x
@[simp]
theorem CategoryTheory.Limits.cokernel.π_desc_apply {C : Type u} {X : C} {Y : C} (f : X Y) {W : C} (k : Y W) (h : ) [inst : ] (x : ) :
↑() () = k x
@[simp]
theorem CategoryTheory.Limits.kernel.condition_apply {C : Type u} {X : C} {Y : C} (f : X Y) [inst : ] (x : ().obj ()) :
f () = 0 x
@[simp]
theorem CategoryTheory.Limits.kernel.lift_ι_apply {C : Type u} {X : C} {Y : C} (f : X Y) {W : C} (k : W X) (h : ) [inst : ] (x : ().obj ().pt) :
↑() () = k x
theorem CategoryTheory.Limits.Cocone.w_apply {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) {j : J} {j' : J} (f : j j') [inst : ] (x : ().obj (F.obj j)) :
↑(c.app j') (↑(F.map f) x) = ↑(c.app j) x