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} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (self : X ≅ Y) [inst : CategoryTheory.ConcreteCategory C] (x : (CategoryTheory.forget C).toPrefunctor.obj X) : self.2 (self.1 x) = x

@[simp]

theorem CategoryTheory.Iso.inv_hom_id_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (self : X ≅ Y) [inst : CategoryTheory.ConcreteCategory C] (x : (CategoryTheory.forget C).toPrefunctor.obj Y) : self.1 (self.2 x) = x

@[simp]

theorem CategoryTheory.IsIso.hom_inv_id_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f] [inst : CategoryTheory.ConcreteCategory C] (x : (CategoryTheory.forget C).toPrefunctor.obj X) : (Classical.choose (_ : ∃ (inv : Y ⟶ X), CategoryTheory.CategoryStruct.comp f inv = CategoryTheory.CategoryStruct.id X ∧ CategoryTheory.CategoryStruct.comp inv f = CategoryTheory.CategoryStruct.id Y)) (f x) = x

@[simp]

theorem CategoryTheory.IsIso.inv_hom_id_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f] [inst : CategoryTheory.ConcreteCategory C] (x : (CategoryTheory.forget C).toPrefunctor.obj Y) : f ((Classical.choose (_ : ∃ (inv : Y ⟶ X), CategoryTheory.CategoryStruct.comp f inv = CategoryTheory.CategoryStruct.id X ∧ CategoryTheory.CategoryStruct.comp inv f = CategoryTheory.CategoryStruct.id Y)) x) = x