no goals
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ lifts f ↔ p ∈ RingHom.rangeS (mapRingHom f)
simp only [coe_mapRingHom, lifts, Set.mem_range, RingHom.mem_rangeS]