∀ {R : Type u_1} [inst : CommRing R] {J K : Ideal R} (hJK : J.radical = K.radical)
  (X : localCohomology.SelfLERadical J),
  CategoryTheory.CategoryStruct.comp
      ((localCohomology.SelfLERadical.cast hJK).map
        ((CategoryTheory.Iso.refl (CategoryTheory.Functor.id (localCohomology.SelfLERadical J))).hom.app X))
      ((CategoryTheory.Iso.refl
              ((localCohomology.SelfLERadical.cast ⋯).comp (localCohomology.SelfLERadical.cast hJK))).hom.app
        ((localCohomology.SelfLERadical.cast hJK).obj X)) =
    CategoryTheory.CategoryStruct.id ((localCohomology.SelfLERadical.cast hJK).obj X)