no goals
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.2110936
B' : Type ?u.2110939
a b : R
n : ℕ
inst✝³ : CommSemiring A'
inst✝² : Semiring B'
inst✝¹ : Ring R
inst✝ : Nontrivial R
r : R
x✝ : IsUnit (X - ↑C r)
g : R[X]
_hfg : (X - ↑C r) * g = 1
hgf : g * (X - ↑C r) = 1
⊢ 0 = 1
erw [← eval_mul_X_sub_C, hgf, eval_one]