awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b
this_1 : Eq (α := Subgroup G) (closure {b ^ n}) (closure {b})
this : Membership.mem (γ := Set G) {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b
⊢ b = |b ^ n|ₘ ∧ 1 < b
have this₁ : (∃ (n_1 : ℤ), (b ^ n) ^ n_1 = b) ∧ 1 < b
Tactic: simp only [mem_closure_singleton, mem_setOf_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b
this_1 : Eq (α := Subgroup G) (closure {b ^ n}) (closure {b})
this : (∃ (n_1 : ℤ), (b ^ n) ^ n_1 = b) ∧ 1 < b
⊢ b = |b ^ n|ₘ ∧ 1 < b
have mp : ∀ (m : ℤ) (hm : (b ^ n) ^ m = b), b = |b ^ n|ₘ ∧ 1 < b
Tactic: obtain ⟨m, hm⟩ := this.left
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b
this_1 : Eq (α := Subgroup G) (closure {b ^ n}) (closure {b})
this : (∃ (n_1 : ℤ), (b ^ n) ^ n_1 = b) ∧ 1 < b
m : ℤ
hm : (b ^ n) ^ m = b
⊢ m * n = 1
have rw : b ^ (m * n) = HPow.hPow (β := ℤ) b 1
Tactic: rw [← zpow_right_inj this.right, zpow_mul', hm, zpow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b
this_1 : Eq (α := Subgroup G) (closure {b ^ n}) (closure {b})
this : (∃ (n_1 : ℤ), (b ^ n) ^ n_1 = b) ∧ 1 < b
m : ℤ
hm : (b ^ n) ^ m = b
rw : b ^ (m * n) = HPow.hPow (β := ℤ) b 1
⊢ m * n = 1
have rw₁ : (b ^ n) ^ m = HPow.hPow (β := ℤ) b 1
Tactic: rw [← zpow_right_inj this.right, zpow_mul', hm, zpow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b
this_1 : Eq (α := Subgroup G) (closure {b ^ n}) (closure {b})
this : (∃ (n_1 : ℤ), (b ^ n) ^ n_1 = b) ∧ 1 < b
m : ℤ
hm : (b ^ n) ^ m = b
rw : b ^ (m * n) = HPow.hPow (β := ℤ) b 1
rw₁ : (b ^ n) ^ m = HPow.hPow (β := ℤ) b 1
⊢ m * n = 1
have rw₂ : b = HPow.hPow (β := ℤ) b 1
Tactic: rw [← zpow_right_inj this.right, zpow_mul', hm, zpow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b
this_1 : Eq (α := Subgroup G) (closure {b ^ n}) (closure {b})
this : (∃ (n_1 : ℤ), (b ^ n) ^ n_1 = b) ∧ 1 < b
m : ℤ
hm : (b ^ n) ^ m = b
rw : b ^ (m * n) = HPow.hPow (β := ℤ) b 1
rw₁ : (b ^ n) ^ m = HPow.hPow (β := ℤ) b 1
rw₂ : b = HPow.hPow (β := ℤ) b 1
⊢ m * n = 1
have rw₃ : b = b
Tactic: rw [← zpow_right_inj this.right, zpow_mul', hm, zpow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b
this_1 : Eq (α := Subgroup G) (closure {b ^ n}) (closure {b})
this : (∃ (n_1 : ℤ), (b ^ n) ^ n_1 = b) ∧ 1 < b
m : ℤ
hm : (b ^ n) ^ m = b
⊢ b = |b ^ n|ₘ ∧ 1 < b
have key : m * n = 1
Tactic: have key : m * n = 1 := by
      rw [← zpow_right_inj this.right, zpow_mul', hm, zpow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b
this_1 : Eq (α := Subgroup G) (closure {b ^ n}) (closure {b})
this : (∃ (n_1 : ℤ), (b ^ n) ^ n_1 = b) ∧ 1 < b
m : ℤ
hm : (b ^ n) ^ m = b
key : m * n = 1
⊢ b = |b ^ n|ₘ ∧ 1 < b
have key₁ : m = 1 ∧ n = 1 ∨ m = -1 ∧ n = -1
Tactic: rw [Int.mul_eq_one_iff_eq_one_or_neg_one] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b
this_1 : Eq (α := Subgroup G) (closure {b ^ n}) (closure {b})
this : (∃ (n_1 : ℤ), (b ^ n) ^ n_1 = b) ∧ 1 < b
m : ℤ
hm : (b ^ n) ^ m = b
key : m = 1 ∧ n = 1 ∨ m = -1 ∧ n = -1
⊢ b = |b ^ n|ₘ ∧ 1 < b
have mp : |b ^ n|ₘ = b ∧ 1 < b
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b
this_1 : Eq (α := Subgroup G) (closure {b ^ n}) (closure {b})
this : (∃ (n_1 : ℤ), (b ^ n) ^ n_1 = b) ∧ 1 < b
m : ℤ
hm : (b ^ n) ^ m = b
key : m = 1 ∧ n = 1 ∨ m = -1 ∧ n = -1
⊢ |b ^ n|ₘ = b ∧ 1 < b
have mp : ∀ (h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {HPow.hPow (β := ℤ) b 1}) y ∧ 1 < y} b)
  (this : Eq (α := Subgroup G) (closure {HPow.hPow (β := ℤ) b 1}) (closure {b}))
  (this : (∃ (n : ℤ), HPow.hPow (β := ℤ) b 1 ^ n = b) ∧ 1 < b) (hm : HPow.hPow (β := ℤ) (HPow.hPow (β := ℤ) b 1) 1 = b),
  |HPow.hPow (β := ℤ) b 1|ₘ = b ∧ 1 < b
Tactic: rcases key with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
Cleared hypotheses: n, h, this_1, this, m, hm, key
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b
this_1 : Eq (α := Subgroup G) (closure {b ^ n}) (closure {b})
this : (∃ (n_1 : ℤ), (b ^ n) ^ n_1 = b) ∧ 1 < b
m : ℤ
hm : (b ^ n) ^ m = b
key : m = 1 ∧ n = 1 ∨ m = -1 ∧ n = -1
mp :
  ∀ (h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {HPow.hPow (β := ℤ) b 1}) y ∧ 1 < y} b)
    (this : Eq (α := Subgroup G) (closure {HPow.hPow (β := ℤ) b 1}) (closure {b}))
    (this : (∃ (n : ℤ), HPow.hPow (β := ℤ) b 1 ^ n = b) ∧ 1 < b)
    (hm : HPow.hPow (β := ℤ) (HPow.hPow (β := ℤ) b 1) 1 = b), |HPow.hPow (β := ℤ) b 1|ₘ = b ∧ 1 < b
⊢ |b ^ n|ₘ = b ∧ 1 < b
have mp₁ : ∀ (h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {HPow.hPow (β := ℤ) b (-1)}) y ∧ 1 < y} b)
  (this : Eq (α := Subgroup G) (closure {HPow.hPow (β := ℤ) b (-1)}) (closure {b}))
  (this : (∃ (n : ℤ), HPow.hPow (β := ℤ) b (-1) ^ n = b) ∧ 1 < b)
  (hm : HPow.hPow (β := ℤ) (HPow.hPow (β := ℤ) b (-1)) (-1) = b), |HPow.hPow (β := ℤ) b (-1)|ₘ = b ∧ 1 < b
Tactic: rcases key with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
Cleared hypotheses: n, h, this_1, this, m, hm, key
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a b : G
h : b = |a|ₘ ∧ 1 < b
⊢ IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b
have mpr : ∀
  (this :
    ∀ {a : G} (h : b = |a|ₘ ∧ 1 < b) (ha : 1 ≤ a),
      IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b)
  (ha : ¬1 ≤ a), IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b
Tactic: wlog ha : 1 ≤ a generalizing a
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a b : G
h : b = |a|ₘ ∧ 1 < b
mpr :
  ∀
    (this :
      ∀ {a : G} (h : b = |a|ₘ ∧ 1 < b) (ha : 1 ≤ a),
        IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b)
    (ha : ¬1 ≤ a), IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b
⊢ IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b
have wlog : ∀ {a : G} (h : b = |a|ₘ ∧ 1 < b) (ha : 1 ≤ a),
  IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b
Tactic: wlog ha : 1 ≤ a generalizing a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a b : G
h : b = |a|ₘ ∧ 1 < b
this :
  ∀ {a : G} (h : b = |a|ₘ ∧ 1 < b) (ha : 1 ≤ a),
    IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b
ha : ¬1 ≤ a
⊢ IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b
have h₁ : ∀ (x : G), Membership.mem (γ := Subgroup G) (closure {a}) x ↔ Membership.mem (γ := Subgroup G) (closure {a⁻¹}) x
Tactic: convert! @this (a⁻¹) ?_ (by simpa using le_of_not_ge ha) using 4
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a b : G
h : b = |a|ₘ ∧ 1 < b
this :
  ∀ {a : G} (h : b = |a|ₘ ∧ 1 < b) (ha : 1 ≤ a),
    IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b
ha : ¬1 ≤ a
h₁ : ∀ (x : G), Membership.mem (γ := Subgroup G) (closure {a}) x ↔ Membership.mem (γ := Subgroup G) (closure {a⁻¹}) x
⊢ IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b
have mpr : b = |a⁻¹|ₘ ∧ 1 < b
Tactic: convert! @this (a⁻¹) ?_ (by simpa using le_of_not_ge ha) using 4
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b a : G
h : b = |a|ₘ ∧ 1 < b
ha : 1 ≤ a
⊢ IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b
have h₁ : b = a ∧ 1 < b
Tactic: rw [mabs, sup_eq_left.mpr ((inv_le_one'.mpr ha).trans ha)] at h
Cleared hypotheses: h, ha
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b a : G
h : b = a ∧ 1 < b
ha : 1 ≤ a
⊢ IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b
have rcases : ∀ (h : 1 < b) (ha : 1 ≤ b), IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b}) y ∧ 1 < y} b
Tactic: rcases h with ⟨rfl, h⟩
Cleared hypotheses: a, h, ha
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
⊢ IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b}) y ∧ 1 < y} b
have refine_1 : Membership.mem (γ := Set G) {y : G | Membership.mem (γ := Subgroup G) (closure {b}) y ∧ 1 < y} b
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
refine_1 : Membership.mem (γ := Set G) {y : G | Membership.mem (γ := Subgroup G) (closure {b}) y ∧ 1 < y} b
⊢ IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b}) y ∧ 1 < y} b
have refine_2 : Membership.mem (γ := Set G) (lowerBounds {y : G | Membership.mem (γ := Subgroup G) (closure {b}) y ∧ 1 < y}) b
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
x : G
⊢ Membership.mem (γ := Set G) {y : G | Membership.mem (γ := Subgroup G) (closure {b}) y ∧ 1 < y} x → b ≤ x
have refine_2 : ∀ (x_1 : ℤ) (h : b ^ x_1 = x), 1 < x → b ≤ x
Tactic: simp only [mem_closure_singleton, mem_setOf_eq, and_imp, forall_exists_index]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
k : ℤ
hk : 1 < b ^ k
⊢ b ≤ b ^ k
have refine_2 : 0 < k
Tactic: rw [← zpow_one b, ← zpow_mul, one_mul, zpow_le_zpow_iff_right h, ← zero_add 1,
          ← Int.lt_iff_add_one_le]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
k : ℤ
hk : 1 < b ^ k
⊢ 0 < k
have refine_2 : ∀ (hk : k ≤ 0), b ^ k ≤ 1
Tactic: contrapose! hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
k : ℤ
hk : k ≤ 0
⊢ b ^ k ≤ 1
have refine_2 : 1 ≤ b ^ (-k)
Tactic: rw [← Left.one_le_inv_iff, ← zpow_neg]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (hypothesis)
Goal:
G_1 : Type u_1
inst : CommGroup G_1
inst_1 : LinearOrder G_1
inst_2 : IsOrderedMonoid G_1
inst_3 : MulArchimedean G_1
G : Type u_2
inst_4 : AddCommGroup G
inst_5 : LinearOrder G
inst_6 : IsOrderedAddMonoid G
inst_7 : Archimedean G
x : G
h : IsLeast {y : G | 0 < y} x
⊢ G ≃+o ℤ
have this : IsLeast {y : G | Membership.mem (γ := AddSubgroup G) ⊤ y ∧ 0 < y} x
Tactic: have : IsLeast {y : G | y ∈ (⊤ : AddSubgroup G) ∧ 0 < y} x := by simpa using h
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (hypothesis)
Goal:
G_1 : Type u_1
inst : CommGroup G_1
inst_1 : LinearOrder G_1
inst_2 : IsOrderedMonoid G_1
inst_3 : MulArchimedean G_1
G : Type u_2
inst_4 : AddCommGroup G
inst_5 : LinearOrder G
inst_6 : IsOrderedAddMonoid G
inst_7 : Archimedean G
x : G
h : IsLeast {y : G | 0 < y} x
this : IsLeast {y : G | Membership.mem (γ := AddSubgroup G) ⊤ y ∧ 0 < y} x
⊢ G ≃+o ℤ
have this₁ : Eq (α := AddSubgroup G) ⊤ (AddSubgroup.closure {x})
Tactic: replace this := AddSubgroup.cyclic_of_min this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
x : G
h : IsLeast {y : G | 1 < y} x
⊢ G ≃*o Multiplicative ℤ
have this : IsLeast (α := Additive G) ({y : Additive G | 0 < y} : Set (Additive G))
  ((Additive.ofMul : (a : G) → Additive G) x : Additive G)
Tactic: have : IsLeast {y : Additive G | 0 < y} (.ofMul x) := 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 : Archimedean G
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) ∨ DenselyOrdered G
have pos : ∀ (H : ∃ (x : G), IsLeast {y : G | 0 < y} x), Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) ∨ DenselyOrdered G
Tactic: by_cases! H : ∃ x, IsLeast {y : G | 0 < y} x
-- 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 : Archimedean G
pos : ∀ (H : ∃ (x : G), IsLeast {y : G | 0 < y} x), Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) ∨ DenselyOrdered G
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) ∨ DenselyOrdered G
have neg : ∀ (H : ∀ (x : G), ¬IsLeast {y : G | 0 < y} x), Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) ∨ DenselyOrdered G
Tactic: by_cases! H : ∃ x, IsLeast {y : G | 0 < y} x
-- 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 : Archimedean G
H : ∃ (x : G), IsLeast {y : G | 0 < y} x
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) ∨ DenselyOrdered G
have pos : ∀ (x : G) (hx : IsLeast {y : G | 0 < y} x), Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) ∨ DenselyOrdered G
Tactic: obtain ⟨x, hx⟩ := 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 : Archimedean G
H : ∀ (x : G), ¬IsLeast {y : G | 0 < y} x
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) ∨ DenselyOrdered G
have neg : ∀ (a₁ a₂ : G), a₁ < a₂ → ∃ (a : G), a₁ < a ∧ a < a₂
Tactic: refine Or.inr ⟨?_⟩
-- 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 : Archimedean G
H : ∀ (x : G), ¬IsLeast {y : G | 0 < y} x
x y : G
hxy : x < y
⊢ ∃ (a : G), x < a ∧ a < y
have H₁ : ¬IsLeast {y : G | 0 < y} (y - x)
Tactic: specialize H (y - x)
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 : Archimedean G
x y : G
hxy : x < y
H : ¬IsLeast {y : G | 0 < y} (y - x)
⊢ ∃ (z : G), 0 < z ∧ z < y - x
have contrapose! : ∀ (H : ∀ (z : G) (_ : 0 < z), y - x ≤ z), IsLeast {y : G | 0 < y} (y - x)
Tactic: contrapose! 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 : Archimedean G
x y : G
hxy : x < y
H : ¬IsLeast {y : G | 0 < y} (y - x)
⊢ ∃ (a : G), x < a ∧ a < y
have neg : ∀ (z : G) (hz : 0 < z ∧ z < y - x), ∃ (a : G), x < a ∧ a < y
Tactic: obtain ⟨z, hz⟩ : ∃ z : G, 0 < z ∧ z < y - x := by
      contrapose! H
      refine ⟨by simp [hxy], fun _ ↦ 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 : Archimedean G
x y : G
hxy : x < y
H : ¬IsLeast {y : G | 0 < y} (y - x)
z : G
hz : 0 < z ∧ z < y - x
⊢ ∃ (a : G), x < a ∧ a < y
have neg : x < x + z
Tactic: refine ⟨x + z, ?_, ?_⟩
-- 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 : Archimedean G
x y : G
hxy : x < y
H : ¬IsLeast {y : G | 0 < y} (y - x)
z : G
hz : 0 < z ∧ z < y - x
neg : x < x + z
⊢ ∃ (a : G), x < a ∧ a < y
have neg₁ : x + z < y
Tactic: refine ⟨x + z, ?_, ?_⟩
-- 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 : Archimedean G
this : ∀ (x : G ≃+o ℤ), ¬DenselyOrdered G
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) ↔ ¬DenselyOrdered G
have inl : ∀ (h : G ≃+o ℤ), Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) ↔ ¬DenselyOrdered G
Tactic: rcases LinearOrderedAddCommGroup.discrete_or_denselyOrdered G with ⟨⟨h⟩⟩ | 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 : Archimedean G
this : ∀ (x : G ≃+o ℤ), ¬DenselyOrdered G
inl : ∀ (h : G ≃+o ℤ), Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) ↔ ¬DenselyOrdered G
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) ↔ ¬DenselyOrdered G
have inr : ∀ (h : DenselyOrdered G), Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) ↔ ¬DenselyOrdered G
Tactic: rcases LinearOrderedAddCommGroup.discrete_or_denselyOrdered G with ⟨⟨h⟩⟩ | 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 : Archimedean G
this : ∀ (x : G ≃+o ℤ), ¬DenselyOrdered G
h : DenselyOrdered G
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) ↔ ¬DenselyOrdered G
have inr : IsEmpty.{u_2 + 1} (G ≃+o ℤ)
Tactic: simp only [h, not_true_eq_false, iff_false, not_nonempty_iff]
-- 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 : Archimedean G
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) ↔ ¬DenselyOrdered G
have suffices : ∀ (x : G ≃+o ℤ), ¬DenselyOrdered G
Tactic: suffices ∀ (_ : G ≃+o ℤ), ¬ DenselyOrdered G by
    rcases LinearOrderedAddCommGroup.discrete_or_denselyOrdered G with ⟨⟨h⟩⟩ | h
    · simpa [this h] using ⟨h⟩
    · simp only [h, not_true_eq_false, iff_false, not_nonempty_iff]
      exact ⟨fun H ↦ (this H) 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 : Archimedean G
e : G ≃+o ℤ
H : DenselyOrdered G
⊢ False
have H₁ : DenselyOrdered ℤ
Tactic: rw [denselyOrdered_iff_of_orderIsoClass e] 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 : Archimedean G
e : G ≃+o ℤ
H : DenselyOrdered ℤ
⊢ False
have obtain : ∀ (w : ℤ), 0 < w ∧ w < 1 → False
Tactic: obtain ⟨_, _⟩ := exists_between (one_pos (α := ℤ))
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
A : Type u_2
inst : AddCommGroup A
inst_1 : LinearOrder A
inst_2 : IsOrderedAddMonoid A
inst_3 : Archimedean A
inst_4 : Nontrivial A
⊢ IsAddCyclic A ↔ ¬DenselyOrdered A
have rw : IsAddCyclic A ↔ Nonempty.{u_2 + 1} (A ≃+o ℤ)
Tactic: rw [← discrete_iff_not_denselyOrdered, isAddCyclic_iff_nonempty_equiv_int]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
A : Type u_2
inst : AddCommGroup A
inst_1 : LinearOrder A
inst_2 : IsOrderedAddMonoid A
inst_3 : Archimedean A
inst_4 : Nontrivial A
rw : IsAddCyclic A ↔ Nonempty.{u_2 + 1} (A ≃+o ℤ)
⊢ IsAddCyclic A ↔ ¬DenselyOrdered A
have rw₁ : Nonempty.{u_2 + 1} (A ≃+o ℤ) ↔ Nonempty.{u_2 + 1} (A ≃+o ℤ)
Tactic: rw [← discrete_iff_not_denselyOrdered, isAddCyclic_iff_nonempty_equiv_int]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
⊢ Nonempty.{max 1 (u_1 + 1)} (G ≃*o Multiplicative ℤ) ∨ DenselyOrdered G
have rw : Nonempty.{max 1 (u_1 + 1)} (Additive G ≃+o ℤ) ∨ DenselyOrdered G
Tactic: rw [← OrderAddMonoidIso.toMultiplicativeRight.nonempty_congr]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
e : G ≃o Additive G := OrderIso.refl G
⊢ Nonempty.{max 1 (u_1 + 1)} (G ≃*o Multiplicative ℤ) ↔ ¬DenselyOrdered G
have rw : Nonempty.{max 1 (u_1 + 1)} (Additive G ≃+o ℤ) ↔ ¬DenselyOrdered G
Tactic: rw [← OrderAddMonoidIso.toMultiplicativeRight.nonempty_congr,
    LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered,
    denselyOrdered_iff_of_orderIsoClass e]
-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
e : G ≃o Additive G := OrderIso.refl G
rw : Nonempty.{max 1 (u_1 + 1)} (Additive G ≃+o ℤ) ↔ ¬DenselyOrdered G
⊢ Nonempty.{max 1 (u_1 + 1)} (G ≃*o Multiplicative ℤ) ↔ ¬DenselyOrdered G
have rw₁ : ¬DenselyOrdered.{u_1} (Additive G) ↔ ¬DenselyOrdered G
Tactic: rw [← OrderAddMonoidIso.toMultiplicativeRight.nonempty_congr,
    LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered,
    denselyOrdered_iff_of_orderIsoClass e]