G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
h : ¬∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
⊢ ∃ a, S = closure {a}
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
⊢ Dense ↑S ∨ ∃ a, S = closure {a}
refine (em _).imp (dense_of_not_isolated_zero S) fun h => ?_
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
h : ∃ ε, ε > 0 ∧ ∀ (g : G), g ∈ S → ¬g ∈ Ioo 0 ε
⊢ ∃ a, S = closure {a}
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
h : ¬∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
⊢ ∃ a, S = closure {a}
push_neg at h
case intro.intro
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
ε : G
ε0 : ε > 0
hε : ∀ (g : G), g ∈ S → ¬g ∈ Ioo 0 ε
⊢ ∃ a, S = closure {a}
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
h : ∃ ε, ε > 0 ∧ ∀ (g : G), g ∈ S → ¬g ∈ Ioo 0 ε
⊢ ∃ a, S = closure {a}
rcases h with ⟨ε, ε0, hε⟩
no goals
case intro.intro
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
ε : G
ε0 : ε > 0
hε : ∀ (g : G), g ∈ S → ¬g ∈ Ioo 0 ε
⊢ ∃ a, S = closure {a}
exact cyclic_of_isolated_zero ε0 (disjoint_left.2 hε)