awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
this : (WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
h : WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2
refine_4 :
  ∀ (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 - g) a b
⊢ ∀ (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 - g) a b

Tactic:
try intro
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
this : (WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
h : WellFoundedOn {x : G | 0 ≤ x} 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 - g) a b

Tactic:
simp [Function.onFun]

Premises used: Function.onFun
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
suffices : (WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
⊢ (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)

Tactic:
suffices Set.WellFoundedOn {x : G | 0 ≤ x} (· < ·) ↔ Nonempty (G ≃+o ℤ) by
    rw [← this]
    refine ⟨fun h ↦ (h.mapsTo (· + g) ?_).mono' ?_, fun h ↦ (h.mapsTo (· - g) ?_).mono' ?_⟩ <;>
    · try intro
      simp [Function.onFun]
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
mp : (WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2) → Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
mpr : Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) → WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2
⊢ (WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)

Tactic:
constructor
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
h : WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2
⊢ WellFounded fun (x1 x2 : (↑{x : G | 0 ≤ x} : Type u_2)) ↦ x1 < x2

Tactic:
replace h : WellFounded (α := {x : G | 0 ≤ x}) (· < ·) := h
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
h : WellFounded fun (x1 x2 : (↑{x : G | 0 ≤ x} : Type u_2)) ↦ x1 < x2
⊢ ∀ (s : Set (↑{x : G | 0 ≤ x} : Type u_2)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m

Tactic:
rw [WellFounded.wellFounded_iff_has_min] at h

Premises used: WellFounded.wellFounded_iff_has_min
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
h : ∀ (s : Set (↑{x : G | 0 ≤ x} : Type u_2)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
pos : ∀ (H : ∀ (x : G) {y : G}, 0 < y → ∃ (n : ℕ), x ≤ n • y), Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
neg : ∀ (H : ∃ (x : G) (y : G), 0 < y ∧ ∀ (n : ℕ), n • y < x), Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)

Tactic:
by_cases! H : ∀ (x : G) {y}, 0 < y → ∃ n : ℕ, x ≤ n • y
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
h : ∀ (s : Set (↑{x : G | 0 ≤ x} : Type u_2)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : ∀ (x : G) {y : G}, 0 < y → ∃ (n : ℕ), x ≤ n • y
⊢ Archimedean G

Tactic:
replace H : Archimedean G := ⟨H⟩
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
h : ∀ (s : Set (↑{x : G | 0 ≤ x} : Type u_2)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
pos : ¬DenselyOrdered G
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)

Tactic:
rw [LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered]

Premises used: LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
h : ∀ (s : Set (↑{x : G | 0 ≤ x} : Type u_2)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
pos : ∀ (y : G) (hy : y ≠ 0), False
⊢ False

Tactic:
obtain ⟨y, hy⟩ := exists_ne (0 : G)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
h : ∀ (s : Set (↑{x : G | 0 ≤ x} : Type u_2)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
pos : ∀ (this : ∀ (y : G) (hy : y ≠ 0) (hy' : 0 < y), False) (hy' : y ≤ 0), False
wlog! : ∀ (y : G) (hy : y ≠ 0) (hy' : 0 < y), False
⊢ False

Tactic:
wlog! hy' : 0 < y generalizing y
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
h : ∀ (s : Set (↑{x : G | 0 ≤ x} : Type u_2)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
this : ∀ (y : G) (hy : y ≠ 0) (hy' : 0 < y), False
hy' : y ≤ 0
⊢ False

Tactic:
this (-y) ?_ ?_

Premises used: Neg.neg
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
h : ∀ (s : Set (↑{x : G | 0 ≤ x} : Type u_2)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
this : ∀ (y : G) (hy : y ≠ 0) (hy' : 0 < y), False
hy' : y ≤ 0
pos : -y ≠ 0
pos₁ : 0 < -y
⊢ False

Tactic:
refine this (-y) ?_ ?_

Premises used: Neg.neg
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
h : ∀ (s : Set (↑{x : G | 0 ≤ x} : Type u_2)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
this : ∀ (y : G) (hy : y ≠ 0) (hy' : 0 < y), False
hy' : y ≤ 0
⊢ -y ≠ 0

Tactic:
simp [hy]
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
h : ∀ (s : Set (↑{x : G | 0 ≤ x} : Type u_2)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
this : ∀ (y : G) (hy : y ≠ 0) (hy' : 0 < y), False
hy' : y ≤ 0
⊢ 0 < -y

Tactic:
simp [lt_of_le_of_ne hy' hy]

Premises used: lt_of_le_of_ne
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
h : ∀ (s : Set (↑{x : G | 0 ≤ x} : Type u_2)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
hy' : 0 < y
obtain :
  ∀ (z : G) (hz : Membership.mem (γ := Set G) {x : G | 0 ≤ x} z)
    (hz' :
      Membership.mem (γ := Set (↑{x : G | 0 ≤ x} : Type u_2))
        {x : (↑{x : G | 0 ≤ x} : Type u_2) |
          Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) 0 ⋯ < x}
        (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) z hz))
    (hz'' :
      ∀ (x : (↑{x : G | 0 ≤ x} : Type u_2)),
        Membership.mem (γ := Set (↑{x : G | 0 ≤ x} : Type u_2))
            {x : (↑{x : G | 0 ≤ x} : Type u_2) |
              Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) 0 ⋯ < x}
            x →
          ¬x < Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) z hz),
    False
⊢ False

Tactic:
obtain ⟨⟨z, hz⟩, hz', hz''⟩ := h ({x | ⟨0, le_rfl⟩ < x}) ⟨⟨y, hy'.le⟩, hy'⟩

Premises used: le_rfl, setOf, LT.lt.le, Subtype.mk, LT.lt, Exists.intro, OfNat.ofNat
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
h : ∀ (s : Set (↑{x : G | 0 ≤ x} : Type u_2)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
hy' : 0 < y
z : G
hz : Membership.mem (γ := Set G) {x : G | 0 ≤ x} z
hz' :
  Membership.mem (γ := Set (↑{x : G | 0 ≤ x} : Type u_2))
    {x : (↑{x : G | 0 ≤ x} : Type u_2) |
      Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) 0 ⋯ < x}
    (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) z hz)
hz'' :
  ∀ (x : (↑{x : G | 0 ≤ x} : Type u_2)),
    Membership.mem (γ := Set (↑{x : G | 0 ≤ x} : Type u_2))
        {x : (↑{x : G | 0 ≤ x} : Type u_2) |
          Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) 0 ⋯ < x}
        x →
      ¬x < Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) z hz
obtain :
  ∀ (w : G) (hw : (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) 0 ⋯) : G) < w)
    (hw' : w < (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) z hz) : G)), False
⊢ False

Tactic:
obtain ⟨w, hw, hw'⟩ := exists_between hz'

Premises used: exists_between
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
h : ∀ (s : Set (↑{x : G | 0 ≤ x} : Type u_2)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
hy' : 0 < y
z : G
hz : Membership.mem (γ := Set G) {x : G | 0 ≤ x} z
hz' :
  Membership.mem (γ := Set (↑{x : G | 0 ≤ x} : Type u_2))
    {x : (↑{x : G | 0 ≤ x} : Type u_2) |
      Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) 0 ⋯ < x}
    (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) z hz)
hz'' :
  ∀ (x : (↑{x : G | 0 ≤ x} : Type u_2)),
    Membership.mem (γ := Set (↑{x : G | 0 ≤ x} : Type u_2))
        {x : (↑{x : G | 0 ≤ x} : Type u_2) |
          Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) 0 ⋯ < x}
        x →
      ¬x < Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) z hz
w : G
hw : (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) 0 ⋯) : G) < w
hw' : w < (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) z hz) : G)
⊢ False

Tactic:
hz'' ⟨w, hw.le⟩ hw hw'

Premises used: LT.lt.le, Subtype.mk
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
h : ∀ (s : Set (↑{x : G | 0 ≤ x} : Type u_2)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
hy' : 0 < y
z : G
hz : Membership.mem (γ := Set G) {x : G | 0 ≤ x} z
hz' :
  Membership.mem (γ := Set (↑{x : G | 0 ≤ x} : Type u_2))
    {x : (↑{x : G | 0 ≤ x} : Type u_2) |
      Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) 0 ⋯ < x}
    (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) z hz)
hz'' :
  ∀ (x : (↑{x : G | 0 ≤ x} : Type u_2)),
    Membership.mem (γ := Set (↑{x : G | 0 ≤ x} : Type u_2))
        {x : (↑{x : G | 0 ≤ x} : Type u_2) |
          Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) 0 ⋯ < x}
        x →
      ¬x < Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) z hz
w : G
hw : (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) 0 ⋯) : G) < w
hw' : w < (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) z hz) : G)
⊢ False

Tactic:
exact hz'' ⟨w, hw.le⟩ hw hw'

Premises used: LT.lt.le, Subtype.mk
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
h : ∀ (s : Set (↑{x : G | 0 ≤ x} : Type u_2)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : ∃ (x : G) (y : G), 0 < y ∧ ∀ (n : ℕ), n • y < x
neg : False
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)

Tactic:
exfalso
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
h : ∀ (s : Set (↑{x : G | 0 ≤ x} : Type u_2)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : ∃ (x : G) (y : G), 0 < y ∧ ∀ (n : ℕ), n • y < x
neg : ∀ (x y : G) (hy0 : 0 < y) (H : ∀ (n : ℕ), n • y < x), False
⊢ False

Tactic:
obtain ⟨x, y, hy0, H⟩ := H
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
h : ∀ (s : Set (↑{x : G | 0 ≤ x} : Type u_2)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
x y : G
hy0 : 0 < y
H : ∀ (n : ℕ), n • y < x
neg :
  ∀ (n : ℕ)
    (hz :
      ∀ (x_1 : (↑{x : G | 0 ≤ x} : Type u_2)),
        Membership.mem (γ := Set (↑{x : G | 0 ≤ x} : Type u_2))
            (range fun (n : ℕ) ↦
              Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) (x - n • y) ⋯)
            x_1 →
          ¬x_1 <
              (fun (n : ℕ) ↦
                  Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) (x - n • y) ⋯)
                n),
    False
⊢ False

Tactic:
obtain ⟨_, ⟨n, rfl⟩, hz⟩ :=
        h (Set.range (fun n : ℕ ↦ ⟨x - n • y, sub_nonneg.mpr (H _).le⟩)) (range_nonempty _)

Premises used: Iff.mpr, HSub.hSub, LT.lt.le, Subtype.mk, Set.range_nonempty, HSMul.hSMul, Set.range, sub_nonneg, rfl
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
h : ∀ (s : Set (↑{x : G | 0 ≤ x} : Type u_2)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
x y : G
hy0 : 0 < y
H : ∀ (n : ℕ), n • y < x
n : ℕ
hz :
  ∀ (x_1 : (↑{x : G | 0 ≤ x} : Type u_2)),
    Membership.mem (γ := Set (↑{x : G | 0 ≤ x} : Type u_2))
        (range fun (n : ℕ) ↦
          Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) (x - n • y) ⋯)
        x_1 →
      ¬x_1 <
          (fun (n : ℕ) ↦ Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) (x - n • y) ⋯) n
⊢ False

Tactic:
hz ⟨x - (n + 1) • y, sub_nonneg.mpr (H _).le⟩ ⟨_, rfl⟩ ?_

Premises used: Iff.mpr, HSub.hSub, LT.lt.le, Subtype.mk, HAdd.hAdd, Exists.intro, HSMul.hSMul, OfNat.ofNat, sub_nonneg, rfl
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
h : ∀ (s : Set (↑{x : G | 0 ≤ x} : Type u_2)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
x y : G
hy0 : 0 < y
H : ∀ (n : ℕ), n • y < x
n : ℕ
hz :
  ∀ (x_1 : (↑{x : G | 0 ≤ x} : Type u_2)),
    Membership.mem (γ := Set (↑{x : G | 0 ≤ x} : Type u_2))
        (range fun (n : ℕ) ↦
          Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) (x - n • y) ⋯)
        x_1 →
      ¬x_1 <
          (fun (n : ℕ) ↦ Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) (x - n • y) ⋯) n
neg :
  Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) (x - (n + 1) • y) ⋯ <
    (fun (n : ℕ) ↦ Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) (x - n • y) ⋯) n
⊢ False

Tactic:
refine hz ⟨x - (n + 1) • y, sub_nonneg.mpr (H _).le⟩ ⟨_, rfl⟩ ?_

Premises used: Iff.mpr, HSub.hSub, LT.lt.le, Subtype.mk, HAdd.hAdd, Exists.intro, HSMul.hSMul, OfNat.ofNat, sub_nonneg, rfl
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
h : ∀ (s : Set (↑{x : G | 0 ≤ x} : Type u_2)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
x y : G
hy0 : 0 < y
H : ∀ (n : ℕ), n • y < x
n : ℕ
hz :
  ∀ (x_1 : (↑{x : G | 0 ≤ x} : Type u_2)),
    Membership.mem (γ := Set (↑{x : G | 0 ≤ x} : Type u_2))
        (range fun (n : ℕ) ↦
          Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) (x - n • y) ⋯)
        x_1 →
      ¬x_1 <
          (fun (n : ℕ) ↦ Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) (x - n • y) ⋯) n
⊢ Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) (x - (n + 1) • y) ⋯ <
    (fun (n : ℕ) ↦ Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) (x - n • y) ⋯) n

Tactic:
simp [add_smul, hy0]

Premises used: add_smul
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
f : G ≃+o ℤ
mpr : ∀ (this : LocallyFiniteOrder G), WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2
⊢ WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2

Tactic:
have : LocallyFiniteOrder G := LocallyFiniteOrder.ofOrderIsoClass f
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
f : G ≃+o ℤ
this : LocallyFiniteOrder G
⊢ Membership.mem (γ := Set G) (lowerBounds {x : G | 0 ≤ x}) 0

Tactic:
simp [mem_lowerBounds]

Premises used: mem_lowerBounds
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Nontrivial G
g : G
f : G ≃+o ℤ
this : LocallyFiniteOrder G
⊢ WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2

Tactic:
exact BddBelow.wellFoundedOn_lt ⟨0, by simp [mem_lowerBounds]⟩

Premises used: BddBelow.wellFoundedOn_lt, Exists.intro, OfNat.ofNat
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid 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 ℤ)

Tactic:
rw [← wellFoundedOn_setOf_le_lt_iff_nonempty_discrete (g := -g)]

Premises used: LinearOrderedAddCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid 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, Iff.intro, Neg.neg
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid 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 : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid 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, neg_le]

Premises used: neg_le, Function.onFun
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid 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, neg_le]

Premises used: neg_le, Function.onFun
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid 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, neg_le]

Premises used: neg_le, Function.onFun
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid 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, neg_le]

Premises used: neg_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
e : G ≃o Additive G := OrderIso.refl G
this :
  (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
rw :
  (WellFoundedOn {x : Additive G | (e : (a : G) → Additive G) g ≤ x} fun (x1 x2 : Additive G) ↦ x1 < x2) ↔
    Nonempty.{max 1 (u_2 + 1)} (G ≃*o Multiplicative ℤ)
rw₁ : Nonempty.{u_2 + 1} (Additive G ≃+o ℤ) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃*o Multiplicative ℤ)
rw₂ rw₃ : Nonempty.{max 1 (u_2 + 1)} (G ≃*o Multiplicative ℤ) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃*o Multiplicative ℤ)
⊢ (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃*o Multiplicative ℤ)

Tactic:
rw [this, LinearOrderedAddCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete,
      OrderAddMonoidIso.toMultiplicativeRight.nonempty_congr]

Premises used: LinearOrderedAddCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete, OrderAddMonoidIso.toMultiplicativeRight, Equiv.nonempty_congr