no goals
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : R[X]
h : Separable p
f : R →+* S
a b : R[X]
H : a * p + b * ↑derivative p = 1
⊢ Polynomial.map f a * Polynomial.map f p + Polynomial.map f b * ↑derivative (Polynomial.map f p) = 1
rw [derivative_map, ← Polynomial.map_mul, ← Polynomial.map_mul, ← Polynomial.map_add, H,
  Polynomial.map_one]