awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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
⊢ (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
have 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
Tactic: rcases eq_or_ne b 0 with rfl | hb
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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
⊢ (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
have 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
Tactic: rcases eq_or_ne b 0 with rfl | hb
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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 ℤ)
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
have refine_4 : LE.le (α := WithZero (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) :
      WithZero (Multiplicative ℤ))
    (↑(Equiv.toFun
          (MulEquiv.toEquiv
            ((Equiv.symm MulEquiv.withZero :
                (a : WithZero G₀ˣ ≃* WithZero (Multiplicative ℤ)) → G₀ˣ ≃* Multiplicative ℤ)
              (MulEquiv.trans WithZero.withZeroUnitsEquiv (↑f : G₀ ≃* WithZero (Multiplicative ℤ)))))
          b) :
      WithZero (Multiplicative ℤ)) ↔
  a ≤ b
Tactic: rw [← WithZero.coe_le_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
⊢ (WellFoundedOn {x : G₀ | g ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    Nonempty.{max 1 (u_2 + 1)} (G₀ ≃*o WithZero (Multiplicative ℤ))
have suffices : (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
Tactic: suffices Set.WellFoundedOn {x : G₀ | g ≤ x} (· < ·) ↔
    Set.WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} (· < ·) by
    rw [this, LinearOrderedCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete]
    refine Nonempty.congr (fun f ↦ ⟨?_, ?_⟩) (fun f ↦ ⟨?_, ?_⟩)
    · exact WithZero.withZeroUnitsEquiv.symm.trans f.withZero
    · intro a b
      rcases eq_or_ne a 0 with rfl | ha
      · simp [WithZero.withZeroUnitsEquiv]
      rcases eq_or_ne b 0 with rfl | hb
      · simp [WithZero.withZeroUnitsEquiv]
      simp [WithZero.withZeroUnitsEquiv, ha, hb, ← Units.val_le_val]
    · exact MulEquiv.withZero.symm (WithZero.withZeroUnitsEquiv.trans f)
    · intros
      rw [← WithZero.coe_le_coe]
      simp
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
⊢ (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
have rw : (WellFoundedOn ({x : G₀ | g ≤ x} \ {0}) fun (x1 x2 : G₀) ↦ x1 < x2) ↔
  WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
Tactic: rw [← Set.wellFoundedOn_sdiff_singleton (a := 0)]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
⊢ (WellFoundedOn ({x : G₀ | g ≤ x} \ {0}) fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
have refine_1 : ∀ (h : WellFoundedOn ({x : G₀ | g ≤ x} \ {0}) fun (x1 x2 : G₀) ↦ x1 < x2),
  MapsTo (α := G₀ˣ) Units.val {x : G₀ˣ | Units.mk0 g hg ≤ x} ({x : G₀ | g ≤ x} \ {0})
Tactic: refine ⟨fun h ↦ (h.mapsTo Units.val ?_).mono' ?_,
    fun h ↦ (h.mapsTo ?_ ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
refine_1 :
  ∀ (h : WellFoundedOn ({x : G₀ | g ≤ x} \ {0}) fun (x1 x2 : G₀) ↦ x1 < x2),
    MapsTo (α := G₀ˣ) Units.val {x : G₀ˣ | Units.mk0 g hg ≤ x} ({x : G₀ | g ≤ x} \ {0})
⊢ (WellFoundedOn ({x : G₀ | g ≤ x} \ {0}) fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
have refine_2 : ∀ (h : WellFoundedOn ({x : G₀ | g ≤ x} \ {0}) fun (x1 x2 : G₀) ↦ x1 < x2) (a : G₀ˣ),
  Membership.mem (γ := Set G₀ˣ) {x : G₀ˣ | Units.mk0 g hg ≤ x} a →
    ∀ (b : G₀ˣ),
      Membership.mem (γ := Set G₀ˣ) {x : G₀ˣ | Units.mk0 g hg ≤ x} b →
        a < b → Function.onFun (fun (x1 x2 : G₀) ↦ x1 < x2) Units.val a b
Tactic: refine ⟨fun h ↦ (h.mapsTo Units.val ?_).mono' ?_,
    fun h ↦ (h.mapsTo ?_ ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
refine_1 :
  ∀ (h : WellFoundedOn ({x : G₀ | g ≤ x} \ {0}) fun (x1 x2 : G₀) ↦ x1 < x2),
    MapsTo (α := G₀ˣ) Units.val {x : G₀ˣ | Units.mk0 g hg ≤ x} ({x : G₀ | g ≤ x} \ {0})
refine_2 :
  ∀ (h : WellFoundedOn ({x : G₀ | g ≤ x} \ {0}) fun (x1 x2 : G₀) ↦ x1 < x2) (a : G₀ˣ),
    Membership.mem (γ := Set G₀ˣ) {x : G₀ˣ | Units.mk0 g hg ≤ x} a →
      ∀ (b : G₀ˣ),
        Membership.mem (γ := Set G₀ˣ) {x : G₀ˣ | Units.mk0 g hg ≤ x} b →
          a < b → Function.onFun (fun (x1 x2 : G₀) ↦ x1 < x2) Units.val a b
⊢ (WellFoundedOn ({x : G₀ | g ≤ x} \ {0}) fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
have refine_3 : (h : WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2) → G₀ → G₀ˣ
Tactic: refine ⟨fun h ↦ (h.mapsTo Units.val ?_).mono' ?_,
    fun h ↦ (h.mapsTo ?_ ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
refine_1 :
  ∀ (h : WellFoundedOn ({x : G₀ | g ≤ x} \ {0}) fun (x1 x2 : G₀) ↦ x1 < x2),
    MapsTo (α := G₀ˣ) Units.val {x : G₀ˣ | Units.mk0 g hg ≤ x} ({x : G₀ | g ≤ x} \ {0})
refine_2 :
  ∀ (h : WellFoundedOn ({x : G₀ | g ≤ x} \ {0}) fun (x1 x2 : G₀) ↦ x1 < x2) (a : G₀ˣ),
    Membership.mem (γ := Set G₀ˣ) {x : G₀ˣ | Units.mk0 g hg ≤ x} a →
      ∀ (b : G₀ˣ),
        Membership.mem (γ := Set G₀ˣ) {x : G₀ˣ | Units.mk0 g hg ≤ x} b →
          a < b → Function.onFun (fun (x1 x2 : G₀) ↦ x1 < x2) Units.val a b
refine_3 : (h : WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2) → G₀ → G₀ˣ
⊢ (WellFoundedOn ({x : G₀ | g ≤ x} \ {0}) fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
have refine_4 : ∀ (h : WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2),
  MapsTo (β := G₀ˣ) (fun (x : G₀) ↦ if h : x = 0 then 1 else Units.mk0 x h) ({x : G₀ | g ≤ x} \ {0})
    {x : G₀ˣ | Units.mk0 g hg ≤ x}
Tactic: refine ⟨fun h ↦ (h.mapsTo Units.val ?_).mono' ?_,
    fun h ↦ (h.mapsTo ?_ ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
refine_1 :
  ∀ (h : WellFoundedOn ({x : G₀ | g ≤ x} \ {0}) fun (x1 x2 : G₀) ↦ x1 < x2),
    MapsTo (α := G₀ˣ) Units.val {x : G₀ˣ | Units.mk0 g hg ≤ x} ({x : G₀ | g ≤ x} \ {0})
refine_2 :
  ∀ (h : WellFoundedOn ({x : G₀ | g ≤ x} \ {0}) fun (x1 x2 : G₀) ↦ x1 < x2) (a : G₀ˣ),
    Membership.mem (γ := Set G₀ˣ) {x : G₀ˣ | Units.mk0 g hg ≤ x} a →
      ∀ (b : G₀ˣ),
        Membership.mem (γ := Set G₀ˣ) {x : G₀ˣ | Units.mk0 g hg ≤ x} b →
          a < b → Function.onFun (fun (x1 x2 : G₀) ↦ x1 < x2) Units.val a b
refine_3 : (h : WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2) → G₀ → G₀ˣ
refine_4 :
  ∀ (h : WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2),
    MapsTo (β := G₀ˣ) (fun (x : G₀) ↦ if h : x = 0 then 1 else Units.mk0 x h) ({x : G₀ | g ≤ x} \ {0})
      {x : G₀ˣ | Units.mk0 g hg ≤ x}
⊢ (WellFoundedOn ({x : G₀ | g ≤ x} \ {0}) fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
have refine_5 : ∀ (h : WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2) (a : G₀),
  Membership.mem (γ := Set G₀) ({x : G₀ | g ≤ x} \ {0}) a →
    ∀ (b : G₀),
      Membership.mem (γ := Set G₀) ({x : G₀ | g ≤ x} \ {0}) b →
        a < b → Function.onFun (fun (x1 x2 : G₀ˣ) ↦ x1 < x2) (fun (x : G₀) ↦ if h : x = 0 then 1 else Units.mk0 x h) a b
Tactic: refine ⟨fun h ↦ (h.mapsTo Units.val ?_).mono' ?_,
    fun h ↦ (h.mapsTo ?_ ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
h : WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
⊢ ∀ (a : G₀),
    Membership.mem (γ := Set G₀) ({x : G₀ | g ≤ x} \ {0}) a →
      ∀ (b : G₀),
        Membership.mem (γ := Set G₀) ({x : G₀ | g ≤ x} \ {0}) b →
          a < b →
            Function.onFun (fun (x1 x2 : G₀ˣ) ↦ x1 < x2) (fun (x : G₀) ↦ if h : x = 0 then 1 else Units.mk0 x h) a b
have refine_5 : ∀ (a : G₀),
  g ≤ a →
    ¬a = 0 →
      ∀ (b : G₀),
        g ≤ b →
          ¬b = 0 →
            a < b →
              LT.lt.{u_2} (α := G₀ˣ) (if h : a = 0 then 1 else Units.mk0 a h) (if h : b = 0 then 1 else Units.mk0 b h)
Tactic: simp only [mem_diff, mem_setOf_eq, mem_singleton_iff, Function.onFun, and_imp]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (hypothesis)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
⊢ (WellFoundedOn {x : G₀ | x ≤ g} fun (x1 x2 : G₀) ↦ x1 > x2) ↔
    Nonempty.{max 1 (u_2 + 1)} (G₀ ≃*o WithZero (Multiplicative ℤ))
have hg' : g⁻¹ ≠ 0
Tactic: have hg' : g⁻¹ ≠ 0 := by simp [hg]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
⊢ (WellFoundedOn {x : G₀ | x ≤ g} fun (x1 x2 : G₀) ↦ x1 > x2) ↔
    Nonempty.{max 1 (u_2 + 1)} (G₀ ≃*o WithZero (Multiplicative ℤ))
have rw : (WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) fun (x1 x2 : G₀) ↦ x1 > x2) ↔
  WellFoundedOn {x : G₀ | g⁻¹ ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2
Tactic: rw [← wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero hg',
    ← Set.wellFoundedOn_sdiff_singleton (a := 0)]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
⊢ (WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) fun (x1 x2 : G₀) ↦ x1 > x2) ↔
    WellFoundedOn {x : G₀ | g⁻¹ ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2
have refine_1 : ∀ (h : WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) fun (x1 x2 : G₀) ↦ x1 > x2),
  MapsTo (β := G₀) (fun (x : G₀) ↦ x⁻¹) {x : G₀ | g⁻¹ ≤ x} ({x : G₀ | x ≤ g} \ {0})
Tactic: refine ⟨fun h ↦ (h.mapsTo (·⁻¹) ?_).mono' ?_, fun h ↦ (h.mapsTo (·⁻¹) ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
refine_1 :
  ∀ (h : WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) fun (x1 x2 : G₀) ↦ x1 > x2),
    MapsTo (β := G₀) (fun (x : G₀) ↦ x⁻¹) {x : G₀ | g⁻¹ ≤ x} ({x : G₀ | x ≤ g} \ {0})
⊢ (WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) fun (x1 x2 : G₀) ↦ x1 > x2) ↔
    WellFoundedOn {x : G₀ | g⁻¹ ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2
have refine_2 : ∀ (h : WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) 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: refine ⟨fun h ↦ (h.mapsTo (·⁻¹) ?_).mono' ?_, fun h ↦ (h.mapsTo (·⁻¹) ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
refine_1 :
  ∀ (h : WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) fun (x1 x2 : G₀) ↦ x1 > x2),
    MapsTo (β := G₀) (fun (x : G₀) ↦ x⁻¹) {x : G₀ | g⁻¹ ≤ x} ({x : G₀ | x ≤ g} \ {0})
refine_2 :
  ∀ (h : WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) 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
⊢ (WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) fun (x1 x2 : G₀) ↦ x1 > x2) ↔
    WellFoundedOn {x : G₀ | g⁻¹ ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2
have refine_3 : ∀ (h : WellFoundedOn {x : G₀ | g⁻¹ ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2),
  MapsTo (β := G₀) (fun (x : G₀) ↦ x⁻¹) ({x : G₀ | x ≤ g} \ {0}) {x : G₀ | g⁻¹ ≤ x}
Tactic: refine ⟨fun h ↦ (h.mapsTo (·⁻¹) ?_).mono' ?_, fun h ↦ (h.mapsTo (·⁻¹) ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
refine_1 :
  ∀ (h : WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) fun (x1 x2 : G₀) ↦ x1 > x2),
    MapsTo (β := G₀) (fun (x : G₀) ↦ x⁻¹) {x : G₀ | g⁻¹ ≤ x} ({x : G₀ | x ≤ g} \ {0})
refine_2 :
  ∀ (h : WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) 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} \ {0}) {x : G₀ | g⁻¹ ≤ x}
⊢ (WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) fun (x1 x2 : G₀) ↦ x1 > x2) ↔
    WellFoundedOn {x : G₀ | g⁻¹ ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2
have refine_4 : ∀ (h : WellFoundedOn {x : G₀ | g⁻¹ ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2) (a : G₀),
  Membership.mem (γ := Set G₀) ({x : G₀ | x ≤ g} \ {0}) a →
    ∀ (b : G₀),
      Membership.mem (γ := Set G₀) ({x : G₀ | x ≤ g} \ {0}) b →
        a > b → Function.onFun (fun (x1 x2 : G₀) ↦ x1 < x2) (fun (x : G₀) ↦ x⁻¹) a b
Tactic: refine ⟨fun h ↦ (h.mapsTo (·⁻¹) ?_).mono' ?_, fun h ↦ (h.mapsTo (·⁻¹) ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) 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} \ {0}) ((fun (x : G₀) ↦ x⁻¹) x)
have refine_1 : Membership.mem (γ := Set G₀) {x : G₀ | g⁻¹ ≤ x} 0 →
  Membership.mem (γ := Set G₀) ({x : G₀ | x ≤ g} \ {0}) ((fun (x : G₀) ↦ x⁻¹) 0)
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) fun (x1 x2 : G₀) ↦ x1 > x2
x : G₀
refine_1 :
  Membership.mem (γ := Set G₀) {x : G₀ | g⁻¹ ≤ x} 0 →
    Membership.mem (γ := Set G₀) ({x : G₀ | x ≤ g} \ {0}) ((fun (x : G₀) ↦ x⁻¹) 0)
⊢ Membership.mem (γ := Set G₀) {x : G₀ | g⁻¹ ≤ x} x →
    Membership.mem (γ := Set G₀) ({x : G₀ | x ≤ g} \ {0}) ((fun (x : G₀) ↦ x⁻¹) x)
have refine_1₁ : ∀ (hx : x ≠ 0),
  Membership.mem (γ := Set G₀) {x : G₀ | g⁻¹ ≤ x} x →
    Membership.mem (γ := Set G₀) ({x : G₀ | x ≤ g} \ {0}) ((fun (x : G₀) ↦ x⁻¹) x)
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) fun (x1 x2 : G₀) ↦ x1 > x2
x : G₀
hx : x ≠ 0
⊢ Membership.mem (γ := Set G₀) {x : G₀ | g⁻¹ ≤ x} x →
    Membership.mem (γ := Set G₀) ({x : G₀ | x ≤ g} \ {0}) ((fun (x : G₀) ↦ x⁻¹) x)
have refine_1 : g⁻¹ ≤ x → x⁻¹ ≤ g
Tactic: simp only [mem_setOf_eq, mem_diff, mem_singleton_iff, inv_eq_zero, hx, not_false_eq_true,
      and_true]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) fun (x1 x2 : G₀) ↦ x1 > x2
x : G₀
hx : x ≠ 0
⊢ g⁻¹ ≤ x → x⁻¹ ≤ g
have refine_1 : 0 < g
Tactic: refine (inv_le_comm₀ ?_ ?_).mp
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) fun (x1 x2 : G₀) ↦ x1 > x2
x : G₀
hx : x ≠ 0
refine_1 : 0 < g
⊢ g⁻¹ ≤ x → x⁻¹ ≤ g
have refine_1₁ : 0 < x
Tactic: refine (inv_le_comm₀ ?_ ?_).mp
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) 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
have refine_2 : ∀ (a : G₀), g⁻¹ ≤ a → ∀ (b : G₀), g⁻¹ ≤ b → a < b → b⁻¹ < a⁻¹
Tactic: simp only [mem_setOf_eq, Function.onFun, gt_iff_lt]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) fun (x1 x2 : G₀) ↦ x1 > x2
a : G₀
ha : g⁻¹ ≤ a
b : G₀
h_1 : g⁻¹ ≤ b
⊢ a < b → b⁻¹ < a⁻¹
have refine_2 : 0 < a
Tactic: refine inv_strictAnti₀ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) fun (x1 x2 : G₀) ↦ x1 > x2
a : G₀
ha : g⁻¹ ≤ a
b : G₀
h_1 : g⁻¹ ≤ b
⊢ 0 < a
have refine_2 : ∀ (ha : a ≤ 0), a < g⁻¹
Tactic: contrapose! ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (hypothesis)
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) fun (x1 x2 : G₀) ↦ x1 > x2
a b : G₀
h_1 : g⁻¹ ≤ b
ha : a ≤ 0
⊢ a < g⁻¹
have ha₁ : a = 0
Tactic: simp only [le_zero_iff] at ha
Cleared hypotheses: ha