awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
⊢ 1 < orderOf g

Tactic:
Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨?_, hα⟩

Premises used: Iff.mpr, And.intro, Nat.one_lt_iff_ne_zero_and_ne_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
h1 : orderOf g ≠ 0
⊢ 1 < orderOf g

Tactic:
refine Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨?_, hα⟩

Premises used: Iff.mpr, And.intro, Nat.one_lt_iff_ne_zero_and_ne_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
h1 : ∀ (h : orderOf g = 0), ∃ (n : ℕ), ¬orderOf g ∣ n ∧ n.gcd (orderOf g) ≠ 1
⊢ orderOf g ≠ 0

Tactic:
contrapose! h
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
hα : orderOf g ≠ 1
h : orderOf g = 0
⊢ ¬orderOf g ∣ 37 ∧ Nat.gcd 37 (orderOf g) ≠ 1

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
hα : orderOf g ≠ 1
h : orderOf g = 0
⊢ ∃ (n : ℕ), ¬orderOf g ∣ n ∧ n.gcd (orderOf g) ≠ 1

Tactic:
exact ⟨37, by simp [h]⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
n : ℕ
hn : n < orderOf g
hn0 : n ≠ 0
⊢ (orderOf g).Coprime n

Tactic:
((h n).resolve_left (Nat.not_dvd_of_pos_of_lt (Nat.pos_iff_ne_zero.mpr hn0) hn)).symm

Premises used: Iff.mpr, Nat.Coprime.symm, Nat.pos_iff_ne_zero, Or.resolve_left, Nat.not_dvd_of_pos_of_lt
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
n : ℕ
hn : n < orderOf g
hn0 : n ≠ 0
⊢ (orderOf g).Coprime n

Tactic:
exact ((h n).resolve_left (Nat.not_dvd_of_pos_of_lt (Nat.pos_iff_ne_zero.mpr hn0) hn)).symm

Premises used: Iff.mpr, Nat.Coprime.symm, Nat.pos_iff_ne_zero, Or.resolve_left, Nat.not_dvd_of_pos_of_lt
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
⊢ Finite α

Tactic:
Nat.finite_of_card_ne_zero prime_card.ne_zero

Premises used: Nat.Prime.ne_zero, IsSimpleGroup.prime_card, Nat.finite_of_card_ne_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : IsMulCommutative α
⊢ IsSimpleGroup α ↔ Nat.Prime (Nat.card α)

Tactic:
⟨fun h ↦ h.prime_card, fun h ↦ isSimpleGroup_of_prime_card (hp := ⟨h⟩) rfl⟩

Premises used: Iff.intro, IsSimpleGroup.prime_card, isSimpleGroup_of_prime_card, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : CommGroup α
⊢ IsSimpleGroup α ↔ Nat.Prime (Nat.card α)

Tactic:
Group.is_simple_iff_prime_card

Premises used: Group.is_simple_iff_prime_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
n : ℤ
⊢ (fun (x : ℤ) ↦ HSMul.hSMul (β := ℤ) x 1) n = n

Tactic:
simp only [smul_eq_mul, mul_one]

Premises used: smul_eq_mul, mul_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
n : ℕ
⊢ IsAddCyclic (ZMod n)

Tactic:
isAddCyclic_of_surjective (Int.castRingHom _) ZMod.intCast_surjective

Premises used: Int.castRingHom, isAddCyclic_of_surjective, ZMod.intCast_surjective
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Nat.Prime (Nat.card (ZMod p))

Tactic:
simpa using hp.out

Premises used: Fact.out
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
A : Type u_4
inst : AddCommGroup A
inst_1 : LinearOrder A
inst_2 : IsOrderedAddMonoid A
inst_3 : Nontrivial A
⊢ IsAddCyclic A ↔ Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ)

Tactic:
⟨?_, fun ⟨e⟩ ↦ e.isAddCyclic.mpr inferInstance⟩

Premises used: Iff.mpr, OrderAddMonoidIso.toAddEquiv, AddEquiv.isAddCyclic, inferInstance, Iff.intro, _private.0.LinearOrderedAddCommGroup.isAddCyclic_iff_nonempty_equiv_int.match_1, IsAddCyclic
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
A : Type u_4
inst : AddCommGroup A
inst_1 : LinearOrder A
inst_2 : IsOrderedAddMonoid A
inst_3 : Nontrivial A
refine : IsAddCyclic A → Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ)
⊢ IsAddCyclic A ↔ Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ)

Tactic:
refine ⟨?_, fun ⟨e⟩ ↦ e.isAddCyclic.mpr inferInstance⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
A : Type u_4
inst : AddCommGroup A
inst_1 : LinearOrder A
inst_2 : IsOrderedAddMonoid A
inst_3 : Nontrivial A
g : A
hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g
obtain : ∀ (a : A) (ha : a ≠ 0), g ≠ 0
⊢ g ≠ 0

Tactic:
obtain ⟨a, ha⟩ := exists_ne (0 : A)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
A : Type u_4
inst : AddCommGroup A
inst_1 : LinearOrder A
inst_2 : IsOrderedAddMonoid A
inst_3 : Nontrivial A
g : A
hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g
a : A
ha : a ≠ 0
obtain : ∀ (m : ℤ) (ha : Ne.{u_4 + 1} (α := A) ((fun (x : ℤ) ↦ x • g) m) 0), g ≠ 0
⊢ g ≠ 0

Tactic:
obtain ⟨m, rfl⟩ := hs a

Premises used: rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
A : Type u_4
inst : AddCommGroup A
inst_1 : LinearOrder A
inst_2 : IsOrderedAddMonoid A
inst_3 : Nontrivial A
g : A
hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g
m : ℤ
ha : Ne.{u_4 + 1} (α := A) ((fun (x : ℤ) ↦ x • g) m) 0
⊢ g ≠ 0

Tactic:
aesop
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
A : Type u_4
inst : AddCommGroup A
inst_1 : LinearOrder A
inst_2 : IsOrderedAddMonoid A
inst_3 : Nontrivial A
g : A
hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g
⊢ g ≠ 0

Tactic:
have h_ne : g ≠ 0 := by
    obtain ⟨a, ha⟩ := exists_ne (0 : A)
    obtain ⟨m, rfl⟩ := hs a
    aesop
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
A : Type u_4
inst : AddCommGroup A
inst_1 : LinearOrder A
inst_2 : IsOrderedAddMonoid A
inst_3 : Nontrivial A
g : A
hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g
h_ne : g ≠ 0
inr :
  ∀
    (this :
      ∀ {A : Type u_4} [inst : AddCommGroup A] [inst_4 : LinearOrder A] [IsOrderedAddMonoid A] [Nontrivial A] (g : A)
        (hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g) (h_ne : g ≠ 0) (hg' : 0 < g),
        Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ))
    (hg' : ¬0 < g), Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ)
wlog :
  ∀ {A : Type u_4} [inst : AddCommGroup A] [inst_4 : LinearOrder A] [IsOrderedAddMonoid A] [Nontrivial A] (g : A)
    (hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g) (h_ne : g ≠ 0) (hg' : 0 < g),
    Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ)
⊢ Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ)

Tactic:
wlog hg' : 0 < g
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
A : Type u_4
inst : AddCommGroup A
inst_1 : LinearOrder A
inst_2 : IsOrderedAddMonoid A
inst_3 : Nontrivial A
g : A
hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g
h_ne : g ≠ 0
this :
  ∀ {A : Type u_4} [inst : AddCommGroup A] [inst_4 : LinearOrder A] [IsOrderedAddMonoid A] [Nontrivial A] (g : A)
    (hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g) (h_ne : g ≠ 0) (hg' : 0 < g),
    Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ)
hg' : ¬0 < g
⊢ Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • -g

Tactic:
simpa using neg_surjective.comp hs

Premises used: neg_surjective, Function.Surjective.comp
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
A : Type u_4
inst : AddCommGroup A
inst_1 : LinearOrder A
inst_2 : IsOrderedAddMonoid A
inst_3 : Nontrivial A
g : A
hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g
h_ne : g ≠ 0
this :
  ∀ {A : Type u_4} [inst : AddCommGroup A] [inst_4 : LinearOrder A] [IsOrderedAddMonoid A] [Nontrivial A] (g : A)
    (hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g) (h_ne : g ≠ 0) (hg' : 0 < g),
    Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ)
hg' : ¬0 < g
⊢ -g ≠ 0

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
A : Type u_4
inst : AddCommGroup A
inst_1 : LinearOrder A
inst_2 : IsOrderedAddMonoid A
inst_3 : Nontrivial A
g : A
hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g
h_ne : g ≠ 0
this :
  ∀ {A : Type u_4} [inst : AddCommGroup A] [inst_4 : LinearOrder A] [IsOrderedAddMonoid A] [Nontrivial A] (g : A)
    (hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g) (h_ne : g ≠ 0) (hg' : 0 < g),
    Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ)
hg' : ¬0 < g
⊢ 0 < -g

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
A : Type u_4
inst : AddCommGroup A
inst_1 : LinearOrder A
inst_2 : IsOrderedAddMonoid A
inst_3 : Nontrivial A
g : A
hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g
h_ne : g ≠ 0
this :
  ∀ {A : Type u_4} [inst : AddCommGroup A] [inst_4 : LinearOrder A] [IsOrderedAddMonoid A] [Nontrivial A] (g : A)
    (hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g) (h_ne : g ≠ 0) (hg' : 0 < g),
    Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ)
hg' : ¬0 < g
⊢ Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ)

Tactic:
exact this (g := -g) (by simpa using neg_surjective.comp hs) (by grind) (by grind)

Premises used: Neg.neg
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
A : Type u_4
inst : AddCommGroup A
inst_1 : LinearOrder A
inst_2 : IsOrderedAddMonoid A
inst_3 : Nontrivial A
g : A
hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g
h_ne : g ≠ 0
hg' : 0 < g
⊢ Function.Injective.{1, u_4 + 1} (β := A) fun (n : ℤ) ↦ n • g

Tactic:
have hi : (fun n : ℤ ↦ n • g).Injective := injective_zsmul_iff_not_isOfFinAddOrder.mpr
      <| not_isOfFinAddOrder_of_isAddTorsionFree h_ne
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
A : Type u_4
inst : AddCommGroup A
inst_1 : LinearOrder A
inst_2 : IsOrderedAddMonoid A
inst_3 : Nontrivial A
g : A
hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g
h_ne : g ≠ 0
hg' : 0 < g
hi : Function.Injective.{1, u_4 + 1} (β := A) fun (n : ℤ) ↦ n • g
⊢ Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ)

Tactic:
⟨.symm { Equiv.ofBijective _ ⟨hi, hs⟩ with
    map_add' := add_zsmul g
    map_le_map_iff' := zsmul_le_zsmul_iff_left hg' }⟩

Premises used: add_zsmul, Nonempty.intro, zsmul_le_zsmul_iff_left, AddEquiv.mk, And.intro, Equiv.ofBijective, HSMul.hSMul, OrderAddMonoidIso.mk, OrderAddMonoidIso.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
A : Type u_4
inst : AddCommGroup A
inst_1 : LinearOrder A
inst_2 : IsOrderedAddMonoid A
inst_3 : Nontrivial A
g : A
hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g
h_ne : g ≠ 0
hg' : 0 < g
hi : Function.Injective.{1, u_4 + 1} (β := A) fun (n : ℤ) ↦ n • g
⊢ Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ)

Tactic:
exact ⟨.symm { Equiv.ofBijective _ ⟨hi, hs⟩ with
    map_add' := add_zsmul g
    map_le_map_iff' := zsmul_le_zsmul_iff_left hg' }⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_4
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
rw : IsAddCyclic.{u_4} (Additive G) ↔ Nonempty.{max 1 (u_4 + 1)} (G ≃*o Multiplicative ℤ)
rw₁ : Nonempty.{u_4 + 1} (Additive G ≃+o ℤ) ↔ Nonempty.{max 1 (u_4 + 1)} (G ≃*o Multiplicative ℤ)
rw₂ rw₃ : Nonempty.{max 1 (u_4 + 1)} (G ≃*o Multiplicative ℤ) ↔ Nonempty.{max 1 (u_4 + 1)} (G ≃*o Multiplicative ℤ)
⊢ IsCyclic G ↔ Nonempty.{max 1 (u_4 + 1)} (G ≃*o Multiplicative ℤ)

Tactic:
rw [← isAddCyclic_additive_iff, LinearOrderedAddCommGroup.isAddCyclic_iff_nonempty_equiv_int,
    OrderAddMonoidIso.toMultiplicativeRight.nonempty_congr]

Premises used: OrderAddMonoidIso.toMultiplicativeRight, Equiv.nonempty_congr, isAddCyclic_additive_iff, LinearOrderedAddCommGroup.isAddCyclic_iff_nonempty_equiv_int
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : IsCyclic α
obtain : ∀ (g : α) (hg : orderOf g = Nat.card α), exponent α = Nat.card α
⊢ exponent α = Nat.card α

Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_ofOrder_eq_natCard (α := α)

Premises used: IsCyclic.exists_ofOrder_eq_natCard
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : IsCyclic α
g : α
hg : orderOf g = Nat.card α
apply : Nat.card α ∣ exponent α
⊢ exponent α = Nat.card α

Tactic:
apply Nat.dvd_antisymm Group.exponent_dvd_nat_card

Premises used: Group.exponent_dvd_nat_card, Nat.dvd_antisymm
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : IsCyclic α
g : α
hg : orderOf g = Nat.card α
rw : orderOf g ∣ exponent α
⊢ Nat.card α ∣ exponent α

Tactic:
rw [← hg]
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : IsCyclic α
g : α
hg : orderOf g = Nat.card α
⊢ orderOf g ∣ exponent α

Tactic:
order_dvd_exponent _

Premises used: Monoid.order_dvd_exponent
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : IsCyclic α
g : α
hg : orderOf g = Nat.card α
⊢ orderOf g ∣ exponent α

Tactic:
exact order_dvd_exponent _

Premises used: Monoid.order_dvd_exponent
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Finite α
h : exponent α = Nat.card α
⊢ IsCyclic α

Tactic:
let ⟨_⟩ := nonempty_fintype α
  let ⟨g, _, hg⟩ := Finset.mem_image.mp (Finset.max'_mem _ _)
  isCyclic_of_orderOf_eq_card g <| hg.trans <| exponent_eq_max'_orderOf.symm.trans h

Premises used: Monoid.exponent_eq_max'_orderOf._proof_1, _private.0.IsCyclic.of_exponent_eq_card.match_1, Finset.univ, Finset.mem_image, Finset.max'_mem, orderOf, nonempty_fintype, Monoid.exponent_eq_max'_orderOf, Exists.intro, Iff.mp, isCyclic_of_orderOf_eq_card, IsCyclic, OfNat.ofNat, Eq.symm, _private.0.IsCyclic.of_exponent_eq_card.match_2, Finset.image, Eq.trans
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Finite α
⊢ IsCyclic α ↔ exponent α = Nat.card α

Tactic:
⟨fun _ => IsCyclic.exponent_eq_card, IsCyclic.of_exponent_eq_card⟩

Premises used: IsCyclic.of_exponent_eq_card, IsCyclic.exponent_eq_card, Iff.intro
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : IsCyclic α
inst_2 : Infinite α
⊢ exponent α = 0

Tactic:
let ⟨_, hg⟩ := IsCyclic.exists_generator (α := α)
  exponent_eq_zero_of_order_zero <| Infinite.orderOf_eq_zero_of_forall_mem_zpowers hg

Premises used: IsCyclic.exists_generator, _private.0.IsCyclic.exponent_eq_zero_of_infinite.match_1, Infinite.orderOf_eq_zero_of_forall_mem_zpowers, Monoid.exponent, OfNat.ofNat, Eq, Monoid.exponent_eq_zero_of_order_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
n : ℕ
rw : Nat.card (ZMod n) = n
rw₁ rw₂ : n = n
⊢ AddMonoid.exponent (ZMod n) = n

Tactic:
rw [IsAddCyclic.exponent_eq_card, Nat.card_zmod]

Premises used: Nat.card_zmod, IsAddCyclic.exponent_eq_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
⊢ Finite α

Tactic:
have : Finite α := Nat.finite_of_card_ne_zero (hα ▸ pow_ne_zero 2 hp.ne_zero)
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this : Finite α
⊢ Nontrivial α

Tactic:
have : Nontrivial α := Finite.one_lt_card_iff_nontrivial.mp
    (hα ▸ one_lt_pow₀ hp.one_lt two_ne_zero)
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this : Nontrivial α
h_exp : exponent α = p
h_cyc : IsCyclic α
inl : ∀ (hp : Nat.Prime 0) (hα : Nat.card α = HPow.hPow (α := ℕ) (β := ℕ) 0 2) (h_exp : exponent α = 0), False
inr : ∀ (hp : Nat.Prime 1) (hα : Nat.card α = HPow.hPow (α := ℕ) (β := ℕ) 1 2) (h_exp : exponent α = 1), False
⊢ False

Tactic:
obtain (rfl | rfl) := eq_zero_or_one_of_sq_eq_self <| hα ▸ h_exp ▸ (h_cyc.exponent_eq_card).symm

Premises used: eq_zero_or_one_of_sq_eq_self, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
this_1 : Finite α
this : Nontrivial α
h_cyc : IsCyclic α
hp : Nat.Prime 0
hα : Nat.card α = HPow.hPow (α := ℕ) (β := ℕ) 0 2
h_exp : exponent α = 0
⊢ False

Tactic:
Nat.not_prime_zero hp

Premises used: Nat.not_prime_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
this_1 : Finite α
this : Nontrivial α
h_cyc : IsCyclic α
hp : Nat.Prime 0
hα : Nat.card α = HPow.hPow (α := ℕ) (β := ℕ) 0 2
h_exp : exponent α = 0
⊢ False

Tactic:
exact Nat.not_prime_zero hp

Premises used: Nat.not_prime_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
this_1 : Finite α
this : Nontrivial α
h_cyc : IsCyclic α
hp : Nat.Prime 1
hα : Nat.card α = HPow.hPow (α := ℕ) (β := ℕ) 1 2
h_exp : exponent α = 1
⊢ False

Tactic:
Nat.not_prime_one hp

Premises used: Nat.not_prime_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
this_1 : Finite α
this : Nontrivial α
h_cyc : IsCyclic α
hp : Nat.Prime 1
hα : Nat.card α = HPow.hPow (α := ℕ) (β := ℕ) 1 2
h_exp : exponent α = 1
⊢ False

Tactic:
exact Nat.not_prime_one hp

Premises used: Nat.not_prime_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this : Nontrivial α
refine : ∀ (h_cyc : ¬IsCyclic α) (g : α) (hg : g ≠ 1), orderOf g = p
⊢ ¬IsCyclic α ↔ exponent α = p

Tactic:
refine ⟨fun h_cyc ↦ (Monoid.exponent_eq_prime_iff hp).mpr fun g hg ↦ ?_, fun h_exp h_cyc ↦ by
    obtain (rfl | rfl) := eq_zero_or_one_of_sq_eq_self <| hα ▸ h_exp ▸ (h_cyc.exponent_eq_card).symm
    · exact Nat.not_prime_zero hp
    · exact Nat.not_prime_one hp⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
⊢ HPow.hPow (β := ℕ) p 2 ≠ 0

Tactic:
aesop
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
⊢ orderOf g ∈ (HPow.hPow (β := ℕ) p 2).divisors

Tactic:
have := (Nat.mem_divisors (m := p ^ 2)).mpr ⟨hα ▸ orderOf_dvd_natCard (x := g), by aesop⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this_2 : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this : orderOf g ∈ (HPow.hPow (β := ℕ) p 2).divisors
⊢ ∃ a < 3, p ^ a = orderOf g

Tactic:
simpa [Nat.divisors_prime_pow hp 2] using this

Premises used: Nat.divisors_prime_pow, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this_2 : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this : orderOf g ∈ (HPow.hPow (β := ℕ) p 2).divisors
⊢ ∃ a < 3, p ^ a = orderOf g

Tactic:
have : ∃ a < 3, p ^ a = orderOf g := by
    simpa [Nat.divisors_prime_pow hp 2] using this
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this_2 : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this_3 : orderOf g ∈ (HPow.hPow (β := ℕ) p 2).divisors
this : ∃ a < 3, p ^ a = orderOf g
⊢ ∃ a < 3, p ^ a = orderOf g

Tactic:
simpa using this
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this_2 : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this_3 : orderOf g ∈ (HPow.hPow (β := ℕ) p 2).divisors
this : ∃ a < 3, p ^ a = orderOf g
obtain : ∀ (a : ℕ) (ha : a < 3) (ha' : p ^ a = orderOf g), orderOf g = p
⊢ orderOf g = p

Tactic:
obtain ⟨a, ha, ha'⟩ := by simpa using this
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this_2 : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this_3 : orderOf g ∈ (HPow.hPow (β := ℕ) p 2).divisors
this : ∃ a < 3, p ^ a = orderOf g
a : ℕ
ha : a < 3
ha' : p ^ a = orderOf g
0 : ∀ (ha : LT.lt (α := ℕ) 0 3) (ha' : HPow.hPow (β := ℕ) p 0 = orderOf g), orderOf g = p
1 : ∀ (ha : LT.lt (α := ℕ) 1 3) (ha' : HPow.hPow (β := ℕ) p 1 = orderOf g), orderOf g = p
2 : ∀ (ha : LT.lt (α := ℕ) 2 3) (ha' : HPow.hPow (β := ℕ) p 2 = orderOf g), orderOf g = p
⊢ orderOf g = p

Tactic:
interval_cases a
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this_2 : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this_3 : orderOf g ∈ (HPow.hPow (β := ℕ) p 2).divisors
this : ∃ a < 3, p ^ a = orderOf g
a : ℕ
ha : LT.lt (α := ℕ) 0 3
ha' : HPow.hPow (β := ℕ) p 0 = orderOf g
⊢ orderOf g = 1

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this_2 : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this_3 : orderOf g ∈ (HPow.hPow (β := ℕ) p 2).divisors
this : ∃ a < 3, p ^ a = orderOf g
a : ℕ
ha : LT.lt (α := ℕ) 0 3
ha' : HPow.hPow (β := ℕ) p 0 = orderOf g
⊢ orderOf g = p

Tactic:
exact False.elim <| hg <| orderOf_eq_one_iff.mp <| by simp_all

Premises used: False.elim, Iff.mp, orderOf_eq_one_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this_2 : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this_3 : orderOf g ∈ (HPow.hPow (β := ℕ) p 2).divisors
this : ∃ a < 3, p ^ a = orderOf g
a : ℕ
ha : LT.lt (α := ℕ) 1 3
ha' : HPow.hPow (β := ℕ) p 1 = orderOf g
⊢ orderOf g = p

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this_2 : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this_3 : orderOf g ∈ (HPow.hPow (β := ℕ) p 2).divisors
this : ∃ a < 3, p ^ a = orderOf g
a : ℕ
ha : LT.lt (α := ℕ) 2 3
ha' : HPow.hPow (β := ℕ) p 2 = orderOf g
⊢ orderOf g = Nat.card α

Tactic:
lia
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this_2 : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this_3 : orderOf g ∈ (HPow.hPow (β := ℕ) p 2).divisors
this : ∃ a < 3, p ^ a = orderOf g
a : ℕ
ha : LT.lt (α := ℕ) 2 3
ha' : HPow.hPow (β := ℕ) p 2 = orderOf g
⊢ orderOf g = p

Tactic:
exact False.elim <| h_cyc <| isCyclic_of_orderOf_eq_card g <| by lia

Premises used: False.elim, isCyclic_of_orderOf_eq_card