R : Type u_2
R₂ : Type ?u.91322
K : Type ?u.91325
M : Type u_1
M₂ : Type ?u.91331
V : Type ?u.91334
S : Type ?u.91337
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
s : Set (Submodule R M)
z : M
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
this : Nonempty ↑s
⊢ z ∈ sSup s ↔ ∃ y, y ∈ s ∧ z ∈ y
R : Type u_2
R₂ : Type ?u.91322
K : Type ?u.91325
M : Type u_1
M₂ : Type ?u.91331
V : Type ?u.91334
S : Type ?u.91337
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
s : Set (Submodule R M)
z : M
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
⊢ z ∈ sSup s ↔ ∃ y, y ∈ s ∧ z ∈ y
have : Nonempty s := hs.to_subtype
no goals
R : Type u_2
R₂ : Type ?u.91322
K : Type ?u.91325
M : Type u_1
M₂ : Type ?u.91331
V : Type ?u.91334
S : Type ?u.91337
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
s : Set (Submodule R M)
z : M
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
this : Nonempty ↑s
⊢ z ∈ sSup s ↔ ∃ y, y ∈ s ∧ z ∈ y
simp only [sSup_eq_iSup', mem_iSup_of_directed _ hdir.directed_val, SetCoe.exists, Subtype.coe_mk,
  exists_prop]