[GOAL]
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hS : ∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
⊢ Dense ↑S
[PROOFSTEP]
cases subsingleton_or_nontrivial G
[GOAL]
case inl
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hS : ∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
h✝ : Subsingleton G
⊢ Dense ↑S
[PROOFSTEP]
refine fun x => _root_.subset_closure ?_
[GOAL]
case inl
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hS : ∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
h✝ : Subsingleton G
x : G
⊢ x ∈ ↑S
[PROOFSTEP]
rw [Subsingleton.elim x 0]
[GOAL]
case inl
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hS : ∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
h✝ : Subsingleton G
x : G
⊢ 0 ∈ ↑S
[PROOFSTEP]
exact zero_mem S
[GOAL]
case inr
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hS : ∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
h✝ : Nontrivial G
⊢ Dense ↑S
[PROOFSTEP]
refine dense_of_exists_between fun a b hlt => ?_
[GOAL]
case inr
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hS : ∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
h✝ : Nontrivial G
a b : G
hlt : a < b
⊢ ∃ c, c ∈ ↑S ∧ a < c ∧ c < b
[PROOFSTEP]
rcases hS (b - a) (sub_pos.2 hlt) with ⟨g, hgS, hg0, hg⟩
[GOAL]
case inr.intro.intro.intro
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hS : ∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
h✝ : Nontrivial G
a b : G
hlt : a < b
g : G
hgS : g ∈ S
hg0 : 0 < g
hg : g < b - a
⊢ ∃ c, c ∈ ↑S ∧ a < c ∧ c < b
[PROOFSTEP]
rcases(existsUnique_add_zsmul_mem_Ioc hg0 0 a).exists with ⟨m, hm⟩
[GOAL]
case inr.intro.intro.intro.intro
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hS : ∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
h✝ : Nontrivial G
a b : G
hlt : a < b
g : G
hgS : g ∈ S
hg0 : 0 < g
hg : g < b - a
m : ℤ
hm : 0 + m • g ∈ Ioc a (a + g)
⊢ ∃ c, c ∈ ↑S ∧ a < c ∧ c < b
[PROOFSTEP]
rw [zero_add] at hm 
[GOAL]
case inr.intro.intro.intro.intro
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hS : ∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
h✝ : Nontrivial G
a b : G
hlt : a < b
g : G
hgS : g ∈ S
hg0 : 0 < g
hg : g < b - a
m : ℤ
hm : m • g ∈ Ioc a (a + g)
⊢ ∃ c, c ∈ ↑S ∧ a < c ∧ c < b
[PROOFSTEP]
refine ⟨m • g, zsmul_mem hgS _, hm.1, hm.2.trans_lt ?_⟩
[GOAL]
case inr.intro.intro.intro.intro
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hS : ∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
h✝ : Nontrivial G
a b : G
hlt : a < b
g : G
hgS : g ∈ S
hg0 : 0 < g
hg : g < b - a
m : ℤ
hm : m • g ∈ Ioc a (a + g)
⊢ a + g < b
[PROOFSTEP]
rwa [lt_sub_iff_add_lt'] at hg 
[GOAL]
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hbot : S ≠ ⊥
H : ¬∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a
⊢ Dense ↑S
[PROOFSTEP]
refine S.dense_of_not_isolated_zero fun ε ε0 => ?_
[GOAL]
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hbot : S ≠ ⊥
H : ¬∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a
ε : G
ε0 : ε > 0
⊢ ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
[PROOFSTEP]
contrapose! H
[GOAL]
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hbot : S ≠ ⊥
ε : G
ε0 : ε > 0
H : ∀ (g : G), g ∈ S → ¬g ∈ Ioo 0 ε
⊢ ∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a
[PROOFSTEP]
exact exists_isLeast_pos hbot ε0 (disjoint_left.2 H)
[GOAL]
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}
[PROOFSTEP]
refine (em _).imp (dense_of_not_isolated_zero S) fun h => ?_
[GOAL]
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}
[PROOFSTEP]
push_neg at h 
[GOAL]
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}
[PROOFSTEP]
rcases h with ⟨ε, ε0, hε⟩
[GOAL]
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}
[PROOFSTEP]
exact cyclic_of_isolated_zero ε0 (disjoint_left.2 hε)
