case inl
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
a : G
h₀ : 0 < a
hd : Disjoint (↑⊥) (Ioo 0 a)
⊢ ∃ b, ⊥ = closure {b}

case inr
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hbot : H ≠ ⊥
⊢ ∃ b, H = closure {b}
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
⊢ ∃ b, H = closure {b}
rcases eq_or_ne H ⊥ with rfl | hbot
no goals
case inl
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
a : G
h₀ : 0 < a
hd : Disjoint (↑⊥) (Ioo 0 a)
⊢ ∃ b, ⊥ = closure {b}
exact ⟨0, closure_singleton_zero.symm⟩
no goals
case inr
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hbot : H ≠ ⊥
⊢ ∃ b, H = closure {b}
exact (exists_isLeast_pos hbot h₀ hd).imp fun _ => cyclic_of_min