R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s s' : { x // x ∈ S }
⊢ ↑(s * s') ∈ S
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s s' : { x // x ∈ S }
⊢ ↑s * ↑s' ∈ S
norm_cast
no goals
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s s' : { x // x ∈ S }
⊢ ↑(s * s') ∈ S
apply SetLike.coe_mem