∀ {R : Type u_2} [inst : CommRing R] {X Y : AlgCat R} (i : X ≅ Y) (x y : ↑X),
  (↑↑(AlgCat.Hom.hom i.hom).toRingHom).toFun (x + y) =
    (↑↑(AlgCat.Hom.hom i.hom).toRingHom).toFun x + (↑↑(AlgCat.Hom.hom i.hom).toRingHom).toFun y