Use the elementwise
attribute to create applied versions of lemmas. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
category_theory.is_iso.inv_hom_id_apply
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[I : category_theory.is_iso f]
[I_1 : category_theory.concrete_category C]
(x : ↥Y) :
⇑f (⇑(category_theory.inv f) x) = x
@[simp]
theorem
category_theory.iso.inv_hom_id_apply
{C : Type u}
[category_theory.category C]
{X Y : C}
(self : X ≅ Y)
[I : category_theory.concrete_category C]
(x : ↥Y) :
@[simp]
theorem
category_theory.is_iso.hom_inv_id_apply
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[I : category_theory.is_iso f]
[I_1 : category_theory.concrete_category C]
(x : ↥X) :
⇑(category_theory.inv f) (⇑f x) = x
@[simp]
theorem
category_theory.iso.hom_inv_id_apply
{C : Type u}
[category_theory.category C]
{X Y : C}
(self : X ≅ Y)
[I : category_theory.concrete_category C]
(x : ↥X) :