G : Type u_1
G' : Type ?u.229139
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.229148
inst✝ : AddGroup A
H K✝ : Subgroup G
k : Set G
K : Set (Subgroup G)
Kne : Set.Nonempty K
hK : DirectedOn (fun x x_1 => x ≤ x_1) K
x : G
this : Nonempty ↑K
⊢ x ∈ sSup K ↔ ∃ s, s ∈ K ∧ x ∈ s
G : Type u_1
G' : Type ?u.229139
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.229148
inst✝ : AddGroup A
H K✝ : Subgroup G
k : Set G
K : Set (Subgroup G)
Kne : Set.Nonempty K
hK : DirectedOn (fun x x_1 => x ≤ x_1) K
x : G
⊢ x ∈ sSup K ↔ ∃ s, s ∈ K ∧ x ∈ s
haveI : Nonempty K := Kne.to_subtype
no goals
G : Type u_1
G' : Type ?u.229139
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.229148
inst✝ : AddGroup A
H K✝ : Subgroup G
k : Set G
K : Set (Subgroup G)
Kne : Set.Nonempty K
hK : DirectedOn (fun x x_1 => x ≤ x_1) K
x : G
this : Nonempty ↑K
⊢ x ∈ sSup K ↔ ∃ s, s ∈ K ∧ x ∈ s
simp only [sSup_eq_iSup', mem_iSup_of_directed hK.directed_val, SetCoe.exists, Subtype.coe_mk,
  exists_prop]