M : Type u_1
A : Type ?u.45947
B : Type ?u.45950
inst✝ : MulOneClass M
S : Set (Submonoid M)
s : Submonoid M
hs : s ∈ S
⊢ s ≤ sSup S
M : Type u_1
A : Type ?u.45947
B : Type ?u.45950
inst✝ : MulOneClass M
S : Set (Submonoid M)
s : Submonoid M
hs : s ∈ S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S
rw [←SetLike.le_def]
no goals
M : Type u_1
A : Type ?u.45947
B : Type ?u.45950
inst✝ : MulOneClass M
S : Set (Submonoid M)
s : Submonoid M
hs : s ∈ S
⊢ s ≤ sSup S
exact le_sSup hs