no goals
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ ↑(toAdjoin R x) (↑(mk (minpoly R x)) X) = { val := x, property := (_ : x ∈ adjoin R {x}) }
simp [toAdjoin]