awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬((↑H : Set G) ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ (↑H : Set G)
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
by_contra : ∀ (hxmin : ¬∃ (b : G), IsLeast {g : G | g ∈ H ∧ 1 < g} b), False
⊢ ∃ (b : G), IsLeast {g : G | g ∈ H ∧ 1 < g} b

Tactic:
by_contra hxmin
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬((↑H : Set G) ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ (↑H : Set G)
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ¬∃ (b : G), IsLeast {g : G | g ∈ H ∧ 1 < g} b
⊢ ∀ (x : G), x ∈ H ∧ 1 < x → ∃ (x_1 : G) (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x

Tactic:
simp only [IsLeast, not_and, mem_setOf_eq, mem_lowerBounds, not_exists, not_forall,
    not_le] at hxmin

Premises used: not_le, not_exists, mem_lowerBounds, Set.mem_setOf_eq, IsLeast, not_and, Classical.not_forall
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬((↑H : Set G) ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ (↑H : Set G)
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ (x_1 : G) (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
rcases : ∀ (y : G) (hxy : y < x) (hyH : y ∈ H) (hy₀ : 1 < y), False
⊢ False

Tactic:
rcases hxmin x ⟨hxH, (one_le_pow_of_one_le'  h₀.le _).trans_lt hnx⟩ with ⟨y, ⟨hyH, hy₀⟩, hxy⟩

Premises used: LT.lt.le, one_le_pow_of_one_le', And.intro, LE.le.trans_lt
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬((↑H : Set G) ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ (↑H : Set G)
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ (x_1 : G) (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
obtain : ∀ (m : ℕ) (hm : a ^ m < y) (hya : y ≤ a ^ (m + 1)), False
⊢ False

Tactic:
obtain ⟨m, hm, hya⟩ := hex y hy₀
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬((↑H : Set G) ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ (↑H : Set G)
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ (x_1 : G) (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
inl : ∀ (hmn : m < n), False
inr : ∀ (hnm : n ≤ m), False
⊢ False

Tactic:
rcases lt_or_ge m n with hmn | hnm

Premises used: lt_or_ge
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬((↑H : Set G) ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ (↑H : Set G)
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ (x_1 : G) (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
hmn : m < n
⊢ False

Tactic:
hmin m hmn ⟨y, hyH, hm, hya⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬((↑H : Set G) ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ (↑H : Set G)
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ (x_1 : G) (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
hmn : m < n
⊢ False

Tactic:
exact hmin m hmn ⟨y, hyH, hm, hya⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬((↑H : Set G) ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ (↑H : Set G)
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ (x_1 : G) (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
hnm : n ≤ m
⊢ False

Tactic:
disjoint_left.1 hd (div_mem hxH hyH) ⟨one_lt_div'.2 hxy, div_lt_iff_lt_mul'.2 ?_⟩

Premises used: Iff.mpr, div_lt_iff_lt_mul', div_mem, Set.disjoint_left, one_lt_div', And.intro, Iff.mp
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬((↑H : Set G) ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ (↑H : Set G)
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ (x_1 : G) (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
hnm : n ≤ m
inr : x < y * a
⊢ False

Tactic:
refine disjoint_left.1 hd (div_mem hxH hyH) ⟨one_lt_div'.2 hxy, div_lt_iff_lt_mul'.2 ?_⟩

Premises used: Iff.mpr, div_lt_iff_lt_mul', div_mem, Set.disjoint_left, one_lt_div', And.intro, Iff.mp
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬((↑H : Set G) ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ (↑H : Set G)
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ (x_1 : G) (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
hnm : n ≤ m
⊢ x ≤ a ^ (n + 1)

Tactic:
hxn
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬((↑H : Set G) ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ (↑H : Set G)
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ (x_1 : G) (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
hnm : n ≤ m
h₁ : 1 ≤ a
⊢ a ^ (n + 1) ≤ a ^ (m + 1)

Tactic:
grw [hnm]
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬((↑H : Set G) ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ (↑H : Set G)
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ (x_1 : G) (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
hnm : n ≤ m
⊢ 1 ≤ a

Tactic:
h₀.le

Premises used: LT.lt.le
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬((↑H : Set G) ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ (↑H : Set G)
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ (x_1 : G) (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
hnm : n ≤ m
⊢ 1 ≤ a

Tactic:
exact h₀.le

Premises used: LT.lt.le
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬((↑H : Set G) ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ (↑H : Set G)
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ (x_1 : G) (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
hnm : n ≤ m
⊢ a ^ (m + 1) = a ^ m * a

Tactic:
pow_succ _ _

Premises used: pow_succ
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬((↑H : Set G) ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ (↑H : Set G)
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ (x_1 : G) (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
hnm : n ≤ m
⊢ a ^ m * a < y * a

Tactic:
gcongr
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬((↑H : Set G) ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ (↑H : Set G)
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ (x_1 : G) (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
hnm : n ≤ m
calc : a ^ (n + 1) ≤ a ^ (m + 1)
calc₁ : a ^ m * a < y * a
⊢ x < y * a

Tactic:
calc x ≤ a ^ (n + 1) := hxn
    _ ≤ a ^ (m + 1) := by grw [hnm]; exact h₀.le
    _ = a ^ m * a := pow_succ _ _
    _ < y * a := by gcongr

Premises used: pow_succ, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
inl : ∀ (hd : Disjoint (↑⊥ : Set G) (Ioo 1 a)), ∃ (b : G), Eq (α := Subgroup G) ⊥ (closure {b})
inr : ∀ (hbot : H ≠ ⊥), ∃ (b : G), H = closure {b}
⊢ ∃ (b : G), H = closure {b}

Tactic:
rcases eq_or_ne H ⊥ with rfl | hbot

Premises used: Bot.bot, eq_or_ne, rfl
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
h₀ : 1 < a
hd : Disjoint (↑⊥ : Set G) (Ioo 1 a)
⊢ ∃ (b : G), Eq (α := Subgroup G) ⊥ (closure {b})

Tactic:
⟨1, closure_singleton_one.symm⟩

Premises used: Subgroup.closure_singleton_one, Exists.intro, OfNat.ofNat, Eq.symm
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
h₀ : 1 < a
hd : Disjoint (↑⊥ : Set G) (Ioo 1 a)
⊢ ∃ (b : G), Eq (α := Subgroup G) ⊥ (closure {b})

Tactic:
exact ⟨1, closure_singleton_one.symm⟩
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hbot : H ≠ ⊥
⊢ ∃ (b : G), H = closure {b}

Tactic:
(exists_isLeast_one_lt hbot h₀ hd).imp fun _ => cyclic_of_min

Premises used: Exists.imp, Subgroup.exists_isLeast_one_lt, Subgroup.cyclic_of_min
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hbot : H ≠ ⊥
⊢ ∃ (b : G), H = closure {b}

Tactic:
exact (exists_isLeast_one_lt hbot h₀ hd).imp fun _ => cyclic_of_min

Premises used: Exists.imp, Subgroup.exists_isLeast_one_lt, Subgroup.cyclic_of_min
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
H : AddSubgroup ℤ
this : Eq (α := Set ℤ) (Ioo 0 1) ∅
⊢ Disjoint (↑H : Set ℤ) (Ioo 0 1)

Tactic:
simp [this]
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : LinearOrderedCommGroupWithZero G
inst_1 : MulArchimedean G
a : G
ha : a < 1
b : Gˣ
inl : ∀ (ha : LT.lt.{u_1} (α := G) 0 1), ∃ (n : ℕ), HPow.hPow (α := G) 0 n < (↑b : G)
inr : ∀ (ha' : a ≠ 0), ∃ (n : ℕ), a ^ n < (↑b : G)
⊢ ∃ (n : ℕ), a ^ n < (↑b : G)

Tactic:
rcases eq_or_ne a 0 with rfl | ha'

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : LinearOrderedCommGroupWithZero G
inst_1 : MulArchimedean G
b : Gˣ
ha : LT.lt.{u_1} (α := G) 0 1
h : HPow.hPow (α := G) (β := ℕ) 0 1 < (↑b : G)
⊢ ∃ (n : ℕ), HPow.hPow (α := G) 0 n < (↑b : G)

Tactic:
use 1
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : LinearOrderedCommGroupWithZero G
inst_1 : MulArchimedean G
b : Gˣ
ha : LT.lt.{u_1} (α := G) 0 1
⊢ HPow.hPow (α := G) (β := ℕ) 0 1 < (↑b : G)

Tactic:
simp
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : LinearOrderedCommGroupWithZero G
inst_1 : MulArchimedean G
a : G
ha : a < 1
b : Gˣ
ha' : a ≠ 0
⊢ IsUnit a

Tactic:
IsUnit.mk0 _ ha'

Premises used: IsUnit.mk0
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : LinearOrderedCommGroupWithZero G
inst_1 : MulArchimedean G
a : G
ha : a < 1
b : Gˣ
ha' : a ≠ 0
inr : ∀ (a : Gˣ) (ha : (↑a : G) < 1) (ha' : (↑a : G) ≠ 0), ∃ (n : ℕ), (↑a : G) ^ n < (↑b : G)
⊢ ∃ (n : ℕ), a ^ n < (↑b : G)

Tactic:
lift a to Gˣ using IsUnit.mk0 _ ha'

Premises used: IsUnit.mk0
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : LinearOrderedCommGroupWithZero G
inst_1 : MulArchimedean G
b a : Gˣ
ha : (↑a : G) < 1
ha' : (↑a : G) ≠ 0
⊢ ∃ (n : ℕ), (↑a : G) ^ n < (↑b : G)

Tactic:
simpa using exists_pow_lt ha b

Premises used: exists_pow_lt
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
ha : a ≠ 1
rw : (∃ (n : ℤ), a ^ n = b) ↔ ∃! k : ℤ, a ^ k = b
⊢ Membership.mem (γ := Subgroup G) (closure {a}) b ↔ ∃! k : ℤ, a ^ k = b

Tactic:
rw [mem_closure_singleton]

Premises used: Subgroup.mem_closure_singleton
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
ha : a ≠ 1
mp : (∃ (n : ℤ), a ^ n = b) → ∃! k : ℤ, a ^ k = b
mpr : (∃! k : ℤ, a ^ k = b) → ∃ (n : ℤ), a ^ n = b
⊢ (∃ (n : ℤ), a ^ n = b) ↔ ∃! k : ℤ, a ^ k = b

Tactic:
constructor
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
ha : a ≠ 1
this : Function.Injective.{1, u_1 + 1} (β := G) fun (x : ℤ) ↦ a ^ x
m : ℤ
⊢ ∃! k : ℤ, a ^ k = a ^ m

Tactic:
⟨m, rfl, fun k hk ↦ this hk⟩

Premises used: ExistsUnique, And.intro, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
ha : a ≠ 1
this : Function.Injective.{1, u_1 + 1} (β := G) fun (x : ℤ) ↦ a ^ x
m : ℤ
⊢ ∃! k : ℤ, a ^ k = a ^ m

Tactic:
exact ⟨m, rfl, fun k hk ↦ this hk⟩
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
ha : a ≠ 1
mp : Function.Injective.{1, u_1 + 1} (β := G) fun (x : ℤ) ↦ a ^ x
⊢ (∃ (n : ℤ), a ^ n = b) → ∃! k : ℤ, a ^ k = b

Tactic:
suffices Function.Injective (a ^ · : ℤ → G) by
      rintro ⟨m, rfl⟩
      exact ⟨m, rfl, fun k hk ↦ this hk⟩
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
ha : a ≠ 1
mp : ∀ (ha : a < 1), Function.Injective.{1, u_1 + 1} (β := G) fun (x : ℤ) ↦ a ^ x
mp₁ : ∀ (ha : 1 < a), Function.Injective.{1, u_1 + 1} (β := G) fun (x : ℤ) ↦ a ^ x
⊢ Function.Injective.{1, u_1 + 1} (β := G) fun (x : ℤ) ↦ a ^ x

Tactic:
rcases ha.lt_or_gt with ha | ha

Premises used: Ne.lt_or_gt
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
ha_1 : a ≠ 1
ha : a < 1
⊢ Function.Injective.{1, u_1 + 1} (β := G) fun (x : ℤ) ↦ a ^ x

Tactic:
(zpow_right_strictAnti ha).injective

Premises used: zpow_right_strictAnti, StrictAnti.injective
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
ha_1 : a ≠ 1
ha : a < 1
⊢ Function.Injective.{1, u_1 + 1} (β := G) fun (x : ℤ) ↦ a ^ x

Tactic:
exact (zpow_right_strictAnti ha).injective

Premises used: zpow_right_strictAnti, StrictAnti.injective
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
ha_1 : a ≠ 1
ha : 1 < a
⊢ Function.Injective.{1, u_1 + 1} (β := G) fun (x : ℤ) ↦ a ^ x

Tactic:
(zpow_right_strictMono ha).injective

Premises used: zpow_right_strictMono, StrictMono.injective
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
ha_1 : a ≠ 1
ha : 1 < a
⊢ Function.Injective.{1, u_1 + 1} (β := G) fun (x : ℤ) ↦ a ^ x

Tactic:
exact (zpow_right_strictMono ha).injective

Premises used: zpow_right_strictMono, StrictMono.injective
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
ha : a ≠ 1
⊢ (∃! k : ℤ, a ^ k = b) → ∃ (n : ℤ), a ^ n = b

Tactic:
fun h ↦ h.exists

Premises used: ExistsUnique.exists
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
ha : a ≠ 1
⊢ (∃! k : ℤ, a ^ k = b) → ∃ (n : ℤ), a ^ n = b

Tactic:
exact fun h ↦ h.exists
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
e : ℤ ≃+ ℤ
this : Eq (α := ℤ) ((e : (a : ℤ) → ℤ) 1 : ℤ) (1 : ℤ) ∨ Eq (α := ℤ) (-(e : (a : ℤ) → ℤ) 1 : ℤ) (1 : ℤ)
⊢ e = AddEquiv.refl ℤ ∨ e = AddEquiv.neg ℤ

Tactic:
simpa [AddEquiv.ext_int_iff, neg_eq_iff_eq_neg]

Premises used: neg_eq_iff_eq_neg, AddEquiv.ext_int_iff
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
e : ℤ ≃+ ℤ
suffices : Eq (α := ℤ) ((e : (a : ℤ) → ℤ) 1 : ℤ) (1 : ℤ) ∨ Eq (α := ℤ) (-(e : (a : ℤ) → ℤ) 1 : ℤ) (1 : ℤ)
⊢ e = AddEquiv.refl ℤ ∨ e = AddEquiv.neg ℤ

Tactic:
suffices e 1 = 1 ∨ -e 1 = 1 by simpa [AddEquiv.ext_int_iff, neg_eq_iff_eq_neg]
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
e : ℤ ≃+ ℤ
⊢ ¬IsOfFinAddOrder (G := ℤ) ((e : (a : ℤ) → ℤ) 1 : ℤ)

Tactic:
have he : ¬IsOfFinAddOrder (e 1) :=
    not_isOfFinAddOrder_of_isAddTorsionFree ((AddEquiv.map_ne_zero_iff e).mpr Int.one_ne_zero)
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
e : ℤ ≃+ ℤ
he : ¬IsOfFinAddOrder (G := ℤ) ((e : (a : ℤ) → ℤ) 1 : ℤ)
rw :
  Eq (α := AddSubgroup ℤ) (AddSubgroup.zmultiples ((e : (a : ℤ) → ℤ) 1) : AddSubgroup ℤ)
    (AddSubgroup.zmultiples 1 : AddSubgroup ℤ)
⊢ Eq (α := ℤ) ((e : (a : ℤ) → ℤ) 1 : ℤ) (1 : ℤ) ∨ Eq (α := ℤ) (-(e : (a : ℤ) → ℤ) 1 : ℤ) (1 : ℤ)

Tactic:
rw [← AddSubgroup.zmultiples_eq_zmultiples_iff he]

Premises used: AddSubgroup.zmultiples_eq_zmultiples_iff
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
e : ℤ ≃+ ℤ
he : ¬IsOfFinAddOrder (G := ℤ) ((e : (a : ℤ) → ℤ) 1 : ℤ)
⊢ Eq (α := AddSubgroup ℤ) (AddSubgroup.zmultiples ((e : (a : ℤ) → ℤ) 1) : AddSubgroup ℤ)
    (AddSubgroup.zmultiples 1 : AddSubgroup ℤ)

Tactic:
simpa [e.surjective, eq_comm] using (e : ℤ →+ ℤ).map_zmultiples 1

Premises used: AddMonoidHomClass.toAddMonoidHom, eq_comm, AddEquiv.surjective, AddMonoidHom.map_zmultiples, OfNat.ofNat
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
⊢ AddEquiv.neg ℤ ∉ {AddEquiv.refl ℤ}

Tactic:
simp [AddEquiv.ext_int_iff]

Premises used: AddEquiv.ext_int_iff
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
x : ℤ ≃+ ℤ
inl : AddEquiv.refl ℤ ∈ Finset.cons (AddEquiv.neg ℤ) {AddEquiv.refl ℤ} instFintypeAddEquivInt._proof_1
inr : AddEquiv.neg ℤ ∈ Finset.cons (AddEquiv.neg ℤ) {AddEquiv.refl ℤ} instFintypeAddEquivInt._proof_1
⊢ x ∈ Finset.cons (AddEquiv.neg ℤ) {AddEquiv.refl ℤ} instFintypeAddEquivInt._proof_1

Tactic:
obtain rfl | rfl := Int.addEquiv_eq_refl_or_neg x

Premises used: Int.addEquiv_eq_refl_or_neg, rfl
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
⊢ AddEquiv.refl ℤ ∈ Finset.cons (AddEquiv.neg ℤ) {AddEquiv.refl ℤ} instFintypeAddEquivInt._proof_1

Tactic:
simp
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
⊢ AddEquiv.neg ℤ ∈ Finset.cons (AddEquiv.neg ℤ) {AddEquiv.refl ℤ} instFintypeAddEquivInt._proof_1

Tactic:
simp
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
⊢ Finset.univ = Finset.cons (AddEquiv.neg ℤ) {AddEquiv.refl ℤ} instFintypeAddEquivInt._proof_1

Tactic:
rfl

Premises used: Finset.univ, Finset.cons, rfl
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
⊢ Fintype.card (ℤ ≃+ ℤ) = 2

Tactic:
rfl

Premises used: Fintype.card, Finset.card, Multiset.card, rfl
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
e : ℤ ≃+o ℤ
H : Eq (α := ℤ ≃+ ℤ) (↑e : ℤ ≃+ ℤ) (AddEquiv.neg ℤ)
⊢ Eq (α := ℤ) ((e : (a : ℤ) → ℤ) 1 : ℤ) (-1 : ℤ)

Tactic:
replace H : e 1 = -1 := congr($H 1)
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
e : ℤ ≃+o ℤ
H : Eq (α := ℤ) ((e : (a : ℤ) → ℤ) 1 : ℤ) (-1 : ℤ)
rw : LT.lt (α := ℤ) 0 1
⊢ LT.lt (α := ℤ) (0 : ℤ) ((e : (a : ℤ) → ℤ) 1 : ℤ)

Tactic:
rw [← map_zero e, map_lt_map_iff]

Premises used: map_zero, map_lt_map_iff