no goals
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hs✝ : FG S
s : Finset A
hs : Algebra.adjoin R ↑s = S
⊢ Algebra.adjoin R ↑(Finset.image (↑f) s) = Subalgebra.map f S
rw [Finset.coe_image, Algebra.adjoin_image, hs]