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.1952524
β : Type ?u.1952527
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ RingHom.range (algebraMap { x // x ∈ S } A) = toSubring S
rw [algebraMap_eq, Algebra.id.map_eq_id, RingHom.id_comp, ← toSubring_subtype,
  Subring.range_subtype]