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.

@[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

@[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

@[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

@[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