R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type ?u.283475
inst✝ : NonUnitalRingHomClass F R S✝
S : Set (NonUnitalSubsemiring R)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : R
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type ?u.283475
inst✝ : NonUnitalRingHomClass F R S✝
S : Set (NonUnitalSubsemiring R)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
haveI : Nonempty S := Sne.to_subtype
no goals
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type ?u.283475
inst✝ : NonUnitalRingHomClass F R S✝
S : Set (NonUnitalSubsemiring R)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : R
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, Subtype.exists, exists_prop]