∀ {R : Type u_1} [inst : CommRing R] (r : R),
  { toRingHom := Localization.awayLift (AdjoinRoot.of (Polynomial.C r * Polynomial.X - 1)) r ⋯, commutes' := ⋯ }.comp
      (AdjoinRoot.liftAlgHom (Polynomial.C r * Polynomial.X - 1) (Algebra.ofId R (Localization.Away r))
        (IsLocalization.Away.invSelf r) ⋯) =
    AlgHom.id R (AdjoinRoot (Polynomial.C r * Polynomial.X - 1))