ι : Sort ?u.7679
M : Type u_1
A : Type ?u.7685
B : Type ?u.7688
inst✝ : Mul M
S T : Subsemigroup M
this : S ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T
ι : Sort ?u.7679
M : Type u_1
A : Type ?u.7685
B : Type ?u.7688
inst✝ : Mul M
S T : Subsemigroup M
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T
have : S ≤ S ⊔ T := le_sup_left
no goals
ι : Sort ?u.7679
M : Type u_1
A : Type ?u.7685
B : Type ?u.7688
inst✝ : Mul M
S T : Subsemigroup M
this : S ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T
tauto