R : Type u_2
R₂ : Type ?u.90559
K : Type ?u.90562
M : Type u_3
M₂ : Type ?u.90568
V : Type ?u.90571
S✝ : Type ?u.90574
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
x✝ : M
p p' : Submodule R M
inst✝³ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₂ M₂
s t : Set M
ι : Sort u_1
inst✝ : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x x_1 => x ≤ x_1) S
x : M
⊢ (∃ i, x ∈ ↑(S i)) ↔ ∃ i, x ∈ S i
R : Type u_2
R₂ : Type ?u.90559
K : Type ?u.90562
M : Type u_3
M₂ : Type ?u.90568
V : Type ?u.90571
S✝ : Type ?u.90574
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
x✝ : M
p p' : Submodule R M
inst✝³ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₂ M₂
s t : Set M
ι : Sort u_1
inst✝ : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ iSup S ↔ ∃ i, x ∈ S i
rw [← SetLike.mem_coe, coe_iSup_of_directed S H, mem_iUnion]
no goals
R : Type u_2
R₂ : Type ?u.90559
K : Type ?u.90562
M : Type u_3
M₂ : Type ?u.90568
V : Type ?u.90571
S✝ : Type ?u.90574
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
x✝ : M
p p' : Submodule R M
inst✝³ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₂ M₂
s t : Set M
ι : Sort u_1
inst✝ : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x x_1 => x ≤ x_1) S
x : M
⊢ (∃ i, x ∈ ↑(S i)) ↔ ∃ i, x ∈ S i
rfl