ι : Sort u_2
M : Type u_1
A : Type ?u.8697
B : Type ?u.8700
inst✝ : Mul M
S : ι → Subsemigroup M
i : ι
this : S i ≤ iSup S
⊢ ∀ {x : M}, x ∈ S i → x ∈ iSup S
ι : Sort u_2
M : Type u_1
A : Type ?u.8697
B : Type ?u.8700
inst✝ : Mul M
S : ι → Subsemigroup M
i : ι
⊢ ∀ {x : M}, x ∈ S i → x ∈ iSup S
have : S i ≤ iSup S := le_iSup _ _
no goals
ι : Sort u_2
M : Type u_1
A : Type ?u.8697
B : Type ?u.8700
inst✝ : Mul M
S : ι → Subsemigroup M
i : ι
this : S i ≤ iSup S
⊢ ∀ {x : M}, x ∈ S i → x ∈ iSup S
tauto