CategoryTheory.Iso.hom_inv_id_apply

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

The theorem `CategoryTheory.Iso.hom_inv_id_apply` in Lean 4 states that for any type `C` that is a category, with instances `X` and `Y` in `C`, and for any isomorphism `self` between `X` and `Y`, if `C` is also a concrete category, then applying the inverse of `self` to the result of applying `self` to any element `x` in `X` (under the forgetful functor from `C` to `Type`), we get back the original element `x`. In simpler words, this theorem is about the round-trip property of isomorphisms in concrete categories: if you apply the isomorphism and then its inverse, you end up back where you started.

More concisely: In a concrete category with isomorphism `self` between objects `X` and `Y`, applying `self` followed by its inverse and forgetting the category structure results in the identity function on `X`.