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

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

Tactic:
exact WithZero.withZeroUnitsEquiv.symm.trans f.withZero

Result:
no goals

Proof state:
case refine_2.inl
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
f : G₀ˣ ≃*o Multiplicative ℤ
b : G₀
⊢ (WithZero.withZeroUnitsEquiv.symm.trans f.withZero).toFun 0 ≤
      (WithZero.withZeroUnitsEquiv.symm.trans f.withZero).toFun b ↔
    0 ≤ b

Tactic:
simp [WithZero.withZeroUnitsEquiv, MulEquiv.withZero]

Result:
no goals

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

Tactic:
intro

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

Proof state:
case refine_4
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
f : G₀ ≃*o ℤₘ₀
a✝ b✝ : G₀ˣ
⊢ (WithZero.withZeroUnitsEquiv.trans ↑f).unzero.toFun a✝ ≤ (WithZero.withZeroUnitsEquiv.trans ↑f).unzero.toFun b✝ ↔
    a✝ ≤ b✝

Tactic:
rw [← WithZero.coe_le_coe]

Result:
case refine_4
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
f : G₀ ≃*o ℤₘ₀
a✝ b✝ : G₀ˣ
⊢ ↑((WithZero.withZeroUnitsEquiv.trans ↑f).unzero.toFun a✝) ≤
      ↑((WithZero.withZeroUnitsEquiv.trans ↑f).unzero.toFun b✝) ↔
    a✝ ≤ b✝

Proof state:
case refine_5
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h : {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
⊢ ∀ (a : G₀),
    g ≤ a →
      ¬a = 0 →
        ∀ (b : G₀),
          g ≤ b → ¬b = 0 → a < b → (if h : a = 0 then 1 else Units.mk0 a h) < if h : b = 0 then 1 else Units.mk0 b h

Tactic:
intro _ _ ha0 _ _ hb0 h

Result:
case refine_5
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h✝ : {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
a✝² : G₀
a✝¹ : g ≤ a✝²
ha0 : ¬a✝² = 0
b✝ : G₀
a✝ : g ≤ b✝
hb0 : ¬b✝ = 0
h : a✝² < b✝
⊢ (if h : a✝² = 0 then 1 else Units.mk0 a✝² h) < if h : b✝ = 0 then 1 else Units.mk0 b✝ h

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

Tactic:
refine ⟨fun h ↦ (h.mapsTo Units.val ?_).mono' ?_,
  fun h ↦ (h.mapsTo ?_ ?_).mono' ?_⟩

Result:
case refine_1
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h : ({x | g ≤ x} \ {0}).WellFoundedOn fun x1 x2 => x1 < x2
⊢ MapsTo Units.val {x | Units.mk0 g hg ≤ x} ({x | g ≤ x} \ {0})

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

case refine_3
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h : {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
⊢ G₀ → G₀ˣ

case refine_4
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h : {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
⊢ MapsTo ?refine_3 ({x | g ≤ x} \ {0}) {x | Units.mk0 g hg ≤ x}

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

Proof state:
case refine_2.inr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
f : G₀ˣ ≃*o Multiplicative ℤ
a b : G₀
ha : a ≠ 0
⊢ (WithZero.withZeroUnitsEquiv.symm.trans f.withZero).toFun a ≤
      (WithZero.withZeroUnitsEquiv.symm.trans f.withZero).toFun b ↔
    a ≤ b

Tactic:
rcases eq_or_ne b 0 with rfl|hb

Result:
case refine_2.inr.inl
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
f : G₀ˣ ≃*o Multiplicative ℤ
a : G₀
ha : a ≠ 0
⊢ (WithZero.withZeroUnitsEquiv.symm.trans f.withZero).toFun a ≤
      (WithZero.withZeroUnitsEquiv.symm.trans f.withZero).toFun 0 ↔
    a ≤ 0

case refine_2.inr.inr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
f : G₀ˣ ≃*o Multiplicative ℤ
a b : G₀
ha : a ≠ 0
hb : b ≠ 0
⊢ (WithZero.withZeroUnitsEquiv.symm.trans f.withZero).toFun a ≤
      (WithZero.withZeroUnitsEquiv.symm.trans f.withZero).toFun b ↔
    a ≤ b

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

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

Result:
case refine_5
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h : {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
⊢ ∀ (a : G₀),
    g ≤ a →
      ¬a = 0 →
        ∀ (b : G₀),
          g ≤ b → ¬b = 0 → a < b → (if h : a = 0 then 1 else Units.mk0 a h) < if h : b = 0 then 1 else Units.mk0 b h

Proof state:
case refine_3
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h : {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
⊢ G₀ → G₀ˣ

Tactic:
exact fun x ↦ if h : x = 0 then 1 else Units.mk0 x h

Result:
no goals

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

Tactic:
rw [← Set.wellFoundedOn_sdiff_singleton (a := 0)]

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