-- 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_2
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₀},
    (WithZero.withZeroUnitsEquiv.symm.trans f.withZero).toFun a ≤
        (WithZero.withZeroUnitsEquiv.symm.trans f.withZero).toFun b ↔
      a ≤ b

Tactic:
intro a b

Result:
case refine_2
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₀
⊢ (WithZero.withZeroUnitsEquiv.symm.trans f.withZero).toFun a ≤
      (WithZero.withZeroUnitsEquiv.symm.trans f.withZero).toFun b ↔
    a ≤ b

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

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

Result:
no goals

Proof state:
case refine_2
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₀
⊢ (WithZero.withZeroUnitsEquiv.symm.trans f.withZero).toFun a ≤
      (WithZero.withZeroUnitsEquiv.symm.trans f.withZero).toFun b ↔
    a ≤ b

Tactic:
rcases eq_or_ne a 0 with rfl|ha

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

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

Proof state:
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 (fun x => if h : x = 0 then 1 else Units.mk0 x h) ({x | g ≤ x} \ {0}) {x | Units.mk0 g hg ≤ x}

Tactic:
simp +contextual [← Units.val_le_val, MapsTo]

Result:
no goals

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

Tactic:
simp [Function.onFun]

Result:
no goals

Proof state:
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
⊢ ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ Nonempty (G₀ ≃*o ℤₘ₀)

Tactic:
rw [this, LinearOrderedCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete]

Result:
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
⊢ Nonempty (G₀ˣ ≃*o Multiplicative ℤ) ↔ Nonempty (G₀ ≃*o ℤₘ₀)

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

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:
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
⊢ Nonempty (G₀ˣ ≃*o Multiplicative ℤ) ↔ Nonempty (G₀ ≃*o ℤₘ₀)

Tactic:
refine Nonempty.congr (fun f ↦ ⟨?_, ?_⟩) (fun f ↦ ⟨?_, ?_⟩)

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

case refine_2
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₀}, (MulEquiv.toEquiv ?refine_1).toFun a ≤ (MulEquiv.toEquiv ?refine_1).toFun b ↔ a ≤ b

case refine_3
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 ℤₘ₀
⊢ G₀ˣ ≃* Multiplicative ℤ

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₀ˣ}, (MulEquiv.toEquiv ?refine_3).toFun a ≤ (MulEquiv.toEquiv ?refine_3).toFun b ↔ a ≤ b

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
x✝ : G₀ˣ
⊢ x✝ ∈ {x | Units.mk0 g hg ≤ x} → ↑x✝ ∈ {x | g ≤ x} \ {0}

Tactic:
simp [← Units.val_le_val]

Result:
no goals

Proof state:
case refine_3
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 ℤₘ₀
⊢ G₀ˣ ≃* Multiplicative ℤ

Tactic:
exact MulEquiv.unzero (WithZero.withZeroUnitsEquiv.trans f)

Result:
no goals