feat(to_additive + Cyclic): auto Cyclic --> addCyclic (#8722)

Teach the conversion `Cyclic ↦ addCyclic` to `to_additive`.

Affected files:
```bash
GroupTheory/SpecificGroups/Cyclic
Tactic/ToAdditive
```

Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

@@ -58,12 +58,12 @@ class IsAddCyclic (α : Type u) [AddGroup α] : Prop where
 #align is_add_cyclic IsAddCyclic
 
 /-- A group is called *cyclic* if it is generated by a single element. -/
-@[to_additive IsAddCyclic]
+@[to_additive]
 class IsCyclic (α : Type u) [Group α] : Prop where
   exists_generator : ∃ g : α, ∀ x, x ∈ zpowers g
 #align is_cyclic IsCyclic
 
-@[to_additive isAddCyclic_of_subsingleton]
+@[to_additive]
 instance (priority := 100) isCyclic_of_subsingleton [Group α] [Subsingleton α] : IsCyclic α :=
   ⟨⟨1, fun x => by
       rw [Subsingleton.elim x 1]
@@ -102,10 +102,8 @@ def IsCyclic.commGroup [hg : Group α] [IsCyclic α] : CommGroup α :=
 
 variable [Group α]
 
-/-- A non-cyclic multiplicative group is non-trivial.
-The additive version is `Nontrivial.of_not_isAddCyclic`. -/
-@[to_additive Nontrivial.of_not_isAddCyclic "A non-cyclic additive group is non-trivial.
-The multiplicative version is `Nontrivial.of_not_isCyclic`."]
+/-- A non-cyclic multiplicative group is non-trivial. -/
+@[to_additive "A non-cyclic additive group is non-trivial."]
 theorem Nontrivial.of_not_isCyclic (nc : ¬IsCyclic α) : Nontrivial α := by
   contrapose! nc
   exact @isCyclic_of_subsingleton _ _ (not_nontrivial_iff_subsingleton.mp nc)
@@ -133,7 +131,7 @@ theorem isCyclic_of_orderOf_eq_card [Fintype α] (x : α) (hx : orderOf x = Fint
 #align is_add_cyclic_of_order_of_eq_card isAddCyclic_of_orderOf_eq_card
 
 /-- A finite group of prime order is cyclic. -/
-@[to_additive isAddCyclic_of_prime_card "A finite group of prime order is cyclic."]
+@[to_additive "A finite group of prime order is cyclic."]
 theorem isCyclic_of_prime_card {α : Type u} [Group α] [Fintype α] {p : ℕ} [hp : Fact p.Prime]
     (h : Fintype.card α = p) : IsCyclic α :=
   ⟨by
@@ -164,7 +162,7 @@ theorem isCyclic_of_prime_card {α : Type u} [Group α] [Fintype α] {p : ℕ} [
 #align is_cyclic_of_prime_card isCyclic_of_prime_card
 #align is_add_cyclic_of_prime_card isAddCyclic_of_prime_card
 
-@[to_additive isAddCyclic_of_surjective]
+@[to_additive]
 theorem isCyclic_of_surjective {H G F : Type*} [Group H] [Group G] [hH : IsCyclic H]
     [MonoidHomClass F H G] (f : F) (hf : Function.Surjective f) : IsCyclic G := by
   obtain ⟨x, hx⟩ := hH
@@ -183,7 +181,7 @@ theorem orderOf_eq_card_of_forall_mem_zpowers [Fintype α] {g : α} (hx : ∀ x,
 #align order_of_eq_card_of_forall_mem_zpowers orderOf_eq_card_of_forall_mem_zpowers
 #align add_order_of_eq_card_of_forall_mem_zmultiples addOrderOf_eq_card_of_forall_mem_zmultiples
 
-@[to_additive exists_nsmul_ne_zero_of_isAddCyclic]
+@[to_additive]
 theorem exists_pow_ne_one_of_isCyclic {G : Type*} [Group G] [Fintype G] [G_cyclic : IsCyclic G]
     {k : ℕ} (k_pos : k ≠ 0) (k_lt_card_G : k < Fintype.card G) : ∃ a : G, a ^ k ≠ 1 := by
   rcases G_cyclic with ⟨a, ha⟩
@@ -216,13 +214,13 @@ theorem Infinite.orderOf_eq_zero_of_forall_mem_zpowers [Infinite α] {g : α}
 #align infinite.order_of_eq_zero_of_forall_mem_zpowers Infinite.orderOf_eq_zero_of_forall_mem_zpowers
 #align infinite.add_order_of_eq_zero_of_forall_mem_zmultiples Infinite.addOrderOf_eq_zero_of_forall_mem_zmultiples
 
-@[to_additive Bot.isAddCyclic]
+@[to_additive]
 instance Bot.isCyclic {α : Type u} [Group α] : IsCyclic (⊥ : Subgroup α) :=
   ⟨⟨1, fun x => ⟨0, Subtype.eq <| (zpow_zero (1 : α)).trans <| Eq.symm (Subgroup.mem_bot.1 x.2)⟩⟩⟩
 #align bot.is_cyclic Bot.isCyclic
 #align bot.is_add_cyclic Bot.isAddCyclic
 
-@[to_additive AddSubgroup.isAddCyclic]
+@[to_additive]
 instance Subgroup.isCyclic {α : Type u} [Group α] [IsCyclic α] (H : Subgroup α) : IsCyclic H :=
   haveI := Classical.propDecidable
   let ⟨g, hg⟩ := IsCyclic.exists_generator (α := α)
@@ -538,7 +536,7 @@ section CommGroup
 
 variable [CommGroup α] [IsSimpleGroup α]
 
-@[to_additive IsSimpleAddGroup.isAddCyclic]
+@[to_additive]
 instance (priority := 100) isCyclic : IsCyclic α := by
   cases' subsingleton_or_nontrivial α with hi hi <;> haveI := hi
   · apply isCyclic_of_subsingleton
@@ -583,7 +581,7 @@ end CommGroup
 
 end IsSimpleGroup
 
-@[to_additive AddCommGroup.is_simple_iff_isAddCyclic_and_prime_card]
+@[to_additive]
 theorem CommGroup.is_simple_iff_isCyclic_and_prime_card [Fintype α] [CommGroup α] :
     IsSimpleGroup α ↔ IsCyclic α ∧ (Fintype.card α).Prime := by
   constructor

Mathlib/Tactic/ToAdditive.lean

@@ -732,6 +732,7 @@ def nameDict : String → List String
   | "prehaar"     => ["add", "Prehaar"]
   | "unit"        => ["add", "Unit"]
   | "units"       => ["add", "Units"]
+  | "cyclic"      => ["add", "Cyclic"]
   | "rootable"    => ["divisible"]
   | x             => [x]