[GOAL]
R : Type u_1
inst✝ : CommRing R
r : R
⊢ ↑(aeval (IsLocalization.Away.invSelf r)) (↑C r * X - 1) = 0
[PROOFSTEP]
simp only [map_sub, map_mul, aeval_C, aeval_X, IsLocalization.Away.mul_invSelf, aeval_one, sub_self]
