-- Mathlib/Algebra/Order/Group/Basic.lean
theorem not_isCyclic_of_denselyOrdered [DenselyOrdered α] [Nontrivial α] : ¬IsCyclic α

Proof state:
case intro.inl.intro.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : a < 1
k : ℤ
hab : a < (fun x => a ^ x) k
hb : (fun x => a ^ x) k < 1
⊢ 0 < k ∧ k < 1

Tactic:
rw [← one_lt_inv'] at hlt

Result:
case intro.inl.intro.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : 1 < a⁻¹
k : ℤ
hab : a < (fun x => a ^ x) k
hb : (fun x => a ^ x) k < 1
⊢ 0 < k ∧ k < 1

Proof state:
case intro.inl
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : a < 1
⊢ False

Tactic:
rcases exists_between hlt with ⟨b, hab, hb⟩

Result:
case intro.inl.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : a < 1
b : α
hab : a < b
hb : b < 1
⊢ False

Proof state:
case intro.inr.inr.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : 1 < a
b : α
hb : 1 < b
hba : b < a
⊢ False

Tactic:
rcases ha b with ⟨k, rfl⟩

Result:
case intro.inr.inr.intro.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : 1 < a
k : ℤ
hb : 1 < (fun x => a ^ x) k
hba : (fun x => a ^ x) k < a
⊢ False

Proof state:
case intro.inr.inr.intro.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : 1 < a
k : ℤ
hb : 1 < (fun x => a ^ x) k
hba : (fun x => a ^ x) k < a
⊢ a ^ 0 < a ^ k ∧ a ^ k < a ^ 1

Tactic:
simp_all

Result:
no goals

Proof state:
case intro.inl.intro.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : 1 < a⁻¹
k : ℤ
hab : a < (fun x => a ^ x) k
hb : (fun x => a ^ x) k < 1
⊢ a⁻¹ ^ 0 < a⁻¹ ^ k ∧ a⁻¹ ^ k < a⁻¹ ^ 1

Tactic:
simp_all

Result:
no goals

Proof state:
case intro.inl.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : a < 1
b : α
hab : a < b
hb : b < 1
⊢ False

Tactic:
rcases ha b with ⟨k, rfl⟩

Result:
case intro.inl.intro.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : a < 1
k : ℤ
hab : a < (fun x => a ^ x) k
hb : (fun x => a ^ x) k < 1
⊢ False

Proof state:
case intro.inr.inr.intro.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : 1 < a
k : ℤ
hb : 1 < (fun x => a ^ x) k
hba : (fun x => a ^ x) k < a
⊢ 0 < k ∧ k < 1

Tactic:
simp_rw [← zpow_lt_zpow_iff_right hlt]

Result:
case intro.inr.inr.intro.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : 1 < a
k : ℤ
hb : 1 < (fun x => a ^ x) k
hba : (fun x => a ^ x) k < a
⊢ a ^ 0 < a ^ k ∧ a ^ k < a ^ 1

Proof state:
case intro.inl.intro.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : a < 1
k : ℤ
hab : a < (fun x => a ^ x) k
hb : (fun x => a ^ x) k < 1
⊢ False

Tactic:
suffices 0 < k ∧ k < 1 by omega

Result:
case intro.inl.intro.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : a < 1
k : ℤ
hab : a < (fun x => a ^ x) k
hb : (fun x => a ^ x) k < 1
⊢ 0 < k ∧ k < 1

Proof state:
case intro
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
⊢ False

Tactic:
rcases lt_trichotomy a 1 with hlt | rfl | hlt

Result:
case intro.inl
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : a < 1
⊢ False

case intro.inr.inl
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
ha : Surjective fun x => 1 ^ x
⊢ False

case intro.inr.inr
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : 1 < a
⊢ False

Proof state:
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
⊢ ¬IsCyclic α

Tactic:
intro h

Result:
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
⊢ False

Proof state:
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : 1 < a
k : ℤ
hb : 1 < (fun x => a ^ x) k
hba : (fun x => a ^ x) k < a
this : 0 < k ∧ k < 1
⊢ False

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
⊢ False

Tactic:
rcases exists_zpow_surjective α with ⟨a, ha⟩

Result:
case intro
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
⊢ False

Proof state:
case intro.inr.inl.intro
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
ha : Surjective fun x => 1 ^ x
b : α
hb : b ≠ 1
⊢ False

Tactic:
simpa [hb.symm] using ha b

Result:
no goals

Proof state:
case intro.inr.inr.intro.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : 1 < a
k : ℤ
hb : 1 < (fun x => a ^ x) k
hba : (fun x => a ^ x) k < a
⊢ False

Tactic:
suffices 0 < k ∧ k < 1 by omega

Result:
case intro.inr.inr.intro.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : 1 < a
k : ℤ
hb : 1 < (fun x => a ^ x) k
hba : (fun x => a ^ x) k < a
⊢ 0 < k ∧ k < 1

Proof state:
case intro.inr.inl
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
ha : Surjective fun x => 1 ^ x
⊢ False

Tactic:
rcases exists_ne (1 : α) with ⟨b, hb⟩

Result:
case intro.inr.inl.intro
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
ha : Surjective fun x => 1 ^ x
b : α
hb : b ≠ 1
⊢ False

Proof state:
case intro.inr.inr
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : 1 < a
⊢ False

Tactic:
rcases exists_between hlt with ⟨b, hb, hba⟩

Result:
case intro.inr.inr.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : 1 < a
b : α
hb : 1 < b
hba : b < a
⊢ False