-- 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:
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 b : G₀
x✝ : g⁻¹ ≤ b
ha : a = 0
⊢ a < g⁻¹

Tactic:
simp [zero_lt_iff, ha, hg]

Result:
no goals

Proof state:
case refine_3
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
x : G₀
⊢ x ∈ {x | x ≤ g} \ {0} → (fun x => x⁻¹) x ∈ {x | g⁻¹ ≤ x}

Tactic:
simp only [mem_diff, mem_setOf_eq, mem_singleton_iff, and_imp]

Result:
case refine_3
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
x : G₀
⊢ x ≤ g → ¬x = 0 → g⁻¹ ≤ x⁻¹

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

Tactic:
have hg' : g⁻¹ ≠ 0 := by simp [hg]

Result:
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 ℤₘ₀)

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
x : G₀
⊢ x ∈ {x | g⁻¹ ≤ x} → (fun x => x⁻¹) x ∈ {x | x ≤ g} \ {0}

Tactic:
rcases eq_or_ne x 0 with rfl|hx

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

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}

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 : G₀
ha : g⁻¹ ≤ a
b : G₀
x✝ : g⁻¹ ≤ b
⊢ 0 < a

Tactic:
contrapose! ha

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 b : G₀
x✝ : g⁻¹ ≤ b
ha : a ≤ 0
⊢ a < g⁻¹

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 : G₀
a✝² : a ≤ g
a✝¹ : ¬a = 0
b : G₀
a✝ : b ≤ g
hb0 : ¬b = 0
⊢ 0 < b

Tactic:
simp [zero_lt_iff, hb0]

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 : G₀
ha : g⁻¹ ≤ a
b : G₀
x✝ : g⁻¹ ≤ b
⊢ a < b → b⁻¹ < a⁻¹

Tactic:
refine inv_strictAnti₀ ?_

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₀
ha : g⁻¹ ≤ a
b : G₀
x✝ : g⁻¹ ≤ b
⊢ 0 < a

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 ≤ g, ¬a = 0 → ∀ b ≤ g, ¬b = 0 → b < a → a⁻¹ < b⁻¹

Tactic:
intro a _ _ b _ hb0

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✝² : a ≤ g
a✝¹ : ¬a = 0
b : G₀
a✝ : b ≤ g
hb0 : ¬b = 0
⊢ b < a → a⁻¹ < b⁻¹

Proof state:
case refine_3
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
x : G₀
hxg : x ≤ g
hx : ¬x = 0
⊢ 0 < x

Tactic:
simp [zero_lt_iff, hx]

Result:
no goals

Proof state:
case refine_3
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
⊢ MapsTo (fun x => x⁻¹) ({x | x ≤ g} \ {0}) {x | g⁻¹ ≤ x}

Tactic:
intro x

Result:
case refine_3
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
x : G₀
⊢ x ∈ {x | x ≤ g} \ {0} → (fun x => x⁻¹) x ∈ {x | g⁻¹ ≤ x}

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 b : G₀
x✝ : g⁻¹ ≤ b
ha : a ≤ 0
⊢ a < g⁻¹

Tactic:
simp only [le_zero_iff] at ha

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 b : G₀
x✝ : g⁻¹ ≤ b
ha : a = 0
⊢ a < g⁻¹

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 : G₀
a✝² : a ≤ g
a✝¹ : ¬a = 0
b : G₀
a✝ : b ≤ g
hb0 : ¬b = 0
⊢ b < a → a⁻¹ < b⁻¹

Tactic:
refine inv_strictAnti₀ ?_

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✝² : a ≤ g
a✝¹ : ¬a = 0
b : G₀
a✝ : b ≤ g
hb0 : ¬b = 0
⊢ 0 < b

Proof state:
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
⊢ g⁻¹ ≠ 0

Tactic:
simp [hg]

Result:
no goals

Proof state:
case refine_3
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
x : G₀
hxg : x ≤ g
hx : ¬x = 0
⊢ g⁻¹ ≤ x⁻¹

Tactic:
refine inv_anti₀ ?_ hxg

Result:
case refine_3
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
x : G₀
hxg : x ≤ g
hx : ¬x = 0
⊢ 0 < x

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 : G₀), g⁻¹ ≤ a → ∀ (b : G₀), g⁻¹ ≤ b → a < b → b⁻¹ < a⁻¹

Tactic:
intro a ha b _

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₀
ha : g⁻¹ ≤ a
b : G₀
x✝ : g⁻¹ ≤ b
⊢ a < b → b⁻¹ < a⁻¹

Proof state:
case refine_3
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
x : G₀
⊢ x ≤ g → ¬x = 0 → g⁻¹ ≤ x⁻¹

Tactic:
intro hxg hx

Result:
case refine_3
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
x : G₀
hxg : x ≤ g
hx : ¬x = 0
⊢ g⁻¹ ≤ x⁻¹