no goals
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.5139389
a a' a₁ a₂ : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝³ : CommSemiring R
inst✝² : CommSemiring S₁
p q : MvPolynomial σ R
inst✝¹ : Algebra R S₁
inst✝ : CommSemiring S₂
f : σ → S₁
s : Set S₁
⊢ Algebra.adjoin R s = AlgHom.range (aeval Subtype.val)
rw [← Algebra.adjoin_range_eq_range_aeval, Subtype.range_coe]