no goals
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f = 0
inst✝ : Algebra R S
hfx : ↑(aeval a) f = 0
r : R
⊢ ↑(of (↑C r * X - 1)) r * root (↑C r * X - 1) = 1
convert sub_eq_zero.1 ((eval₂_sub _).symm.trans <| eval₂_root <| C r * X - 1) <;>
  simp only [eval₂_mul, eval₂_C, eval₂_X, eval₂_one]