ι : Sort ?u.8999
M : Type u_1
A : Type ?u.9005
B : Type ?u.9008
inst✝ : Mul M
S : Set (Subsemigroup M)
s : Subsemigroup M
hs : s ∈ S
this : s ≤ sSup S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S
ι : Sort ?u.8999
M : Type u_1
A : Type ?u.9005
B : Type ?u.9008
inst✝ : Mul M
S : Set (Subsemigroup M)
s : Subsemigroup M
hs : s ∈ S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S
have : s ≤ sSup S := le_sSup hs
no goals
ι : Sort ?u.8999
M : Type u_1
A : Type ?u.9005
B : Type ?u.9008
inst✝ : Mul M
S : Set (Subsemigroup M)
s : Subsemigroup M
hs : s ∈ S
this : s ≤ sSup S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S
tauto