awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
wlog :
  ∀ {a : G} (h : b = |a|ₘ ∧ 1 < 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

Tactic:
wlog ha : 1 ≤ a generalizing a
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
⊢ 1 ≤ a⁻¹

Tactic:
simpa using le_of_not_ge ha

Premises used: le_of_not_ge
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
mpr : b = |a⁻¹|ₘ ∧ 1 < b
⊢ IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b

Tactic:
convert! @this (a⁻¹) ?_ (by simpa using le_of_not_ge ha) using 4
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
x : G
⊢ Membership.mem (γ := Subgroup G) (closure {a}) x ↔ Membership.mem (γ := Subgroup G) (closure {a⁻¹}) x

Tactic:
simp
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
mpr mpr₁ mpr₂ mpr₃ : b = |a|ₘ ∧ 1 < b
⊢ b = |a⁻¹|ₘ ∧ 1 < b

Tactic:
rwa [mabs_inv]

Premises used: mabs_inv
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
⊢ b = a ∧ 1 < b

Tactic:
rw [mabs, sup_eq_left.mpr ((inv_le_one'.mpr ha).trans ha)] at h

Premises used: Iff.mpr, inv_le_one', sup_eq_left, LE.le.trans, mabs
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
h₁ : b = a ∧ 1 < b
⊢ 1 ≤ a

Tactic:
rw [mabs, sup_eq_left.mpr ((inv_le_one'.mpr ha).trans ha)] at h

Premises used: Iff.mpr, inv_le_one', sup_eq_left, LE.le.trans, mabs
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
rcases : ∀ (h : 1 < b) (ha : 1 ≤ b), IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b}) y ∧ 1 < y} b
⊢ IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b

Tactic:
rcases h with ⟨rfl, h⟩

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

Tactic:
⟨?_, ?_⟩

Premises used: IsLeast, And.intro
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
refine_2 :
  Membership.mem (γ := Set G) (lowerBounds {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

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
⊢ Membership.mem (γ := Set G) {y : G | Membership.mem (γ := Subgroup G) (closure {b}) y ∧ 1 < y} b

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
refine_2 : ∀ (x_1 : ℤ) (h : b ^ x_1 = x), 1 < x → b ≤ x
⊢ Membership.mem (γ := Set G) {y : G | Membership.mem (γ := Subgroup G) (closure {b}) y ∧ 1 < y} x → b ≤ x

Tactic:
simp only [mem_closure_singleton, mem_setOf_eq, and_imp, forall_exists_index]

Premises used: and_imp, forall_exists_index, Subgroup.mem_closure_singleton, Set.mem_setOf_eq
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
refine_2 : 0 < k
⊢ b ≤ b ^ 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]

Premises used: Int.lt_iff_add_one_le, zpow_mul, zpow_one, zero_add, zpow_le_zpow_iff_right, OfNat.ofNat, one_mul
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
refine_2 : ∀ (hk : k ≤ 0), b ^ k ≤ 1
⊢ 0 < k

Tactic:
contrapose! hk
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
refine_2 : 1 ≤ b ^ (-k)
⊢ b ^ k ≤ 1

Tactic:
rw [← Left.one_le_inv_iff, ← zpow_neg]

Premises used: zpow_neg, Left.one_le_inv_iff
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
⊢ 0 ≤ -k

Tactic:
simp [hk]
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
⊢ 1 ≤ b ^ (-k)

Tactic:
exact one_le_zpow ha (by simp [hk])

Premises used: one_le_zpow
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
⊢ IsLeast {y : G | Membership.mem (γ := AddSubgroup G) ⊤ y ∧ 0 < y} x

Tactic:
simpa using h
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
⊢ 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
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
⊢ Eq (α := AddSubgroup G) ⊤ (AddSubgroup.closure {x})

Tactic:
replace this := AddSubgroup.cyclic_of_min this
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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 : Eq (α := AddSubgroup G) ⊤ (AddSubgroup.closure {x})
e : G ≃+o ↥⊤ := { toAddEquiv := AddEquiv.symm AddSubsemigroup.topEquiv, map_le_map_iff' := ⋯ }
⊢ Eq (α := AddSubsemigroup G) (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid ⊤))
    (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (AddSubgroup.closure {x})))

Tactic:
simp [this]
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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 : Eq (α := AddSubgroup G) ⊤ (AddSubgroup.closure {x})
e : G ≃+o ↥⊤ := { toAddEquiv := AddEquiv.symm AddSubsemigroup.topEquiv, map_le_map_iff' := ⋯ }
e' : ↥⊤ ≃+o ↥(AddSubgroup.closure {x}) := { toAddEquiv := AddEquiv.subsemigroupCongr ⋯, map_le_map_iff' := ⋯ }
g : ↥⊤ ≃+o ℤ := { toAddEquiv := AddSubsemigroup.topEquiv, map_le_map_iff' := ⋯ }
⊢ Eq (α := AddSubsemigroup ℤ) (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (AddSubgroup.closure {1})))
    (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid ⊤))

Tactic:
simp
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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 : Eq (α := AddSubgroup G) ⊤ (AddSubgroup.closure {x})
e : G ≃+o ↥⊤ := { toAddEquiv := AddEquiv.symm AddSubsemigroup.topEquiv, map_le_map_iff' := ⋯ }
e' : ↥⊤ ≃+o ↥(AddSubgroup.closure {x}) := { toAddEquiv := AddEquiv.subsemigroupCongr ⋯, map_le_map_iff' := ⋯ }
g : ↥⊤ ≃+o ℤ := { toAddEquiv := AddSubsemigroup.topEquiv, map_le_map_iff' := ⋯ }
g' : ↥(AddSubgroup.closure {1}) ≃+o ↥⊤ :=
  { toAddEquiv := AddEquiv.subsemigroupCongr int_orderAddMonoidIso_of_isLeast_pos._proof_2, map_le_map_iff' := ⋯ }
⊢ x = 0 ↔ Eq (α := ℤ) 1 0

Tactic:
simp [h.left.ne']

Premises used: LT.lt.ne', And.left
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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 : Eq (α := AddSubgroup G) ⊤ (AddSubgroup.closure {x})
e : G ≃+o ↥⊤ := { toAddEquiv := AddEquiv.symm AddSubsemigroup.topEquiv, map_le_map_iff' := ⋯ }
e' : ↥⊤ ≃+o ↥(AddSubgroup.closure {x}) := { toAddEquiv := AddEquiv.subsemigroupCongr ⋯, map_le_map_iff' := ⋯ }
g : ↥⊤ ≃+o ℤ := { toAddEquiv := AddSubsemigroup.topEquiv, map_le_map_iff' := ⋯ }
g' : ↥(AddSubgroup.closure {1}) ≃+o ↥⊤ :=
  { toAddEquiv := AddEquiv.subsemigroupCongr int_orderAddMonoidIso_of_isLeast_pos._proof_2, map_le_map_iff' := ⋯ }
f : ↥(AddSubgroup.closure {x}) ≃+o ↥(AddSubgroup.closure {1}) := closure_equiv_closure x 1 ⋯
⊢ G ≃+o ℤ

Tactic:
exact ((((e.trans e').trans f).trans g').trans g : G ≃+o ℤ)

Premises used: OrderAddMonoidIso.trans
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
⊢ 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
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
this :
  IsLeast (α := Additive G) ({y : Additive G | 0 < y} : Set (Additive G))
    ((Additive.ofMul : (a : G) → Additive G) x : Additive G)
f' : Additive G ≃+o ℤ := LinearOrderedAddCommGroup.int_orderAddMonoidIso_of_isLeast_pos this
⊢ G ≃*o Multiplicative ℤ

Tactic:
exact f'.toMultiplicativeRight

Premises used: OrderAddMonoidIso.toMultiplicativeRight, DFunLike.coe
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
⊢ Archimedean G

Tactic:
.comap (LocallyFiniteOrder.addMonoidHom G) LocallyFiniteOrder.orderAddMonoidHom_strictMono

Premises used: LocallyFiniteOrder.orderAddMonoidHom_strictMono, Archimedean.comap, LocallyFiniteOrder.addMonoidHom
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : LocallyFiniteOrder G
⊢ MulArchimedean G

Tactic:
.comap (LocallyFiniteOrder.orderMonoidHom G).toMonoidHom
    LocallyFiniteOrder.orderMonoidHom_strictMono

Premises used: MulArchimedean.comap, LocallyFiniteOrder.orderMonoidHom_strictMono, LocallyFiniteOrder.orderMonoidHom, OrderMonoidHom.toMonoidHom
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
neg : ∀ (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

Tactic:
by_cases! H : ∃ x, IsLeast {y : G | 0 < y} x
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
pos : ∀ (x : G) (hx : 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

Tactic:
obtain ⟨x, hx⟩ := H
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Archimedean G
x : G
hx : IsLeast {y : G | 0 < y} x
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) ∨ DenselyOrdered G

Tactic:
Or.inl ⟨(int_orderAddMonoidIso_of_isLeast_pos hx)⟩

Premises used: LinearOrderedAddCommGroup.int_orderAddMonoidIso_of_isLeast_pos, Nonempty.intro, Or.inl
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Archimedean G
x : G
hx : IsLeast {y : G | 0 < y} x
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) ∨ DenselyOrdered G

Tactic:
exact Or.inl ⟨(int_orderAddMonoidIso_of_isLeast_pos hx)⟩

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

Tactic:
Or.inr ⟨?_⟩

Premises used: DenselyOrdered.mk, Or.inr
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
neg : ∀ (a₁ a₂ : G), a₁ < a₂ → ∃ (a : G), a₁ < a ∧ a < a₂
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) ∨ DenselyOrdered G

Tactic:
refine Or.inr ⟨?_⟩

Premises used: Or.inr
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
⊢ ¬IsLeast {y : G | 0 < y} (y - x)

Tactic:
specialize H (y - x)

Premises used: HSub.hSub
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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)
contrapose! : ∀ (H : ∀ (z : G) (_ : 0 < z), y - x ≤ z), IsLeast {y : G | 0 < y} (y - x)
⊢ ∃ (z : G), 0 < z ∧ z < y - x

Tactic:
contrapose! H
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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 : ∀ (z : G) (_ : 0 < z), y - x ≤ z
⊢ Membership.mem (γ := Set G) {y : G | 0 < y} (y - x)

Tactic:
simp [hxy]
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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 : ∀ (z : G) (_ : 0 < z), y - x ≤ z
⊢ IsLeast {y : G | 0 < y} (y - x)

Tactic:
refine ⟨by simp [hxy], fun _ ↦ H _⟩
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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)
neg : ∀ (z : G) (hz : 0 < z ∧ z < y - x), ∃ (a : G), x < a ∧ a < y
⊢ ∃ (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 _⟩
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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

Tactic:
⟨x + z, ?_, ?_⟩

Premises used: HAdd.hAdd, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
neg₁ : x + z < y
⊢ ∃ (a : G), x < a ∧ a < y

Tactic:
refine ⟨x + z, ?_, ?_⟩
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
⊢ x < x + z

Tactic:
simp [hz.left]

Premises used: And.left
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
⊢ x + z < y

Tactic:
simpa [lt_sub_iff_add_lt'] using hz.right

Premises used: lt_sub_iff_add_lt', And.right
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
inr : ∀ (h : DenselyOrdered G), Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) ↔ ¬DenselyOrdered G
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) ↔ ¬DenselyOrdered G

Tactic:
rcases LinearOrderedAddCommGroup.discrete_or_denselyOrdered G with ⟨⟨h⟩⟩ | h

Premises used: LinearOrderedAddCommGroup.discrete_or_denselyOrdered
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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 : G ≃+o ℤ
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) ↔ ¬DenselyOrdered G

Tactic:
simpa [this h] using ⟨h⟩
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
inr : IsEmpty.{u_2 + 1} (G ≃+o ℤ)
⊢ Nonempty.{max 1 (u_2 + 1)} (G ≃+o ℤ) ↔ ¬DenselyOrdered G

Tactic:
simp only [h, not_true_eq_false, iff_false, not_nonempty_iff]

Premises used: iff_false, not_true_eq_false, not_nonempty_iff
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
⊢ IsEmpty.{u_2 + 1} (G ≃+o ℤ)

Tactic:
⟨fun H ↦ (this H) h⟩

Premises used: IsEmpty.mk
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
⊢ IsEmpty.{u_2 + 1} (G ≃+o ℤ)

Tactic:
exact ⟨fun H ↦ (this H) h⟩
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : Archimedean G
suffices : ∀ (x : G ≃+o ℤ), ¬DenselyOrdered G
⊢ Nonempty.{max 1 (u_2 + 1)} (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⟩
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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
⊢ DenselyOrdered ℤ

Tactic:
rw [denselyOrdered_iff_of_orderIsoClass e] at H

Premises used: denselyOrdered_iff_of_orderIsoClass
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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 ℤ
obtain : ∀ (w : ℤ), 0 < w ∧ w < 1 → False
⊢ False

Tactic:
obtain ⟨_, _⟩ := exists_between (one_pos (α := ℤ))

Premises used: exists_between, one_pos
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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 ℤ
w : ℤ
h : 0 < w ∧ w < 1
⊢ False

Tactic:
lia
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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 ℤ)
rw₁ rw₂ : Nonempty.{u_2 + 1} (A ≃+o ℤ) ↔ Nonempty.{u_2 + 1} (A ≃+o ℤ)
⊢ IsAddCyclic A ↔ ¬DenselyOrdered A

Tactic:
rw [← discrete_iff_not_denselyOrdered, isAddCyclic_iff_nonempty_equiv_int]

Premises used: LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered, LinearOrderedAddCommGroup.isAddCyclic_iff_nonempty_equiv_int
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
rw : Nonempty.{max 1 (u_1 + 1)} (Additive G ≃+o ℤ) ∨ DenselyOrdered G
⊢ Nonempty.{max 1 (u_1 + 1)} (G ≃*o Multiplicative ℤ) ∨ DenselyOrdered G

Tactic:
rw [← OrderAddMonoidIso.toMultiplicativeRight.nonempty_congr]

Premises used: OrderAddMonoidIso.toMultiplicativeRight, Equiv.nonempty_congr
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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)} (Additive G ≃+o ℤ) ∨ DenselyOrdered G

Tactic:
LinearOrderedAddCommGroup.discrete_or_denselyOrdered (Additive G)

Premises used: Additive, LinearOrderedAddCommGroup.discrete_or_denselyOrdered