-- Mathlib/GroupTheory/ArchimedeanDensely.lean
lemma LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero
    {G₀ : Type*} [LinearOrderedCommGroupWithZero G₀] [Nontrivial G₀ˣ] {g : G₀} (hg : g ≠ 0) :
    Set.WellFoundedOn {x : G₀ | x ≤ g} (· > ·) ↔ Nonempty (G₀ ≃*o ℤₘ₀)

Proof state:
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
⊢ ({x | x ≤ g}.WellFoundedOn fun x1 x2 => x1 > x2) ↔ Nonempty (G₀ ≃*o ℤₘ₀)

Tactic:
rw [← wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero hg',
  ← Set.wellFoundedOn_sdiff_singleton (a := 0)]

Result:
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
⊢ (({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 => x1 > x2) ↔ {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2

Proof state:
case refine_1.inr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 => x1 > x2
x : G₀
hx : x ≠ 0
⊢ x ∈ {x | g⁻¹ ≤ x} → (fun x => x⁻¹) x ∈ {x | x ≤ g} \ {0}

Tactic:
simp only [mem_setOf_eq, mem_diff, mem_singleton_iff, inv_eq_zero, hx, not_false_eq_true,
  and_true]

Result:
case refine_1.inr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 => x1 > x2
x : G₀
hx : x ≠ 0
⊢ g⁻¹ ≤ x → x⁻¹ ≤ g

Proof state:
case refine_1
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 => x1 > x2
⊢ MapsTo (fun x => x⁻¹) {x | g⁻¹ ≤ x} ({x | x ≤ g} \ {0})

Tactic:
intro x

Result:
case refine_1
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 => x1 > x2
x : G₀
⊢ x ∈ {x | g⁻¹ ≤ x} → (fun x => x⁻¹) x ∈ {x | x ≤ g} \ {0}

Proof state:
case refine_4
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
⊢ ∀ a ∈ {x | x ≤ g} \ {0}, ∀ b ∈ {x | x ≤ g} \ {0}, a > b → Function.onFun (fun x1 x2 => x1 < x2) (fun x => x⁻¹) a b

Tactic:
simp only [mem_diff, mem_setOf_eq, mem_singleton_iff, gt_iff_lt, Function.onFun, and_imp]

Result:
case refine_4
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
⊢ ∀ a ≤ g, ¬a = 0 → ∀ b ≤ g, ¬b = 0 → b < a → a⁻¹ < b⁻¹

Proof state:
case refine_1.inl
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 => x1 > x2
⊢ 0 ∈ {x | g⁻¹ ≤ x} → (fun x => x⁻¹) 0 ∈ {x | x ≤ g} \ {0}

Tactic:
simp [hg]

Result:
no goals

Proof state:
case refine_1.inr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 => x1 > x2
x : G₀
hx : x ≠ 0
⊢ g⁻¹ ≤ x → x⁻¹ ≤ g

Tactic:
refine (inv_le_comm₀ ?_ ?_).mp <;>
simp [zero_lt_iff, hg, hx]

Result:
no goals

Proof state:
case refine_2
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).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⁻¹) a b

Tactic:
simp only [mem_setOf_eq, Function.onFun, gt_iff_lt]

Result:
case refine_2
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 => x1 > x2
⊢ ∀ (a : G₀), g⁻¹ ≤ a → ∀ (b : G₀), g⁻¹ ≤ b → a < b → b⁻¹ < a⁻¹