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

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
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
cases subsingleton_or_nontrivial G
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
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
refine dense_of_exists_between fun a b hlt => ?_
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
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
rcases hS (b - a) (sub_pos.2 hlt) with ⟨g, hgS, hg0, hg⟩
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
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
rcases (existsUnique_add_zsmul_mem_Ioc hg0 0 a).exists with ⟨m, hm⟩
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
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
rw [zero_add] at hm
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
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
refine ⟨m • g, zsmul_mem hgS _, hm.1, hm.2.trans_lt ?_⟩
no goals
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
rwa [lt_sub_iff_add_lt'] at hg
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
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
refine fun x => _root_.subset_closure ?_
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
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
rw [Subsingleton.elim x 0]
no goals
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
exact zero_mem S