-- Mathlib/GroupTheory/ArchimedeanDensely.lean
/-- Any linearly ordered archimedean additive group is either isomorphic (and order-isomorphic)
to the integers, or is densely ordered. -/
lemma LinearOrderedAddCommGroup.discrete_or_denselyOrdered (G : Type*)
    [LinearOrderedAddCommGroup G] [Archimedean G] :
    Nonempty (G ≃+o ℤ) ∨ DenselyOrdered G

Proof state:
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
x y : G
hxy : x < y
H : ¬IsLeast {y | 0 < y} (y - x)
⊢ ∃ z, 0 < z ∧ z < y - x

Tactic:
contrapose! H

Result:
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
x y : G
hxy : x < y
H : ∀ (z : G), 0 < z → y - x ≤ z
⊢ IsLeast {y | 0 < y} (y - x)

Proof state:
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
x y : G
hxy : x < y
H : ∀ (z : G), 0 < z → y - x ≤ z
⊢ y - x ∈ {y | 0 < y}

Tactic:
simp [hxy]

Result:
no goals

Proof state:
case neg.intro.refine_1
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
x y : G
hxy : x < y
H : ¬IsLeast {y | 0 < y} (y - x)
z : G
hz : 0 < z ∧ z < y - x
⊢ x < x + z

Tactic:
simp [hz.left]

Result:
no goals

Proof state:
case pos
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : ∃ x, IsLeast {y | 0 < y} x
⊢ Nonempty (G ≃+o ℤ) ∨ DenselyOrdered G

Tactic:
obtain ⟨x, hx⟩ := H

Result:
case pos.intro
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
x : G
hx : IsLeast {y | 0 < y} x
⊢ Nonempty (G ≃+o ℤ) ∨ DenselyOrdered G

Proof state:
case neg
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : ∀ (x : G), ¬IsLeast {y | 0 < y} x
x y : G
hxy : x < y
⊢ ∃ a, x < a ∧ a < y

Tactic:
specialize H (y - x)

Result:
case neg
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
x y : G
hxy : x < y
H : ¬IsLeast {y | 0 < y} (y - x)
⊢ ∃ a, x < a ∧ a < y

Proof state:
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
⊢ Nonempty (G ≃+o ℤ) ∨ DenselyOrdered G

Tactic:
by_cases H : ∃ x, IsLeast {y : G | 0 < y} x

Result:
case pos
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : ∃ x, IsLeast {y | 0 < y} x
⊢ Nonempty (G ≃+o ℤ) ∨ DenselyOrdered G

case neg
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : ¬∃ x, IsLeast {y | 0 < y} x
⊢ Nonempty (G ≃+o ℤ) ∨ DenselyOrdered G

Proof state:
case neg
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : ¬∃ x, IsLeast {y | 0 < y} x
⊢ Nonempty (G ≃+o ℤ) ∨ DenselyOrdered G

Tactic:
push_neg at H

Result:
case neg
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : ∀ (x : G), ¬IsLeast {y | 0 < y} x
⊢ Nonempty (G ≃+o ℤ) ∨ DenselyOrdered G

Proof state:
case pos.intro
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
x : G
hx : IsLeast {y | 0 < y} x
⊢ Nonempty (G ≃+o ℤ) ∨ DenselyOrdered G

Tactic:
exact Or.inl ⟨(int_orderAddMonoidIso_of_isLeast_pos hx)⟩

Result:
no goals

Proof state:
case neg.intro.refine_2
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
x y : G
hxy : x < y
H : ¬IsLeast {y | 0 < y} (y - x)
z : G
hz : 0 < z ∧ z < y - x
⊢ x + z < y

Tactic:
simpa [lt_sub_iff_add_lt'] using hz.right

Result:
no goals

Proof state:
case neg
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : ∀ (x : G), ¬IsLeast {y | 0 < y} x
⊢ Nonempty (G ≃+o ℤ) ∨ DenselyOrdered G

Tactic:
refine Or.inr ⟨?_⟩

Result:
case neg
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : ∀ (x : G), ¬IsLeast {y | 0 < y} x
⊢ ∀ (a₁ a₂ : G), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Proof state:
case neg
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
x y : G
hxy : x < y
H : ¬IsLeast {y | 0 < y} (y - x)
⊢ ∃ a, x < a ∧ a < y

Tactic:
obtain ⟨z, hz⟩ : ∃ z : G, 0 < z ∧ z < y - x := by
  contrapose! H
  refine ⟨by simp [hxy], fun _ ↦ H _⟩

Result:
case neg.intro
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
x y : G
hxy : x < y
H : ¬IsLeast {y | 0 < y} (y - x)
z : G
hz : 0 < z ∧ z < y - x
⊢ ∃ a, x < a ∧ a < y

Proof state:
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
x y : G
hxy : x < y
H : ∀ (z : G), 0 < z → y - x ≤ z
⊢ IsLeast {y | 0 < y} (y - x)

Tactic:
refine ⟨by simp [hxy], fun _ ↦ H _⟩

Result:
no goals

Proof state:
case neg.intro
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
x y : G
hxy : x < y
H : ¬IsLeast {y | 0 < y} (y - x)
z : G
hz : 0 < z ∧ z < y - x
⊢ ∃ a, x < a ∧ a < y

Tactic:
refine ⟨x + z, ?_, ?_⟩

Result:
case neg.intro.refine_1
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
x y : G
hxy : x < y
H : ¬IsLeast {y | 0 < y} (y - x)
z : G
hz : 0 < z ∧ z < y - x
⊢ x < x + z

case neg.intro.refine_2
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
x y : G
hxy : x < y
H : ¬IsLeast {y | 0 < y} (y - x)
z : G
hz : 0 < z ∧ z < y - x
⊢ x + z < y

Proof state:
case neg
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : ∀ (x : G), ¬IsLeast {y | 0 < y} x
⊢ ∀ (a₁ a₂ : G), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
intro x y hxy

Result:
case neg
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : ∀ (x : G), ¬IsLeast {y | 0 < y} x
x y : G
hxy : x < y
⊢ ∃ a, x < a ∧ a < y