awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ℤ)
a b : G₀ˣ
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
⊢ 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

Tactic:
rw [← WithZero.coe_le_coe]

Premises used: WithZero.coe_le_coe
-- 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 ℤ)
a b : G₀ˣ
⊢ 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:
simp
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
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
⊢ (WellFoundedOn {x : G₀ | g ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2) ↔
    Nonempty.{max 1 (u_2 + 1)} (G₀ ≃*o WithZero (Multiplicative ℤ))

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
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
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
⊢ (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:
rw [← Set.wellFoundedOn_sdiff_singleton (a := 0)]

Premises used: Set.wellFoundedOn_sdiff_singleton
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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

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

Premises used: Units.val, Set.WellFoundedOn.mono', Set.WellFoundedOn.mapsTo, Iff.intro
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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}
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
⊢ (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:
refine ⟨fun h ↦ (h.mapsTo Units.val ?_).mono' ?_,
    fun h ↦ (h.mapsTo ?_ ?_).mono' ?_⟩
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
h : WellFoundedOn ({x : G₀ | g ≤ x} \ {0}) fun (x1 x2 : G₀) ↦ x1 < x2
x : G₀ˣ
⊢ Membership.mem (γ := Set G₀ˣ) {x : G₀ˣ | Units.mk0 g hg ≤ x} x →
    Membership.mem (γ := Set G₀) ({x : G₀ | g ≤ x} \ {0}) (↑x : G₀)

Tactic:
simp [← Units.val_le_val]

Premises used: 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
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:
simp [Function.onFun]

Premises used: 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
h : WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
⊢ G₀ → G₀ˣ

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

Premises used: dite, Units.mk0, OfNat.ofNat, Eq
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
⊢ 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:
simp +contextual [← Units.val_le_val, MapsTo]

Premises used: Units.val_le_val, Set.MapsTo
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
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)
⊢ ∀ (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:
simp only [mem_diff, mem_setOf_eq, mem_singleton_iff, Function.onFun, and_imp]

Premises used: Function.onFun, and_imp, Set.mem_setOf_eq, Set.mem_singleton_iff, Set.mem_diff
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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₀
refine_5 :
  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)
⊢ 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:
_
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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₀
h_1 : g ≤ a
ha0 : ¬a = 0
refine_5 :
  ∀ (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)
⊢ ∀ (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:
_
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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₀
h_1 : g ≤ a
ha0 : ¬a = 0
b : G₀
refine_5 :
  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)
⊢ 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:
_
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
h_1 : WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} fun (x1 x2 : G₀ˣ) ↦ x1 < x2
a : G₀
h_2 : g ≤ a
ha0 : ¬a = 0
b : G₀
h_3 : g ≤ b
hb0 : ¬b = 0
h : 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 [ha0, hb0, ← Units.val_lt_val, h]

Premises used: Units.val_lt_val
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
⊢ g⁻¹ ≠ 0

Tactic:
simp [hg]
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
⊢ g⁻¹ ≠ 0

Tactic:
have hg' : g⁻¹ ≠ 0 := by simp [hg]
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G₀ : Type u_2
inst : LinearOrderedCommGroupWithZero G₀
inst_1 : Nontrivial.{u_2} G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
rw :
  (WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) 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 WithZero (Multiplicative ℤ))

Tactic:
rw [← wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero hg',
    ← Set.wellFoundedOn_sdiff_singleton (a := 0)]

Premises used: Set.wellFoundedOn_sdiff_singleton, LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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

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 : 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}
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
⊢ (WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) 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 : 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)
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)
⊢ 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

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
hg' : g⁻¹ ≠ 0
h : WellFoundedOn ({x : G₀ | x ≤ g} \ {0}) fun (x1 x2 : G₀) ↦ x1 > x2
⊢ Membership.mem (γ := Set G₀) {x : G₀ | g⁻¹ ≤ x} 0 →
    Membership.mem (γ := Set G₀) ({x : G₀ | x ≤ g} \ {0}) ((fun (x : G₀) ↦ x⁻¹) 0)

Tactic:
simp [hg]
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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 : g⁻¹ ≤ x → 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)

Tactic:
simp only [mem_setOf_eq, mem_diff, mem_singleton_iff, inv_eq_zero, hx, not_false_eq_true,
      and_true]

Premises used: inv_eq_zero, and_true, Set.mem_setOf_eq, Set.mem_singleton_iff, Set.mem_diff, not_false_eq_true
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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

Tactic:
(inv_le_comm₀ ?_ ?_).mp

Premises used: inv_le_comm₀, Iff.mp
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
refine_1₁ : 0 < x
⊢ g⁻¹ ≤ x → x⁻¹ ≤ g

Tactic:
refine (inv_le_comm₀ ?_ ?_).mp

Premises used: inv_le_comm₀, Iff.mp
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
⊢ 0 < g

Tactic:
simp [zero_lt_iff, hg, hx]

Premises used: zero_lt_iff
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
⊢ 0 < x

Tactic:
simp [zero_lt_iff, hg, hx]

Premises used: zero_lt_iff
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
refine_2 : ∀ (a : G₀), g⁻¹ ≤ a → ∀ (b : G₀), g⁻¹ ≤ b → a < b → b⁻¹ < a⁻¹
⊢ ∀ (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 only [mem_setOf_eq, Function.onFun, gt_iff_lt]

Premises used: Function.onFun, Set.mem_setOf_eq, gt_iff_lt
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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₀
refine_2 : g⁻¹ ≤ b → a < b → b⁻¹ < a⁻¹
⊢ g⁻¹ ≤ b → a < b → b⁻¹ < a⁻¹

Tactic:
_
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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⁻¹

Tactic:
inv_strictAnti₀ ?_

Premises used: inv_strictAnti₀
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
refine_2 : 0 < a
⊢ a < b → b⁻¹ < a⁻¹

Tactic:
refine inv_strictAnti₀ ?_

Premises used: inv_strictAnti₀
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
refine_2 : ∀ (ha : a ≤ 0), a < g⁻¹
⊢ 0 < a

Tactic:
contrapose! ha
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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 = 0

Tactic:
simp only [le_zero_iff] at ha

Premises used: le_zero_iff
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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⁻¹

Tactic:
simp [zero_lt_iff, ha, hg]

Premises used: zero_lt_iff
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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₀ | g⁻¹ ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2
x : G₀
refine_3 : x ≤ g → ¬x = 0 → g⁻¹ ≤ x⁻¹
⊢ Membership.mem (γ := Set G₀) ({x : G₀ | x ≤ g} \ {0}) x →
    Membership.mem (γ := Set G₀) {x : G₀ | g⁻¹ ≤ x} ((fun (x : G₀) ↦ x⁻¹) x)

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

Premises used: and_imp, Set.mem_setOf_eq, Set.mem_singleton_iff, Set.mem_diff
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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₀ | g⁻¹ ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2
x : G₀
hxg : x ≤ g
hx : ¬x = 0
⊢ g⁻¹ ≤ x⁻¹

Tactic:
inv_anti₀ ?_ hxg

Premises used: inv_anti₀
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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₀ | g⁻¹ ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2
x : G₀
hxg : x ≤ g
hx : ¬x = 0
refine_3 : 0 < x
⊢ g⁻¹ ≤ x⁻¹

Tactic:
refine inv_anti₀ ?_ hxg

Premises used: inv_anti₀
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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₀ | g⁻¹ ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2
x : G₀
hxg : x ≤ g
hx : ¬x = 0
⊢ 0 < x

Tactic:
simp [zero_lt_iff, hx]

Premises used: zero_lt_iff
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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₀ | g⁻¹ ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2
refine_4 : ∀ a ≤ g, ¬a = 0 → ∀ b ≤ g, ¬b = 0 → b < a → a⁻¹ < b⁻¹
⊢ ∀ (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:
simp only [mem_diff, mem_setOf_eq, mem_singleton_iff, gt_iff_lt, Function.onFun, and_imp]

Premises used: Function.onFun, and_imp, Set.mem_setOf_eq, Set.mem_singleton_iff, Set.mem_diff, gt_iff_lt
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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₀ | g⁻¹ ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2
a : G₀
refine_4 : a ≤ g → ¬a = 0 → ∀ b ≤ g, ¬b = 0 → b < a → a⁻¹ < b⁻¹
⊢ a ≤ g → ¬a = 0 → ∀ b ≤ g, ¬b = 0 → b < a → a⁻¹ < b⁻¹

Tactic:
_
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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₀ | g⁻¹ ≤ x} fun (x1 x2 : G₀) ↦ x1 < x2
a : G₀
h_1 : a ≤ g
refine_4 : ¬a = 0 → ∀ b ≤ g, ¬b = 0 → b < a → a⁻¹ < b⁻¹
⊢ ¬a = 0 → ∀ b ≤ g, ¬b = 0 → b < a → a⁻¹ < b⁻¹

Tactic:
_