R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f : R[X]
x : AdjoinRoot f
⊢ x ∈ Algebra.adjoin R {root f}
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f : R[X]
⊢ Algebra.adjoin R {root f} = ⊤
refine Algebra.eq_top_iff.2 fun x => ?_
no goals
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f : R[X]
x : AdjoinRoot f
⊢ x ∈ Algebra.adjoin R {root f}
induction x using AdjoinRoot.induction_on with
  | ih p =>  exact (Algebra.adjoin_singleton_eq_range_aeval R (root f)).symm ▸ ⟨p, aeval_eq p⟩
no goals
case ih
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f p : R[X]
⊢ ↑(mk f) p ∈ Algebra.adjoin R {root f}
exact (Algebra.adjoin_singleton_eq_range_aeval R (root f)).symm ▸ ⟨p, aeval_eq p⟩