M : Type u_2
A : Type ?u.45573
B : Type ?u.45576
inst✝ : MulOneClass M
ι : Sort u_1
S : ι → Submonoid M
i : ι
⊢ S i ≤ iSup S
M : Type u_2
A : Type ?u.45573
B : Type ?u.45576
inst✝ : MulOneClass M
ι : Sort u_1
S : ι → Submonoid M
i : ι
⊢ ∀ {x : M}, x ∈ S i → x ∈ iSup S
rw [←SetLike.le_def]
no goals
M : Type u_2
A : Type ?u.45573
B : Type ?u.45576
inst✝ : MulOneClass M
ι : Sort u_1
S : ι → Submonoid M
i : ι
⊢ S i ≤ iSup S
exact le_iSup _ _