M : Type u_1
A : Type ?u.44116
B : Type ?u.44119
inst✝ : MulOneClass M
S T : Submonoid M
⊢ T ≤ S ⊔ T
M : Type u_1
A : Type ?u.44116
B : Type ?u.44119
inst✝ : MulOneClass M
S T : Submonoid M
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T
rw [←SetLike.le_def]
no goals
M : Type u_1
A : Type ?u.44116
B : Type ?u.44119
inst✝ : MulOneClass M
S T : Submonoid M
⊢ T ≤ S ⊔ T
exact le_sup_right