From a4edf40f0bfdbb2237b0816dad780e12c2f1ae87 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 6 Aug 2024 01:12:34 -0400
Subject: [PATCH 1/3] Snapshot

---
 Mathlib/Algebra/Group/Defs.lean               | 17 ++++++++-
 .../GroupTheory/SpecificGroups/Cyclic.lean    | 38 ++++++-------------
 2 files changed, 28 insertions(+), 27 deletions(-)

diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean
index fbd37bae38782..087ec9658c6b1 100644
--- a/Mathlib/Algebra/Group/Defs.lean
+++ b/Mathlib/Algebra/Group/Defs.lean
@@ -5,6 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
 -/
 import Mathlib.Data.Int.Notation
 import Mathlib.Algebra.Group.ZeroOne
+import Mathlib.Logic.Function.Defs
 import Mathlib.Tactic.Lemma
 import Mathlib.Tactic.TypeStar
 import Mathlib.Tactic.Simps.Basic
@@ -860,6 +861,20 @@ instance SubNegMonoid.SMulInt {M} [SubNegMonoid M] : SMul ℤ M :=
 
 attribute [to_additive existing SubNegMonoid.SMulInt] DivInvMonoid.Pow
 
+/-- A group is called *cyclic* if it is generated by a single element. -/
+class IsAddCyclic (G : Type u) [SMul ℤ G] : Prop where
+  protected exists_zsmul_surjective : ∃ g : G, Function.Surjective (· • g : ℤ → G)
+
+/-- A group is called *cyclic* if it is generated by a single element. -/
+@[to_additive]
+class IsCyclic (G : Type u) [Pow G ℤ] : Prop where
+  protected exists_zpow_surjective : ∃ g : G, Function.Surjective (g ^ · : ℤ → G)
+
+@[to_additive]
+theorem exists_zpow_surjective (G : Type*) [Pow G ℤ] [IsCyclic G] :
+    ∃ g : G, Function.Surjective (g ^ · : ℤ → G) :=
+  IsCyclic.exists_zpow_surjective
+
 section DivInvMonoid
 
 variable [DivInvMonoid G] {a b : G}
@@ -1163,5 +1178,5 @@ initialize_simps_projections AddGroup
 initialize_simps_projections CommGroup
 initialize_simps_projections AddCommGroup
 
-assert_not_exists Function.Injective
+assert_not_exists Function.Injective.eq_iff
 assert_not_exists IsCommutative
diff --git a/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean b/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
index f32c588e807ba..02bdc1e54f0cc 100644
--- a/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
+++ b/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
@@ -49,20 +49,13 @@ attribute [local instance] setFintype
 
 open Subgroup
 
-/-- A group is called *cyclic* if it is generated by a single element. -/
-class IsAddCyclic (α : Type u) [AddGroup α] : Prop where
-  exists_generator : ∃ g : α, ∀ x, x ∈ AddSubgroup.zmultiples g
-
-/-- A group is called *cyclic* if it is generated by a single element. -/
 @[to_additive]
-class IsCyclic (α : Type u) [Group α] : Prop where
-  exists_generator : ∃ g : α, ∀ x, x ∈ zpowers g
+theorem IsCyclic.exists_generator [Group α] [IsCyclic α] : ∃ g : α, ∀ x, x ∈ Subgroup.zpowers g :=
+  exists_zpow_surjective α
 
 @[to_additive]
 instance (priority := 100) isCyclic_of_subsingleton [Group α] [Subsingleton α] : IsCyclic α :=
-  ⟨⟨1, fun x => by
-      rw [Subsingleton.elim x 1]
-      exact mem_zpowers 1⟩⟩
+  ⟨⟨1, fun _ => ⟨0, Subsingleton.elim _ _⟩⟩⟩
 
 @[simp]
 theorem isCyclic_multiplicative_iff [AddGroup α] : IsCyclic (Multiplicative α) ↔ IsAddCyclic α :=
@@ -113,11 +106,10 @@ MonoidAddHom.map_add_cyclic := AddMonoidHom.map_addCyclic
 @[to_additive]
 theorem isCyclic_of_orderOf_eq_card [Fintype α] (x : α) (hx : orderOf x = Fintype.card α) :
     IsCyclic α := by
-  classical
-    use x
-    simp_rw [← SetLike.mem_coe, ← Set.eq_univ_iff_forall]
-    rw [← Fintype.card_congr (Equiv.Set.univ α), ← Fintype.card_zpowers] at hx
-    exact Set.eq_of_subset_of_card_le (Set.subset_univ _) (ge_of_eq hx)
+  use x
+  rw [← Set.range_iff_surjective, ← coe_zpowers]
+  rw [← Fintype.card_congr (Equiv.Set.univ α), ← Fintype.card_zpowers] at hx
+  exact Set.eq_of_subset_of_card_le (Set.subset_univ _) (ge_of_eq hx)
 @[deprecated (since := "2024-02-21")]
 alias isAddCyclic_of_orderOf_eq_card := isAddCyclic_of_addOrderOf_eq_card
 
@@ -561,17 +553,11 @@ variable [CommGroup α] [IsSimpleGroup α]
 
 @[to_additive]
 instance (priority := 100) isCyclic : IsCyclic α := by
-  cases' subsingleton_or_nontrivial α with hi hi <;> haveI := hi
-  · apply isCyclic_of_subsingleton
-  · obtain ⟨g, hg⟩ := exists_ne (1 : α)
-    refine ⟨⟨g, fun x => ?_⟩⟩
-    cases' IsSimpleOrder.eq_bot_or_eq_top (Subgroup.zpowers g) with hb ht
-    · exfalso
-      apply hg
-      rw [← Subgroup.mem_bot, ← hb]
-      apply Subgroup.mem_zpowers
-    · rw [ht]
-      apply Subgroup.mem_top
+  nontriviality α
+  obtain ⟨g, hg⟩ := exists_ne (1 : α)
+  have : Subgroup.zpowers g = ⊤ :=
+    (eq_bot_or_eq_top (Subgroup.zpowers g)).resolve_left (Subgroup.zpowers_ne_bot.2 hg)
+  exact ⟨⟨g, (Subgroup.eq_top_iff' _).1 this⟩⟩
 
 @[to_additive]
 theorem prime_card [Fintype α] : (Fintype.card α).Prime := by

From 732870eb7025a035958f9fc887bd3e4e15fe6d33 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 6 Aug 2024 08:27:54 -0400
Subject: [PATCH 2/3] Shake an import

---
 Mathlib/Logic/Function/Defs.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Logic/Function/Defs.lean b/Mathlib/Logic/Function/Defs.lean
index 97aa6b6452579..57c703c66bfff 100644
--- a/Mathlib/Logic/Function/Defs.lean
+++ b/Mathlib/Logic/Function/Defs.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Haitao Zhang
 -/
 import Mathlib.Tactic.AdaptationNote
 import Mathlib.Tactic.Attr.Register
-import Mathlib.Tactic.Basic
+import Mathlib.Tactic.Lemma
 import Mathlib.Tactic.Eqns
 import Mathlib.Tactic.TypeStar
 import Batteries.Logic

From 54abc4a4a7f61e34ad0e49c2467a0605b3c75c3e Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 6 Aug 2024 09:19:54 -0400
Subject: [PATCH 3/3] feat(Order/Group): a nontrivial densely linear ordered
 group isn't cyclic

---
 Mathlib/Algebra/Order/Group/Basic.lean | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/Mathlib/Algebra/Order/Group/Basic.lean b/Mathlib/Algebra/Order/Group/Basic.lean
index 09aeb718a03a4..418e88d11ca9a 100644
--- a/Mathlib/Algebra/Order/Group/Basic.lean
+++ b/Mathlib/Algebra/Order/Group/Basic.lean
@@ -102,4 +102,27 @@ lemma zpow_left_inj (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b := (zpow_left_injec
 `zsmul_lt_zsmul_iff'`."]
 lemma zpow_eq_zpow_iff' (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b := zpow_left_inj hn
 
+variable (α) in
+/-- A nontrivial densely linear ordered commutative group can't be a cyclic group. -/
+@[to_additive
+  "A nontrivial densely linear ordered additive commutative group can't be a cyclic group."]
+theorem not_isCyclic_of_denselyOrdered [DenselyOrdered α] [Nontrivial α] : ¬IsCyclic α := by
+  intro h
+  rcases exists_zpow_surjective α with ⟨a, ha⟩
+  rcases lt_trichotomy a 1 with hlt | rfl | hlt
+  · rcases exists_between hlt with ⟨b, hab, hb⟩
+    rcases ha b with ⟨k, rfl⟩
+    suffices 0 < k ∧ k < 1 by omega
+    rw [← one_lt_inv'] at hlt
+    simp_rw [← zpow_lt_zpow_iff hlt]
+    simp_all
+  · rcases exists_ne (1 : α) with ⟨b, hb⟩
+    simpa [hb.symm] using ha b
+  · rcases exists_between hlt with ⟨b, hb, hba⟩
+    rcases ha b with ⟨k, rfl⟩
+    suffices 0 < k ∧ k < 1 by omega
+    simp_rw [← zpow_lt_zpow_iff hlt]
+    simp_all
+
 end LinearOrderedCommGroup
+