-- Mathlib/GroupTheory/ArchimedeanDensely.lean
@[to_additive]
lemma Subgroup.isLeast_of_closure_iff_eq_mabs {a b : G} :
    IsLeast {y : G | y ∈ closure ({a} : Set G) ∧ 1 < y} b ↔ b = |a|ₘ ∧ 1 < b

Proof state:
case mpr
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
a b : G
h : b = mabs a ∧ 1 < b
⊢ IsLeast {y | y ∈ closure {a} ∧ 1 < y} b

Tactic:
wlog ha : 1 ≤ a generalizing a

Result:
case mpr.inr
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
a b : G
h : b = mabs a ∧ 1 < b
this : ∀ {a : G}, b = mabs a ∧ 1 < b → 1 ≤ a → IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
ha : ¬1 ≤ a
⊢ IsLeast {y | y ∈ closure {a} ∧ 1 < y} b

G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
b a : G
h : b = mabs a ∧ 1 < b
ha : 1 ≤ a
⊢ IsLeast {y | y ∈ closure {a} ∧ 1 < y} b

Proof state:
case intro.refine_2
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
k : ℤ
hk : 1 < b ^ k
⊢ 0 < k

Tactic:
contrapose! hk

Result:
case intro.refine_2
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
k : ℤ
hk : k ≤ 0
⊢ b ^ k ≤ 1

Proof state:
case mp.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y | y ∈ closure {b ^ n} ∧ 1 < y} b
this✝ : 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 = mabs (b ^ n) ∧ 1 < b

Tactic:
rw [eq_comm]

Result:
case mp.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y | y ∈ closure {b ^ n} ∧ 1 < y} b
this✝ : 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
⊢ mabs (b ^ n) = b ∧ 1 < b

Proof state:
case mp.intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y | y ∈ closure {b ^ n} ∧ 1 < y} b
this✝ : closure {b ^ n} = closure {b}
this : b ∈ {y | y ∈ closure {b ^ n} ∧ 1 < y}
⊢ b = mabs (b ^ n) ∧ 1 < b

Tactic:
simp only [mem_closure_singleton, mem_setOf_eq, ← mul_zsmul] at this

Result:
case mp.intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y | y ∈ closure {b ^ n} ∧ 1 < y} b
this✝ : closure {b ^ n} = closure {b}
this : (∃ n_1, (b ^ n) ^ n_1 = b) ∧ 1 < b
⊢ b = mabs (b ^ n) ∧ 1 < b

Proof state:
case intro.refine_2
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
k : ℤ
hk : k ≤ 0
⊢ b ^ k ≤ 1

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

Result:
case intro.refine_2
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
k : ℤ
hk : k ≤ 0
⊢ 1 ≤ b ^ (-k)

Proof state:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
k : ℤ
hk : k ≤ 0
⊢ 0 ≤ -k

Tactic:
simp [hk]

Result:
no goals

Proof state:
case intro.refine_2
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
x : G
⊢ x ∈ {y | y ∈ closure {b} ∧ 1 < y} → b ≤ x

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

Result:
case intro.refine_2
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
x : G
⊢ ∀ (x_1 : ℤ), b ^ x_1 = x → 1 < x → b ≤ x

Proof state:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y | y ∈ closure {b ^ n} ∧ 1 < y} b
this✝ : closure {b ^ n} = closure {b}
this : (∃ n_1, (b ^ n) ^ n_1 = b) ∧ 1 < b
m : ℤ
hm : (b ^ n) ^ m = b
⊢ m * n = 1

Tactic:
rw [← zpow_right_inj this.right, zpow_mul', hm, zpow_one]

Result:
no goals

Proof state:
case mp
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
a b : G
h : IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
this : closure {a} = closure {b}
ha : ∃ n, b ^ n = a
⊢ b = mabs a ∧ 1 < b

Tactic:
obtain ⟨n, rfl⟩ := ha

Result:
case mp.intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y | y ∈ closure {b ^ n} ∧ 1 < y} b
this : closure {b ^ n} = closure {b}
⊢ b = mabs (b ^ n) ∧ 1 < b

Proof state:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
a b : G
h : IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
this : closure {a} = closure {b}
⊢ a ∈ closure {b}

Tactic:
simp [← this]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
b a : G
h : b = mabs a ∧ 1 < b
ha : 1 ≤ a
⊢ IsLeast {y | y ∈ closure {a} ∧ 1 < y} b

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

Result:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
b a : G
h : b = a ∧ 1 < b
ha : 1 ≤ a
⊢ IsLeast {y | y ∈ closure {a} ∧ 1 < y} b

Proof state:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
b a : G
h : b = a ∧ 1 < b
ha : 1 ≤ a
⊢ IsLeast {y | y ∈ closure {a} ∧ 1 < y} b

Tactic:
rcases h with ⟨rfl, h⟩

Result:
case intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
⊢ IsLeast {y | y ∈ closure {b} ∧ 1 < y} b

Proof state:
case mp.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y | y ∈ closure {b ^ n} ∧ 1 < y} b
this✝ : 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 = mabs (b ^ n) ∧ 1 < b

Tactic:
rw [Int.mul_eq_one_iff_eq_one_or_neg_one] at key

Result:
case mp.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y | y ∈ closure {b ^ n} ∧ 1 < y} b
this✝ : 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 = mabs (b ^ n) ∧ 1 < b

Proof state:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
a b : G
⊢ IsLeast {y | y ∈ closure {a} ∧ 1 < y} b ↔ b = mabs a ∧ 1 < b

Tactic:
constructor <;> intro h

Result:
case mp
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
a b : G
h : IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
⊢ b = mabs a ∧ 1 < b

case mpr
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
a b : G
h : b = mabs a ∧ 1 < b
⊢ IsLeast {y | y ∈ closure {a} ∧ 1 < y} b

Proof state:
case mpr.inr
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
a b : G
h : b = mabs a ∧ 1 < b
this : ∀ {a : G}, b = mabs a ∧ 1 < b → 1 ≤ a → IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
ha : ¬1 ≤ a
⊢ IsLeast {y | y ∈ closure {a} ∧ 1 < y} b

Tactic:
convert @this (a⁻¹) ?_ (by simpa using le_of_not_le ha) using 4

Result:
case h.e'_3.h.e'_2.h.h.e'_1.a
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
a b : G
h : b = mabs a ∧ 1 < b
this : ∀ {a : G}, b = mabs a ∧ 1 < b → 1 ≤ a → IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
ha : ¬1 ≤ a
x✝ : G
⊢ x✝ ∈ closure {a} ↔ x✝ ∈ closure {a⁻¹}

case mpr.inr
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
a b : G
h : b = mabs a ∧ 1 < b
this : ∀ {a : G}, b = mabs a ∧ 1 < b → 1 ≤ a → IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
ha : ¬1 ≤ a
⊢ b = mabs a⁻¹ ∧ 1 < b

Proof state:
case intro.refine_2
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
x : G
⊢ ∀ (x_1 : ℤ), b ^ x_1 = x → 1 < x → b ≤ x

Tactic:
rintro k rfl hk

Result:
case intro.refine_2
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
k : ℤ
hk : 1 < b ^ k
⊢ b ≤ b ^ k