-- Mathlib/GroupTheory/ArchimedeanDensely.lean
lemma LinearOrderedAddCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete
    {G : Type*} [LinearOrderedAddCommGroup G] [Nontrivial G] {g : G} :
    Set.WellFoundedOn {x : G | g ≤ x} (· < ·) ↔ Nonempty (G ≃+o ℤ)

Proof state:
case pos.intro.inr.refine_2
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
this : ∀ (y : G), y ≠ 0 → 0 < y → False
hy' : y ≤ 0
⊢ 0 < -y

Tactic:
simp [lt_of_le_of_ne hy' hy]

Result:
no goals

Proof state:
case mpr
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
⊢ Nonempty (G ≃+o ℤ) → {x | 0 ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2

Tactic:
rintro ⟨f⟩

Result:
case mpr.intro
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
f : G ≃+o ℤ
⊢ {x | 0 ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2

Proof state:
case pos
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
⊢ Nonempty (G ≃+o ℤ)

Tactic:
rw [LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered]

Result:
case pos
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
⊢ ¬DenselyOrdered G

Proof state:
case pos
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
⊢ ¬DenselyOrdered G

Tactic:
intro hd

Result:
case pos
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
⊢ False

Proof state:
case neg.intro.intro.intro.intro.intro.intro
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
x y : G
hy0 : 0 < y
H : ∀ (n : ℕ), n • y < x
n : ℕ
hz : ∀ x_1 ∈ range fun n => ⟨x - n • y, ⋯⟩, ¬x_1 < (fun n => ⟨x - n • y, ⋯⟩) n
⊢ False

Tactic:
refine hz ⟨x - (n + 1) • y, sub_nonneg.mpr (H _).le⟩ ⟨_, rfl⟩ ?_

Result:
case neg.intro.intro.intro.intro.intro.intro
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
x y : G
hy0 : 0 < y
H : ∀ (n : ℕ), n • y < x
n : ℕ
hz : ∀ x_1 ∈ range fun n => ⟨x - n • y, ⋯⟩, ¬x_1 < (fun n => ⟨x - n • y, ⋯⟩) n
⊢ ⟨x - (n + 1) • y, ⋯⟩ < (fun n => ⟨x - n • y, ⋯⟩) n

Proof state:
case refine_4
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
this : ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ Nonempty (G ≃+o ℤ)
h : {x | 0 ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
a✝ : G
⊢ a✝ ∈ {x | g ≤ x} → ∀ b ∈ {x | g ≤ x}, a✝ < b → Function.onFun (fun x1 x2 => x1 < x2) (fun x => x - g) a✝ b

Tactic:
simp [Function.onFun]

Result:
no goals

Proof state:
case neg
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : ∃ x y, 0 < y ∧ ∀ (n : ℕ), n • y < x
⊢ False

Tactic:
obtain ⟨x, y, hy0, H⟩ := H

Result:
case neg.intro.intro.intro
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
x y : G
hy0 : 0 < y
H : ∀ (n : ℕ), n • y < x
⊢ False

Proof state:
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
f : G ≃+o ℤ
this : LocallyFiniteOrder G
⊢ 0 ∈ lowerBounds {x | 0 ≤ x}

Tactic:
simp [mem_lowerBounds]

Result:
no goals

Proof state:
case pos
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
⊢ False

Tactic:
obtain ⟨y, hy⟩ := exists_ne (0 : G)

Result:
case pos.intro
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
⊢ False

Proof state:
case intro.mk.intro
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
hy' : 0 < y
z : G
hz : z ∈ {x | 0 ≤ x}
hz' : ⟨z, hz⟩ ∈ {x | ⟨0, ⋯⟩ < x}
hz'' : ∀ x ∈ {x | ⟨0, ⋯⟩ < x}, ¬x < ⟨z, hz⟩
⊢ False

Tactic:
obtain ⟨w, hw, hw'⟩ := exists_between hz'

Result:
case intro.mk.intro.intro.intro
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
hy' : 0 < y
z : G
hz : z ∈ {x | 0 ≤ x}
hz' : ⟨z, hz⟩ ∈ {x | ⟨0, ⋯⟩ < x}
hz'' : ∀ x ∈ {x | ⟨0, ⋯⟩ < x}, ¬x < ⟨z, hz⟩
w : G
hw : ↑⟨0, ⋯⟩ < w
hw' : w < ↑⟨z, hz⟩
⊢ False

Proof state:
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
hy' : 0 < y
⊢ False

Tactic:
obtain ⟨⟨z, hz⟩, hz', hz''⟩ := h ({x | ⟨0, le_rfl⟩ < x}) ⟨⟨y, hy'.le⟩, hy'⟩

Result:
case intro.mk.intro
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
hy' : 0 < y
z : G
hz : z ∈ {x | 0 ≤ x}
hz' : ⟨z, hz⟩ ∈ {x | ⟨0, ⋯⟩ < x}
hz'' : ∀ x ∈ {x | ⟨0, ⋯⟩ < x}, ¬x < ⟨z, hz⟩
⊢ False

Proof state:
case pos.intro.inr.refine_2
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
this : ∀ (y : G), y ≠ 0 → 0 < y → False
hy' : ¬0 < y
⊢ 0 < -y

Tactic:
simp only [not_lt] at hy'

Result:
case pos.intro.inr.refine_2
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
this : ∀ (y : G), y ≠ 0 → 0 < y → False
hy' : y ≤ 0
⊢ 0 < -y

Proof state:
case mpr.intro
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
f : G ≃+o ℤ
⊢ {x | 0 ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2

Tactic:
have : LocallyFiniteOrder G := LocallyFiniteOrder.ofOrderIsoClass f

Result:
case mpr.intro
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
f : G ≃+o ℤ
this : LocallyFiniteOrder G
⊢ {x | 0 ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2

Proof state:
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
this : ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ Nonempty (G ≃+o ℤ)
⊢ ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ Nonempty (G ≃+o ℤ)

Tactic:
rw [← this]

Result:
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
this : ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ Nonempty (G ≃+o ℤ)
⊢ ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ {x | 0 ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2

Proof state:
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
⊢ ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ Nonempty (G ≃+o ℤ)

Tactic:
constructor

Result:
case mp
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
⊢ ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) → Nonempty (G ≃+o ℤ)

case mpr
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
⊢ Nonempty (G ≃+o ℤ) → {x | 0 ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2