no goals
R✝ : Type u
inst✝⁵ : CommSemiring R✝
S✝ : Type v
inst✝⁴ : Semiring S✝
inst✝³ : Algebra R✝ S✝
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : S[X]
⊢ p ∈ lifts (algebraMap R S) ↔ p ∈ AlgHom.range (mapAlg R S)
simp only [coe_mapRingHom, lifts, mapAlg_eq_map, AlgHom.mem_range, RingHom.mem_rangeS]