-- Mathlib/GroupTheory/Archimedean.lean
theorem Subgroup.exists_isLeast_one_lt {H : Subgroup G} (hbot : H ≠ ⊥) {a : G} (h₀ : 1 < a)
    (hd : Disjoint (H : Set G) (Ioo 1 a)) : ∃ b, IsLeast { g : G | g ∈ H ∧ 1 < g } b

Proof state:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
⊢ ∃ b, IsLeast {g | g ∈ H ∧ 1 < g} b

Tactic:
rcases Nat.findX this with ⟨n, ⟨x, hxH, hnx, hxn⟩, hmin⟩

Result:
case mk.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
⊢ ∃ b, IsLeast {g | g ∈ H ∧ 1 < g} b

Proof state:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
g : G
hg : g > 1
⊢ ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))

Tactic:
rcases existsUnique_mul_zpow_mem_Ico h₀ 1 (g / a) with ⟨m, ⟨hm, hm'⟩, -⟩

Result:
case intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
g : G
hg : g > 1
m : ℤ
hm : g / a ≤ 1 * a ^ m
hm' : 1 * a ^ m < g / a * a
⊢ ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))

Proof state:
case mk.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ¬∃ b, IsLeast {g | g ∈ H ∧ 1 < g} b
⊢ False

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

Result:
case mk.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ x_1, ∃ (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
⊢ False

Proof state:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
g : G
hg : g > 1
m : ℤ
hm : g ≤ a ^ (m + 1)
hm' : a ^ m < g
⊢ 0 ≤ m

Tactic:
rw [← Int.lt_add_one_iff, ← zpow_lt_zpow_iff_right h₀, zpow_zero]

Result:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
g : G
hg : g > 1
m : ℤ
hm : g ≤ a ^ (m + 1)
hm' : a ^ m < g
⊢ 1 < a ^ (m + 1)

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
g : G
hg : g > 1
m : ℕ
hm : g ≤ a ^ m.succ
hm' : a ^ m < g
⊢ ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))

Tactic:
exact ⟨m, hm', hm⟩

Result:
no goals

Proof state:
case intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
g : G
hg : g > 1
m : ℤ
hm : g / a ≤ 1 * a ^ m
hm' : 1 * a ^ m < g / a * a
⊢ ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))

Tactic:
simp only [one_mul, div_le_iff_le_mul, div_mul_cancel, ← zpow_add_one] at hm hm'

Result:
case intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
g : G
hg : g > 1
m : ℤ
hm : g ≤ a ^ (m + 1)
hm' : a ^ m < g
⊢ ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
g : G
hg : g > 1
m : ℕ
hm : g ≤ a ^ (↑m + 1)
hm' : a ^ ↑m < g
⊢ ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))

Tactic:
simp only [← Nat.cast_succ, zpow_natCast] at hm hm'

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
g : G
hg : g > 1
m : ℕ
hm : g ≤ a ^ m.succ
hm' : a ^ m < g
⊢ ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))

Proof state:
case mk.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ x_1, ∃ (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : y ∈ Ioc (a ^ m) (a ^ (m + 1))
⊢ False

Tactic:
rcases lt_or_le m n with hmn | hnm

Result:
case mk.intro.intro.intro.intro.intro.intro.intro.intro.inl
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ x_1, ∃ (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : y ∈ Ioc (a ^ m) (a ^ (m + 1))
hmn : m < n
⊢ False

case mk.intro.intro.intro.intro.intro.intro.intro.intro.inr
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ x_1, ∃ (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : y ∈ Ioc (a ^ m) (a ^ (m + 1))
hnm : n ≤ m
⊢ False

Proof state:
case mk.intro.intro.intro.intro.intro.intro.intro.intro.inr
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ x_1, ∃ (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : y ∈ Ioc (a ^ m) (a ^ (m + 1))
hnm : n ≤ m
⊢ x < y * a

Tactic:
calc x ≤ a^ (n + 1) := hxn
_ ≤ a ^ (m + 1) := pow_le_pow_right' h₀.le (add_le_add_right hnm _)
_ = a ^ m * a := pow_succ _ _
_ < y * a := mul_lt_mul_right' hm.1 _

Result:
no goals