-- 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 mp
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
⊢ Nonempty (G ≃+o ℤ)

Tactic:
by_cases H : ∀ (x : G) {y}, 0 < y → ∃ n : ℕ, x ≤ n • y

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 : ∀ (x : G) {y : G}, 0 < y → ∃ n, x ≤ n • y
⊢ Nonempty (G ≃+o ℤ)

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 : G) {y : G}, 0 < y → ∃ n, x ≤ n • y
⊢ Nonempty (G ≃+o ℤ)

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
⊢ ⟨x - (n + 1) • y, ⋯⟩ < (fun n => ⟨x - n • y, ⋯⟩) n

Tactic:
simp [add_smul, hy0]

Result:
no goals

Proof state:
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

Tactic:
wlog hy' : 0 < y generalizing y

Result:
case pos.intro.inr
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
⊢ False

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

Proof state:
case mp
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
h : WellFounded fun x1 x2 => x1 < x2
⊢ Nonempty (G ≃+o ℤ)

Tactic:
rw [WellFounded.wellFounded_iff_has_min] at h

Result:
case mp
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
⊢ Nonempty (G ≃+o ℤ)

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 ∈ {x | g ≤ x}, ∀ b ∈ {x | g ≤ x}, a < b → Function.onFun (fun x1 x2 => x1 < x2) (fun x => x - g) a b

Tactic:
intro

Result:
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

Proof state:
case pos.intro.inr.refine_1
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
⊢ -y ≠ 0

Tactic:
simp [hy]

Result:
no goals

Proof state:
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

Tactic:
exact hz'' ⟨w, hw.le⟩ hw hw'

Result:
no goals

Proof state:
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

Tactic:
exact BddBelow.wellFoundedOn_lt ⟨0, by 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 : ∀ (x : G) {y : G}, 0 < y → ∃ n, x ≤ n • y
⊢ Nonempty (G ≃+o ℤ)

Tactic:
replace H : Archimedean G := ⟨H⟩

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
⊢ Nonempty (G ≃+o ℤ)

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
⊢ Nonempty (G ≃+o ℤ)

Tactic:
exfalso

Result:
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

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 : G) {y : G}, 0 < y → ∃ n, x ≤ n • y
⊢ Nonempty (G ≃+o ℤ)

Tactic:
push_neg at H

Result:
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
⊢ Nonempty (G ≃+o ℤ)

Proof state:
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

Tactic:
obtain ⟨_, ⟨n, rfl⟩, hz⟩ :=
  h (Set.range (fun n : ℕ ↦ ⟨x - n • y, sub_nonneg.mpr (H _).le⟩)) (range_nonempty _)

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
⊢ False

Proof state:
case pos.intro.inr
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
⊢ False

Tactic:
refine this (-y) ?_ ?_

Result:
case pos.intro.inr.refine_1
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
⊢ -y ≠ 0

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

Proof state:
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 ℤ)

Tactic:
intro h

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