-- 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 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

Tactic:
refine ⟨?_, ?_⟩

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

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

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
⊢ mabs (b ^ n) = b ∧ 1 < b

Tactic:
rcases key with ⟨rfl, rfl⟩|⟨rfl, rfl⟩ <;>
simp [this.right.le, this.right, mabs]

Result:
no goals

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
⊢ b = mabs a⁻¹ ∧ 1 < b

Tactic:
rwa [mabs_inv]

Result:
no goals

Proof state:
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
⊢ 1 ≤ a⁻¹

Tactic:
simpa using le_of_not_le ha

Result:
no goals

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
⊢ b = mabs (b ^ n) ∧ 1 < b

Tactic:
have key : m * n = 1 := by
  rw [← zpow_right_inj this.right, zpow_mul', hm, zpow_one]

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 * n = 1
⊢ 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
⊢ b ∈ lowerBounds {y | y ∈ closure {b} ∧ 1 < y}

Tactic:
intro x

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 ∈ {y | y ∈ closure {b} ∧ 1 < y} → b ≤ x

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 : (∃ n_1, (b ^ n) ^ n_1 = b) ∧ 1 < b
⊢ b = mabs (b ^ n) ∧ 1 < b

Tactic:
obtain ⟨m, hm⟩ := this.left

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
⊢ b = mabs (b ^ n) ∧ 1 < b

Proof state:
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⁻¹}

Tactic:
simp

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 : a ∈ closure {b}
⊢ b = mabs a ∧ 1 < b

Tactic:
rw [mem_closure_singleton] at ha

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
this : closure {a} = closure {b}
ha : ∃ n, b ^ n = a
⊢ b = mabs a ∧ 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}
⊢ b = mabs (b ^ n) ∧ 1 < b

Tactic:
have := h.left

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 : b ∈ {y | y ∈ closure {b ^ n} ∧ 1 < y}
⊢ 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
⊢ 1 ≤ b ^ (-k)

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

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
⊢ b = mabs a ∧ 1 < b

Tactic:
have := Subgroup.cyclic_of_min 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
this : closure {a} = closure {b}
⊢ b = mabs a ∧ 1 < b

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

Tactic:
simp [h]

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
k : ℤ
hk : 1 < b ^ 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]

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
⊢ 0 < k

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}
⊢ b = mabs a ∧ 1 < b

Tactic:
have ha : a ∈ closure ({b} : Set G) := by
  simp [← this]

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
this : closure {a} = closure {b}
ha : a ∈ closure {b}
⊢ b = mabs a ∧ 1 < b