no goals
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_1
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type ?u.30644
inst✝ : CommRing P
⊢ coeSubmodule S ⊤ = 1
rw [coeSubmodule, Submodule.map_top, Submodule.one_eq_range]