awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
suffices :
  (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔
    WellFoundedOn {x : Additive G | (e : (a : G) → Additive G) g ≤ x} fun (x1 x2 : Additive G) ↦ x1 < x2
⊢ (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃*o Multiplicative ℤ)

Tactic:
suffices Set.WellFoundedOn {x : G | g ≤ x} (· < ·) ↔ Set.WellFoundedOn {x | e g ≤ x} (· < ·) by
    rw [this, LinearOrderedAddCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete,
      OrderAddMonoidIso.toMultiplicativeRight.nonempty_congr]
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
⊢ (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔
    WellFoundedOn {x : Additive G | (e : (a : G) → Additive G) g ≤ x} fun (x1 x2 : Additive G) ↦ x1 < x2

Tactic:
⟨fun h ↦ (h.mapsTo e.symm fun _ ↦ e.le_symm_apply.mpr).mono' ?_,
    fun h ↦ (h.mapsTo e fun _ ↦ ?_).mono' ?_⟩

Premises used: Iff.mpr, Set.WellFoundedOn.mono', Set.WellFoundedOn.mapsTo, OrderIso.symm, Iff.intro, OrderIso.le_symm_apply, DFunLike.coe
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
refine_1 :
  ∀ (h : WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) (a : Additive G),
    Membership.mem (γ := Set (Additive G))
        (fun (x : Additive G) ↦ (instLEAdditive : LE (Additive G)).1 ((e : (a : G) → Additive G) g) x) a →
      ∀ (b : Additive G),
        Membership.mem (γ := Set (Additive G))
            (fun (x : Additive G) ↦ (instLEAdditive : LE (Additive G)).1 ((e : (a : G) → Additive G) g) x) b →
          a < b → Function.onFun (fun (x1 x2 : G) ↦ x1 < x2) (⇑e.symm : (a : Additive G) → G) a b
refine_2 :
  ∀ (h : WellFoundedOn {x : Additive G | (e : (a : G) → Additive G) g ≤ x} fun (x1 x2 : Additive G) ↦ x1 < x2) (x : G),
    Membership.mem (γ := Set G) {x : G | g ≤ x} x →
      Membership.mem (α := Additive G) (γ := Set (Additive G)) {x : Additive G | (e : (a : G) → Additive G) g ≤ x}
        ((e : (a : G) → Additive G) x : Additive G)
refine_3 :
  ∀ (h : WellFoundedOn {x : Additive G | (e : (a : G) → Additive G) g ≤ x} fun (x1 x2 : Additive G) ↦ x1 < x2) (a : G),
    Membership.mem (γ := Set G) {x : G | g ≤ x} a →
      ∀ (b : G),
        Membership.mem (γ := Set G) {x : G | g ≤ x} b →
          a < b → Function.onFun (fun (x1 x2 : Additive G) ↦ x1 < x2) (⇑e : (a : G) → Additive G) a b
⊢ (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔
    WellFoundedOn {x : Additive G | (e : (a : G) → Additive G) g ≤ x} fun (x1 x2 : Additive G) ↦ x1 < x2

Tactic:
refine ⟨fun h ↦ (h.mapsTo e.symm fun _ ↦ e.le_symm_apply.mpr).mono' ?_,
    fun h ↦ (h.mapsTo e fun _ ↦ ?_).mono' ?_⟩
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
h : WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2
⊢ ∀ (a : Additive G),
    Membership.mem (γ := Set (Additive G))
        (fun (x : Additive G) ↦ (instLEAdditive : LE (Additive G)).1 ((e : (a : G) → Additive G) g) x) a →
      ∀ (b : Additive G),
        Membership.mem (γ := Set (Additive G))
            (fun (x : Additive G) ↦ (instLEAdditive : LE (Additive G)).1 ((e : (a : G) → Additive G) g) x) b →
          a < b → Function.onFun (fun (x1 x2 : G) ↦ x1 < x2) (⇑e.symm : (a : Additive G) → G) a b

Tactic:
simp [Function.onFun]

Premises used: Function.onFun
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
h : WellFoundedOn {x : Additive G | (e : (a : G) → Additive G) g ≤ x} fun (x1 x2 : Additive G) ↦ x1 < x2
x : G
⊢ Membership.mem (γ := Set G) {x : G | g ≤ x} x →
    Membership.mem (α := Additive G) (γ := Set (Additive G)) {x : Additive G | (e : (a : G) → Additive G) g ≤ x}
      ((e : (a : G) → Additive G) x : Additive G)

Tactic:
simp [Function.onFun]

Premises used: Function.onFun
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
h : WellFoundedOn {x : Additive G | (e : (a : G) → Additive G) g ≤ x} fun (x1 x2 : Additive G) ↦ x1 < x2
⊢ ∀ (a : G),
    Membership.mem (γ := Set G) {x : G | g ≤ x} a →
      ∀ (b : G),
        Membership.mem (γ := Set G) {x : G | g ≤ x} b →
          a < b → Function.onFun (fun (x1 x2 : Additive G) ↦ x1 < x2) (⇑e : (a : G) → Additive G) a b

Tactic:
simp [Function.onFun]

Premises used: Function.onFun
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
rw :
  (WellFoundedOn {x : G | x ≤ g} fun (x1 x2 : G) ↦ x1 > x2) ↔ WellFoundedOn {x : G | g⁻¹ ≤ x} fun (x1 x2 : G) ↦ x1 < x2
⊢ (WellFoundedOn {x : G | x ≤ g} fun (x1 x2 : G) ↦ x1 > x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃*o Multiplicative ℤ)

Tactic:
rw [← wellFoundedOn_setOf_le_lt_iff_nonempty_discrete (g := g⁻¹)]

Premises used: LinearOrderedCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
⊢ (WellFoundedOn {x : G | x ≤ g} fun (x1 x2 : G) ↦ x1 > x2) ↔ WellFoundedOn {x : G | g⁻¹ ≤ x} fun (x1 x2 : G) ↦ x1 < x2

Tactic:
⟨fun h ↦ (h.mapsTo (·⁻¹) ?_).mono' ?_, fun h ↦ (h.mapsTo (·⁻¹) ?_).mono' ?_⟩

Premises used: Set.WellFoundedOn.mono', Set.WellFoundedOn.mapsTo, Inv.inv, Iff.intro
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
refine_1 :
  ∀ (h : WellFoundedOn {x : G | x ≤ g} fun (x1 x2 : G) ↦ x1 > x2),
    MapsTo (β := G) (fun (x : G) ↦ x⁻¹) {x : G | g⁻¹ ≤ x} {x : G | x ≤ g}
refine_2 :
  ∀ (h : WellFoundedOn {x : G | x ≤ g} fun (x1 x2 : G) ↦ x1 > x2) (a : G),
    Membership.mem (γ := Set G) {x : G | g⁻¹ ≤ x} a →
      ∀ (b : G),
        Membership.mem (γ := Set G) {x : G | g⁻¹ ≤ x} b →
          a < b → Function.onFun (fun (x1 x2 : G) ↦ x1 > x2) (fun (x : G) ↦ x⁻¹) a b
refine_3 :
  ∀ (h : WellFoundedOn {x : G | g⁻¹ ≤ x} fun (x1 x2 : G) ↦ x1 < x2),
    MapsTo (β := G) (fun (x : G) ↦ x⁻¹) {x : G | x ≤ g} {x : G | g⁻¹ ≤ x}
refine_4 :
  ∀ (h : WellFoundedOn {x : G | g⁻¹ ≤ x} fun (x1 x2 : G) ↦ x1 < x2) (a : G),
    Membership.mem (γ := Set G) {x : G | x ≤ g} a →
      ∀ (b : G),
        Membership.mem (γ := Set G) {x : G | x ≤ g} b →
          a > b → Function.onFun (fun (x1 x2 : G) ↦ x1 < x2) (fun (x : G) ↦ x⁻¹) a b
⊢ (WellFoundedOn {x : G | x ≤ g} fun (x1 x2 : G) ↦ x1 > x2) ↔ WellFoundedOn {x : G | g⁻¹ ≤ x} fun (x1 x2 : G) ↦ x1 < x2

Tactic:
refine ⟨fun h ↦ (h.mapsTo (·⁻¹) ?_).mono' ?_, fun h ↦ (h.mapsTo (·⁻¹) ?_).mono' ?_⟩
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
h : WellFoundedOn {x : G | x ≤ g} fun (x1 x2 : G) ↦ x1 > x2
x : G
⊢ Membership.mem (γ := Set G) {x : G | g⁻¹ ≤ x} x → Membership.mem (γ := Set G) {x : G | x ≤ g} ((fun (x : G) ↦ x⁻¹) x)

Tactic:
simp [Function.onFun, inv_le']

Premises used: inv_le', Function.onFun
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
h : WellFoundedOn {x : G | x ≤ g} fun (x1 x2 : G) ↦ x1 > x2
a : G
⊢ Membership.mem (γ := Set G) {x : G | g⁻¹ ≤ x} a →
    ∀ (b : G),
      Membership.mem (γ := Set G) {x : G | g⁻¹ ≤ x} b →
        a < b → Function.onFun (fun (x1 x2 : G) ↦ x1 > x2) (fun (x : G) ↦ x⁻¹) a b

Tactic:
simp [Function.onFun, inv_le']

Premises used: inv_le', Function.onFun
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
h : WellFoundedOn {x : G | g⁻¹ ≤ x} fun (x1 x2 : G) ↦ x1 < x2
x : G
⊢ Membership.mem (γ := Set G) {x : G | x ≤ g} x → Membership.mem (γ := Set G) {x : G | g⁻¹ ≤ x} ((fun (x : G) ↦ x⁻¹) x)

Tactic:
simp [Function.onFun, inv_le']

Premises used: inv_le', Function.onFun
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
g : G
h : WellFoundedOn {x : G | g⁻¹ ≤ x} fun (x1 x2 : G) ↦ x1 < x2
a : G
⊢ Membership.mem (γ := Set G) {x : G | x ≤ g} a →
    ∀ (b : G),
      Membership.mem (γ := Set G) {x : G | x ≤ g} b →
        a > b → Function.onFun (fun (x1 x2 : G) ↦ x1 < x2) (fun (x : G) ↦ x⁻¹) a b

Tactic:
simp [Function.onFun, inv_le']

Premises used: inv_le', Function.onFun
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
this :
  (WellFoundedOn {x : G₀ | g ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
rw : Nonempty.{u_2 + 1} (G₀ˣ ≃*o Multiplicative ℤ) ↔ Nonempty.{max 1 (u_2 + 1)} (G₀ ≃*o WithZero (Multiplicative ℤ))
⊢ (WellFoundedOn {x : G₀ | g ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    Nonempty.{max 1 (u_2 + 1)} (G₀ ≃*o WithZero (Multiplicative ℤ))

Tactic:
rw [this, LinearOrderedCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete]

Premises used: LinearOrderedCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
this :
  (WellFoundedOn {x : G₀ | g ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
⊢ Nonempty.{u_2 + 1} (G₀ˣ ≃*o Multiplicative ℤ) ↔ Nonempty.{max 1 (u_2 + 1)} (G₀ ≃*o WithZero (Multiplicative ℤ))

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

Premises used: Nonempty.congr, OrderMonoidIso.mk
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
this :
  (WellFoundedOn {x : G₀ | g ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
refine_1 : (f : G₀ˣ ≃*o Multiplicative ℤ) → G₀ ≃* WithZero (Multiplicative ℤ)
refine_2 :
  ∀ (f : G₀ˣ ≃*o Multiplicative ℤ) {a b : G₀},
    (MulEquiv.toEquiv
              (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
                (↑((OrderMonoidIso.withZero :
                          (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                        f :
                      WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                  WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
          a ≤
        (MulEquiv.toEquiv
              (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
                (↑((OrderMonoidIso.withZero :
                          (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                        f :
                      WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                  WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
          b ↔
      a ≤ b
refine_3 : (f : G₀ ≃*o WithZero (Multiplicative ℤ)) → G₀ˣ ≃* Multiplicative ℤ
refine_4 :
  ∀ (f : G₀ ≃*o WithZero (Multiplicative ℤ)) {a b : G₀ˣ},
    LE.le (α := Multiplicative ℤ)
        (Equiv.toFun
          (MulEquiv.toEquiv
            ((Equiv.symm MulEquiv.withZero :
                (a : WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)) → G₀ˣ ≃* Multiplicative ℤ)
              (MulEquiv.trans WithZero.withZeroUnitsEquiv (↑f : G₀ ≃* WithZero (Multiplicative ℤ)))))
          a)
        (Equiv.toFun
          (MulEquiv.toEquiv
            ((Equiv.symm MulEquiv.withZero :
                (a : WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)) → G₀ˣ ≃* Multiplicative ℤ)
              (MulEquiv.trans WithZero.withZeroUnitsEquiv (↑f : G₀ ≃* WithZero (Multiplicative ℤ)))))
          b) ↔
      a ≤ b
⊢ Nonempty.{u_2 + 1} (G₀ˣ ≃*o Multiplicative ℤ) ↔ Nonempty.{max 1 (u_2 + 1)} (G₀ ≃*o WithZero (Multiplicative ℤ))

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

Premises used: Nonempty.congr
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
this :
  (WellFoundedOn {x : G₀ | g ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
f : G₀ˣ ≃*o Multiplicative ℤ
⊢ G₀ ≃* WithZero (Multiplicative ℤ)

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

Premises used: MulEquiv.trans, WithZero.withZeroUnitsEquiv, MulEquiv.symm
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
this :
  (WellFoundedOn {x : G₀ | g ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
f : G₀ˣ ≃*o Multiplicative ℤ
a b : G₀
refine_2 :
  (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        0 ≤
      (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        b ↔
    0 ≤ b
refine_2₁ :
  ∀ (ha : a ≠ 0),
    (MulEquiv.toEquiv
              (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
                (↑((OrderMonoidIso.withZero :
                          (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                        f :
                      WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                  WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
          a ≤
        (MulEquiv.toEquiv
              (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
                (↑((OrderMonoidIso.withZero :
                          (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                        f :
                      WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                  WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
          b ↔
      a ≤ b
⊢ (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        a ≤
      (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        b ↔
    a ≤ b

Tactic:
rcases eq_or_ne a 0 with rfl | ha

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
this :
  (WellFoundedOn {x : G₀ | g ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
f : G₀ˣ ≃*o Multiplicative ℤ
b : G₀
⊢ (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        0 ≤
      (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        b ↔
    0 ≤ b

Tactic:
simp [WithZero.withZeroUnitsEquiv]

Premises used: WithZero.withZeroUnitsEquiv
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
this :
  (WellFoundedOn {x : G₀ | g ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
f : G₀ˣ ≃*o Multiplicative ℤ
a b : G₀
ha : a ≠ 0
refine_2 :
  (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        a ≤
      (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        0 ↔
    a ≤ 0
refine_2₁ :
  ∀ (hb : b ≠ 0),
    (MulEquiv.toEquiv
              (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
                (↑((OrderMonoidIso.withZero :
                          (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                        f :
                      WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                  WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
          a ≤
        (MulEquiv.toEquiv
              (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
                (↑((OrderMonoidIso.withZero :
                          (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                        f :
                      WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                  WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
          b ↔
      a ≤ b
⊢ (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        a ≤
      (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        b ↔
    a ≤ b

Tactic:
rcases eq_or_ne b 0 with rfl | hb

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
this :
  (WellFoundedOn {x : G₀ | g ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
f : G₀ˣ ≃*o Multiplicative ℤ
a : G₀
ha : a ≠ 0
⊢ (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        a ≤
      (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        0 ↔
    a ≤ 0

Tactic:
simp [WithZero.withZeroUnitsEquiv]

Premises used: WithZero.withZeroUnitsEquiv
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
this :
  (WellFoundedOn {x : G₀ | g ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
f : G₀ˣ ≃*o Multiplicative ℤ
a b : G₀
ha : a ≠ 0
hb : b ≠ 0
⊢ (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        a ≤
      (MulEquiv.toEquiv
            (MulEquiv.trans (MulEquiv.symm WithZero.withZeroUnitsEquiv)
              (↑((OrderMonoidIso.withZero :
                        (a : G₀ˣ ≃*o Multiplicative ℤ) → WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ))
                      f :
                    WithZero G₀ˣ ≃*o WithZero (Multiplicative ℤ)) :
                WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)))).toFun
        b ↔
    a ≤ b

Tactic:
simp [WithZero.withZeroUnitsEquiv, ha, hb, ← Units.val_le_val]

Premises used: WithZero.withZeroUnitsEquiv, Units.val_le_val
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
this :
  (WellFoundedOn {x : G₀ | g ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
f : G₀ ≃*o WithZero (Multiplicative ℤ)
⊢ G₀ˣ ≃* Multiplicative ℤ

Tactic:
exact MulEquiv.withZero.symm (WithZero.withZeroUnitsEquiv.trans f)

Premises used: MulEquiv.trans, WithZero.withZeroUnitsEquiv, MulEquiv.withZero, Equiv.symm, DFunLike.coe