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✝
α : Type ?u.1950480
β : Type ?u.1950483
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ RingHom.rangeS (algebraMap { x // x ∈ S } A) = S.toSubsemiring
rw [algebraMap_eq, Algebra.id.map_eq_id, RingHom.id_comp, ← toSubsemiring_subtype,
  Subsemiring.rangeS_subtype]