awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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 ℤ)
⊢ (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
have rw : (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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 ℤ)
⊢ (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2
have refine_1 : ∀ (h : WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2),
  MapsTo (β := G) (fun (x : G) ↦ x + g) {x : G | 0 ≤ x} {x : G | g ≤ x}
Tactic: refine ⟨fun h ↦ (h.mapsTo (· + g) ?_).mono' ?_, fun h ↦ (h.mapsTo (· - g) ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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 ℤ)
refine_1 :
  ∀ (h : WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2),
    MapsTo (β := G) (fun (x : G) ↦ x + g) {x : G | 0 ≤ x} {x : G | g ≤ x}
⊢ (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2
have refine_2 : ∀ (h : WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) (a : G),
  Membership.mem (γ := Set G) {x : G | 0 ≤ x} a →
    ∀ (b : G),
      Membership.mem (γ := Set G) {x : G | 0 ≤ x} b →
        a < b → Function.onFun (fun (x1 x2 : G) ↦ x1 < x2) (fun (x : G) ↦ x + g) a b
Tactic: refine ⟨fun h ↦ (h.mapsTo (· + g) ?_).mono' ?_, fun h ↦ (h.mapsTo (· - g) ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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 ℤ)
refine_1 :
  ∀ (h : WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2),
    MapsTo (β := G) (fun (x : G) ↦ x + g) {x : G | 0 ≤ x} {x : G | g ≤ x}
refine_2 :
  ∀ (h : WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) (a : G),
    Membership.mem (γ := Set G) {x : G | 0 ≤ x} a →
      ∀ (b : G),
        Membership.mem (γ := Set G) {x : G | 0 ≤ x} b →
          a < b → Function.onFun (fun (x1 x2 : G) ↦ x1 < x2) (fun (x : G) ↦ x + g) a b
⊢ (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2
have refine_3 : ∀ (h : WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2),
  MapsTo (β := G) (fun (x : G) ↦ x - g) {x : G | g ≤ x} {x : G | 0 ≤ x}
Tactic: refine ⟨fun h ↦ (h.mapsTo (· + g) ?_).mono' ?_, fun h ↦ (h.mapsTo (· - g) ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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 ℤ)
refine_1 :
  ∀ (h : WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2),
    MapsTo (β := G) (fun (x : G) ↦ x + g) {x : G | 0 ≤ x} {x : G | g ≤ x}
refine_2 :
  ∀ (h : WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) (a : G),
    Membership.mem (γ := Set G) {x : G | 0 ≤ x} a →
      ∀ (b : G),
        Membership.mem (γ := Set G) {x : G | 0 ≤ x} b →
          a < b → Function.onFun (fun (x1 x2 : G) ↦ x1 < x2) (fun (x : G) ↦ x + g) a b
refine_3 :
  ∀ (h : WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2),
    MapsTo (β := G) (fun (x : G) ↦ x - g) {x : G | g ≤ x} {x : G | 0 ≤ x}
⊢ (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2
have refine_4 : ∀ (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: refine ⟨fun h ↦ (h.mapsTo (· + g) ?_).mono' ?_, fun h ↦ (h.mapsTo (· - g) ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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 | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2
⊢ MapsTo (β := G) (fun (x : G) ↦ x + g) {x : G | 0 ≤ x} {x : G | g ≤ x}
have refine_1 : ∀ ⦃x : G⦄,
  Membership.mem (γ := Set G) {x : G | 0 ≤ x} x → Membership.mem (γ := Set G) {x : G | g ≤ x} ((fun (x : G) ↦ x + g) x)
Tactic: try intro
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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
⊢ MapsTo (β := G) (fun (x : G) ↦ x - g) {x : G | g ≤ x} {x : G | 0 ≤ x}
have refine_3 : ∀ ⦃x : G⦄,
  Membership.mem (γ := Set G) {x : G | g ≤ x} x → Membership.mem (γ := Set G) {x : G | 0 ≤ x} ((fun (x : G) ↦ x - g) x)
Tactic: try intro
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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 | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
have suffices : (WellFoundedOn {x : G | 0 ≤ 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]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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 | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
have mp : (WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2) → Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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 ℤ)
⊢ (WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
have mpr : Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) → WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (hypothesis)
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
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
have h₁ : WellFounded fun (x1 x2 : (↑{x : G | 0 ≤ x} : Type u_2)) ↦ x1 < x2
Tactic: replace h : WellFounded (α := {x : G | 0 ≤ x}) (· < ·) := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (hypothesis)
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
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
have h₁ : ∀ (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
have pos : ∀ (H : ∀ (x : G) {y : G}, 0 < y → ∃ (n : ℕ), x ≤ n • y), Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
Tactic: by_cases! H : ∀ (x : G) {y}, 0 < y → ∃ n : ℕ, x ≤ n • y
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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 ℤ)
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
have neg : ∀ (H : ∃ (x : G) (y : G), 0 < y ∧ ∀ (n : ℕ), n • y < x), Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
Tactic: by_cases! H : ∀ (x : G) {y}, 0 < y → ∃ n : ℕ, x ≤ n • y
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (hypothesis)
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
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
have H₁ : Archimedean G
Tactic: replace H : Archimedean G := ⟨H⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
have pos : ¬DenselyOrdered G
Tactic: rw [LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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
⊢ False
have pos : ∀ (y : G) (hy : y ≠ 0), False
Tactic: obtain ⟨y, hy⟩ := exists_ne (0 : G)
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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
⊢ False
have pos : ∀ (this : ∀ (y : G) (hy : y ≠ 0) (hy' : 0 < y), False) (hy' : y ≤ 0), False
Tactic: wlog! hy' : 0 < y generalizing y
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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
⊢ False
have wlog! : ∀ (y : G) (hy : y ≠ 0) (hy' : 0 < y), False
Tactic: wlog! hy' : 0 < y generalizing y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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
have pos : -y ≠ 0
Tactic: refine this (-y) ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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
⊢ False
have pos₁ : 0 < -y
Tactic: refine this (-y) ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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
⊢ False
have 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 sorry < 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 sorry < x}
          x →
        ¬x < Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) z hz),
  False
Tactic: obtain ⟨⟨z, hz⟩, hz', hz''⟩ := h ({x | ⟨0, le_rfl⟩ < x}) ⟨⟨y, hy'.le⟩, hy'⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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
⊢ False
have obtain : ∀ (w : G) (hw : (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) 0 sorry) : G) < w)
  (hw' : w < (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) z hz) : G)), False
Tactic: obtain ⟨w, hw, hw'⟩ := exists_between hz'
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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
⊢ False
have neg : ∀ (x y : G) (hy0 : 0 < y) (H : ∀ (n : ℕ), n • y < x), False
Tactic: obtain ⟨x, y, hy0, H⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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
⊢ False
have 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) sorry)
          x_1 →
        ¬x_1 <
            (fun (n : ℕ) ↦ Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) (x - n • y) sorry)
              n),
  False
Tactic: obtain ⟨_, ⟨n, rfl⟩, hz⟩ :=
        h (Set.range (fun n : ℕ ↦ ⟨x - n • y, sub_nonneg.mpr (H _).le⟩)) (range_nonempty _)
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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
have neg : Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) (x - (n + 1) • y) sorry <
  (fun (n : ℕ) ↦ Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Set G) {x : G | 0 ≤ x} x) (x - n • y) sorry) n
Tactic: refine hz ⟨x - (n + 1) • y, sub_nonneg.mpr (H _).le⟩ ⟨_, rfl⟩ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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 ℤ
⊢ WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2
have mpr : ∀ (this : LocallyFiniteOrder G), WellFoundedOn {x : G | 0 ≤ x} fun (x1 x2 : G) ↦ x1 < x2
Tactic: have : LocallyFiniteOrder G := LocallyFiniteOrder.ofOrderIsoClass f
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ)
have rw : (WellFoundedOn {x : G | x ≤ g} 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 (g := -g)]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
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
have 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}
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 : 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}
⊢ (WellFoundedOn {x : G | x ≤ g} 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} 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 : 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
⊢ (WellFoundedOn {x : G | x ≤ g} 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} {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 : 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}
⊢ (WellFoundedOn {x : G | x ≤ g} 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} 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: 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 : 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
⊢ (WellFoundedOn {x : G | g ≤ x} fun (x1 x2 : G) ↦ x1 < x2) ↔ Nonempty.{max 1 (u_2 + 1)} (G ≃*o Multiplicative ℤ)
have 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 ℤ)
Tactic: rw [this, LinearOrderedAddCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete,
      OrderAddMonoidIso.toMultiplicativeRight.nonempty_congr]