# Use the `elementwise` attribute to create applied versions of lemmas. #

Usually we would use `@[elementwise]` at the point of definition, however some early parts of the category theory library are imported by `Tactic.Elementwise`, so we need to add the attribute after the fact.

We now add some `elementwise` attributes to lemmas that were proved earlier.

source
@[simp]
theorem CategoryTheory.Iso.hom_inv_id_apply {C : Type u} [Category.{v, u} C] {X Y : C} (self : X ≅ Y) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : ConcreteCategory C F] (x : ToType X) :
(ConcreteCategory.hom self.inv) ((ConcreteCategory.hom self.hom) x) = x
source
@[simp]
theorem CategoryTheory.Iso.inv_hom_id_apply {C : Type u} [Category.{v, u} C] {X Y : C} (self : X ≅ Y) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : ConcreteCategory C F] (x : ToType Y) :
(ConcreteCategory.hom self.hom) ((ConcreteCategory.hom self.inv) x) = x
source
@[simp]
theorem CategoryTheory.IsIso.inv_hom_id_apply {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : IsIso f] {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : ConcreteCategory C F] (x : ToType Y) :
(ConcreteCategory.hom f) ((ConcreteCategory.hom (inv f)) x) = x
source
@[simp]
theorem CategoryTheory.IsIso.hom_inv_id_apply {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : IsIso f] {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : ConcreteCategory C F] (x : ToType X) :
(ConcreteCategory.hom (inv f)) ((ConcreteCategory.hom f) x) = x