awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h_1 : Nontrivial α
a b : α
hab : a ≠ b
habG : swap a b ∉ G
g_1 g : Perm α
x y : α
hxy : x ≠ y
ih : g ∈ G ↔ g ∈ alternatingGroup α
h : (swap x y ∈ G ↔ g ∈ alternatingGroup α) ↔ (swap x y ∈ alternatingGroup α ↔ g ∈ alternatingGroup α)
⊢ swap x y * g ∈ G ↔ swap x y * g ∈ alternatingGroup α

Tactic:
rw [mul_mem_iff_of_index_two hG, mul_mem_iff_of_index_two alternatingGroup.index_eq_two, ih]

Premises used: Subgroup.mul_mem_iff_of_index_two, alternatingGroup.index_eq_two
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h_1 : Nontrivial α
a b : α
hab : a ≠ b
habG : swap a b ∉ G
g_1 g : Perm α
x y : α
hxy : x ≠ y
ih : g ∈ G ↔ g ∈ alternatingGroup α
h : swap x y ∉ G
⊢ (swap x y ∈ G ↔ g ∈ alternatingGroup α) ↔ (swap x y ∈ alternatingGroup α ↔ g ∈ alternatingGroup α)

Tactic:
refine iff_congr (iff_of_false ?_ (by cases (sign_swap hxy).symm.trans ·)) Iff.rfl

Premises used: iff_congr, Iff.rfl, iff_of_false
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h_1 : Nontrivial α
a b : α
hab : a ≠ b
habG : swap a b ∉ G
g_1 g : Perm α
x y : α
hxy : x ≠ y
ih : g ∈ G ↔ g ∈ alternatingGroup α
h : ∀ (habG : swap x y ∈ G), swap a b ∈ G
⊢ swap x y ∉ G

Tactic:
contrapose habG
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h_1 : Nontrivial α
a b : α
hab : a ≠ b
g_1 g : Perm α
x y : α
hxy : x ≠ y
ih : g ∈ G ↔ g ∈ alternatingGroup α
habG : swap x y ∈ G
h :
  Exists.choose (p := fun (c : Perm α) ↦ c * swap x y * c⁻¹ = swap a b) ⋯ * swap x y *
      (Exists.choose (p := fun (c : Perm α) ↦ c * swap x y * c⁻¹ = swap a b) ⋯)⁻¹ ∈
    G
⊢ swap a b ∈ G

Tactic:
rw [← (isConj_iff.mp <| isConj_swap hxy hab).choose_spec]

Premises used: isConj_iff, Exists.choose_spec, Equiv.Perm.isConj_swap, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h : Nontrivial α
a b : α
hab : a ≠ b
g_1 g : Perm α
x y : α
hxy : x ≠ y
ih : g ∈ G ↔ g ∈ alternatingGroup α
habG : swap x y ∈ G
⊢ Exists.choose (p := fun (c : Perm α) ↦ c * swap x y * c⁻¹ = swap a b) ⋯ * swap x y *
      (Exists.choose (p := fun (c : Perm α) ↦ c * swap x y * c⁻¹ = swap a b) ⋯)⁻¹ ∈
    G

Tactic:
(normal_of_index_eq_two hG).conj_mem _ habG _

Premises used: Subgroup.normal_of_index_eq_two, Subgroup.Normal.conj_mem
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h : Nontrivial α
a b : α
hab : a ≠ b
g_1 g : Perm α
x y : α
hxy : x ≠ y
ih : g ∈ G ↔ g ∈ alternatingGroup α
habG : swap x y ∈ G
⊢ Exists.choose (p := fun (c : Perm α) ↦ c * swap x y * c⁻¹ = swap a b) ⋯ * swap x y *
      (Exists.choose (p := fun (c : Perm α) ↦ c * swap x y * c⁻¹ = swap a b) ⋯)⁻¹ ∈
    G

Tactic:
exact (normal_of_index_eq_two hG).conj_mem _ habG _

Premises used: Subgroup.normal_of_index_eq_two, Subgroup.Normal.conj_mem
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
inl : ∀ (h : G.index = 0), alternatingGroup α ≤ G
inr : ∀ (h : G.index > 0), alternatingGroup α ≤ G
⊢ alternatingGroup α ≤ G

Tactic:
rcases G.index.eq_zero_or_pos with h | h

Premises used: Subgroup.index, Nat.eq_zero_or_pos
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h : G.index = 0
⊢ alternatingGroup α ≤ G

Tactic:
(index_ne_zero_of_finite h).elim

Premises used: Subgroup.index_ne_zero_of_finite, False.elim
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h : G.index = 0
⊢ alternatingGroup α ≤ G

Tactic:
exact (index_ne_zero_of_finite h).elim

Premises used: Subgroup.index_ne_zero_of_finite, False.elim
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h : G.index > 0
inr : ∀ (h : G.index = Nat.succ 0), alternatingGroup α ≤ G
inr₁ : ∀ (h : Nat.succ 0 < G.index), alternatingGroup α ≤ G
⊢ alternatingGroup α ≤ G

Tactic:
rcases (Nat.succ_le_iff.mpr h).eq_or_lt' with h | h

Premises used: Iff.mpr, LE.le.eq_or_lt', Nat.succ_le_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h_1 : G.index > 0
h : G.index = Nat.succ 0
⊢ alternatingGroup α ≤ G

Tactic:
index_eq_one.mp h ▸ le_top

Premises used: Eq.rec, le_top, Iff.mp, Subgroup.index_eq_one, Eq.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h_1 : G.index > 0
h : G.index = Nat.succ 0
⊢ alternatingGroup α ≤ G

Tactic:
exact index_eq_one.mp h ▸ le_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h_1 : G.index > 0
h : Nat.succ 0 < G.index
inr inr₁ : alternatingGroup α ≤ alternatingGroup α
⊢ alternatingGroup α ≤ G

Tactic:
rw [eq_alternatingGroup_of_index_eq_two (hG.antisymm h)]

Premises used: Equiv.Perm.eq_alternatingGroup_of_index_eq_two, LE.le.antisymm
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
φ : Perm α ≃* Perm α
⊢ Nontrivial α

Tactic:
nontriviality α
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
φ : Perm α ≃* Perm α
h : Nontrivial α
hG : (comap φ.toMonoidHom (alternatingGroup α)).index = 2
⊢ comap φ.toMonoidHom (alternatingGroup α) = alternatingGroup α

Tactic:
apply eq_alternatingGroup_of_index_eq_two

Premises used: Equiv.Perm.eq_alternatingGroup_of_index_eq_two
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
φ : Perm α ≃* Perm α
h : Nontrivial α
hG : (alternatingGroup α).index = 2
hG₁ hG₂ : Eq (α := ℕ) 2 2
⊢ (comap φ.toMonoidHom (alternatingGroup α)).index = 2

Tactic:
rw [index_comap_of_surjective _ (Equiv.surjective _), alternatingGroup.index_eq_two]

Premises used: Subgroup.index_comap_of_surjective, alternatingGroup.index_eq_two
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : IsCyclic α
⊢ ∃ (g : α), ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x

Tactic:
exists_zpow_surjective α

Premises used: Set.Mem, setOf, exists_zpow_surjective, Set.range, Function.Surjective
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
simp : IsCyclic α ↔ ∃ (g : α), ∀ (x : α), ∃ (k : ℤ), g ^ k = x
⊢ IsCyclic α ↔ ∃ (g : α), Eq (α := Subgroup α) (zpowers g) ⊤

Tactic:
simp only [eq_top_iff', mem_zpowers_iff]

Premises used: Subgroup.eq_top_iff', Subgroup.mem_zpowers_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
⊢ IsCyclic α ↔ ∃ (g : α), ∀ (x : α), ∃ (k : ℤ), g ^ k = x

Tactic:
⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

Premises used: _private.0.isCyclic_iff_exists_zpowers_eq_top.match_2, Exists, Iff.intro, IsCyclic.mk
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
⊢ IsCyclic α ↔ ∃ (g : α), ∀ (x : α), ∃ (k : ℤ), g ^ k = x

Tactic:
exact ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
H : Subgroup α
rw : (∃ (g : ↥H), Eq (α := Subgroup ↥H) (zpowers g) ⊤) ↔ ∃ (g : α), zpowers g = H
⊢ IsCyclic.{u_1} ↥H ↔ ∃ (g : α), zpowers g = H

Tactic:
rw [isCyclic_iff_exists_zpowers_eq_top]

Premises used: isCyclic_iff_exists_zpowers_eq_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
H : Subgroup α
simp_rw : (∃ a ∈ H, zpowers a = H) ↔ ∃ (g : α), zpowers g = H
⊢ (∃ (g : ↥H), Eq (α := Subgroup ↥H) (zpowers g) ⊤) ↔ ∃ (g : α), zpowers g = H

Tactic:
simp_rw [← map_subtype_inj, ← MonoidHom.range_eq_map,
    H.range_subtype, MonoidHom.map_zpowers, Subtype.exists, coe_subtype, exists_prop]

Premises used: Subgroup.map_subtype_inj, MonoidHom.range_eq_map, Subgroup.coe_subtype, Subtype.exists, exists_prop, MonoidHom.map_zpowers, Subgroup.range_subtype
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
H : Subgroup α
⊢ (∃ a ∈ H, zpowers a = H) ↔ ∃ (g : α), zpowers g = H

Tactic:
exists_congr fun g ↦ and_iff_right_of_imp fun h ↦ h ▸ mem_zpowers g

Premises used: Eq.rec, Subgroup.mem_zpowers, exists_congr, and_iff_right_of_imp
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
H : Subgroup α
⊢ (∃ a ∈ H, zpowers a = H) ↔ ∃ (g : α), zpowers g = H

Tactic:
exact exists_congr fun g ↦ and_iff_right_of_imp fun h ↦ h ▸ mem_zpowers g

Premises used: exists_congr, and_iff_right_of_imp
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group G
g : G
⊢ IsCyclic.{u_2} ↥(zpowers g)

Tactic:
(Subgroup.isCyclic_iff_exists_zpowers_eq_top _).mpr ⟨g, rfl⟩

Premises used: Iff.mpr, Exists.intro, Subgroup.isCyclic_iff_exists_zpowers_eq_top, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group α
inst_1 : Subsingleton α
⊢ IsCyclic α

Tactic:
⟨⟨1, fun _ => ⟨0, Subsingleton.elim _ _⟩⟩⟩

Premises used: HPow.hPow, Exists.intro, IsCyclic.mk, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : SubNegMonoid α
⊢ IsCyclic.{u_1} (Multiplicative α) ↔ IsAddCyclic α

Tactic:
⟨fun H ↦ ⟨H.1⟩, fun H ↦ ⟨H.1⟩⟩

Premises used: IsAddCyclic.mk, IsAddCyclic.exists_zsmul_surjective, Iff.intro, IsCyclic.exists_zpow_surjective, IsCyclic.mk
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : AddGroup α
inst_1 : IsAddCyclic α
⊢ IsCyclic.{u_1} (Multiplicative α)

Tactic:
isCyclic_multiplicative_iff.mpr inferInstance

Premises used: Iff.mpr, inferInstance, isCyclic_multiplicative_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : DivInvMonoid α
⊢ IsAddCyclic.{u_1} (Additive α) ↔ IsCyclic α

Tactic:
⟨fun H ↦ ⟨H.1⟩, fun H ↦ ⟨H.1⟩⟩

Premises used: IsAddCyclic.mk, IsAddCyclic.exists_zsmul_surjective, Iff.intro, IsCyclic.exists_zpow_surjective, IsCyclic.mk
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group α
inst_1 : IsCyclic α
⊢ IsAddCyclic.{u_1} (Additive α)

Tactic:
isAddCyclic_additive_iff.mpr inferInstance

Premises used: Iff.mpr, inferInstance, isAddCyclic_additive_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
nc : ¬IsCyclic α
contrapose! : ∀ (nc : Subsingleton α), IsCyclic α
⊢ Nontrivial α

Tactic:
contrapose! nc
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
nc : Subsingleton α
⊢ IsCyclic α

Tactic:
isCyclic_of_subsingleton

Premises used: isCyclic_of_subsingleton
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
nc : Subsingleton α
⊢ IsCyclic α

Tactic:
exact isCyclic_of_subsingleton

Premises used: isCyclic_of_subsingleton
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
h : IsCyclic G
σ : G →* G
obtain :
  ∀ (h : G) (hG : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers h) x),
    ∃ (m : ℤ), ∀ (g : G), (σ : (a : G) → G) g = g ^ m
⊢ ∃ (m : ℤ), ∀ (g : G), (σ : (a : G) → G) g = g ^ m

Tactic:
obtain ⟨h, hG⟩ := IsCyclic.exists_generator (α := G)

Premises used: IsCyclic.exists_generator
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
h_1 : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers h) x
obtain :
  ∀ (m : ℤ) (hm : Eq (α := G) ((fun (x : ℤ) ↦ h ^ x) m : G) ((σ : (a : G) → G) h : G)),
    ∃ (m : ℤ), ∀ (g : G), (σ : (a : G) → G) g = g ^ m
⊢ ∃ (m : ℤ), ∀ (g : G), (σ : (a : G) → G) g = g ^ m

Tactic:
obtain ⟨m, hm⟩ := hG (σ h)

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
h_1 : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers h) x
m : ℤ
hm : Eq (α := G) ((fun (x : ℤ) ↦ h ^ x) m : G) ((σ : (a : G) → G) h : G)
⊢ ∃ (m : ℤ), ∀ (g : G), (σ : (a : G) → G) g = g ^ m

Tactic:
⟨m, fun g => ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
h_1 : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers h) x
m : ℤ
hm : Eq (α := G) ((fun (x : ℤ) ↦ h ^ x) m : G) ((σ : (a : G) → G) h : G)
refine : ∀ (g : G), (σ : (a : G) → G) g = g ^ m
⊢ ∃ (m : ℤ), ∀ (g : G), (σ : (a : G) → G) g = g ^ m

Tactic:
refine ⟨m, fun g => ?_⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
h_1 : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers h) x
m : ℤ
hm : Eq (α := G) ((fun (x : ℤ) ↦ h ^ x) m : G) ((σ : (a : G) → G) h : G)
g : G
obtain : ∀ (n : ℤ), (σ : (a : G) → G) ((fun (x : ℤ) ↦ h ^ x) n) = HPow.hPow (α := G) ((fun (x : ℤ) ↦ h ^ x) n) m
⊢ (σ : (a : G) → G) g = g ^ m

Tactic:
obtain ⟨n, rfl⟩ := hG g

Premises used: rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
h_1 : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers h) x
m : ℤ
hm : Eq (α := G) ((fun (x : ℤ) ↦ h ^ x) m : G) ((σ : (a : G) → G) h : G)
n : ℤ
rw : HPow.hPow (α := G) ((σ : (a : G) → G) h : G) n = HPow.hPow (α := G) ((fun (x : ℤ) ↦ h ^ x) n) m
rw₁ : HPow.hPow (α := G) ((fun (x : ℤ) ↦ h ^ x) m) n = HPow.hPow (α := G) ((fun (x : ℤ) ↦ h ^ x) n) m
rw₂ : h ^ (m * n) = HPow.hPow (α := G) ((fun (x : ℤ) ↦ h ^ x) n) m
rw₃ rw₄ : h ^ (m * n) = h ^ (m * n)
⊢ (σ : (a : G) → G) ((fun (x : ℤ) ↦ h ^ x) n) = HPow.hPow (α := G) ((fun (x : ℤ) ↦ h ^ x) n) m

Tactic:
rw [map_zpow, ← hm, ← zpow_mul, ← zpow_mul']

Premises used: zpow_mul', zpow_mul, map_zpow
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : Finite α
simp_rw : (∃ (g : α), Eq (α := Subgroup α) (zpowers g) ⊤) ↔ ∃ (g : α), orderOf g = Nat.card α
simp_rw₁ : (∃ (g : α), Nat.card.{u_1} ↥(zpowers g) = Nat.card α) ↔ ∃ (g : α), orderOf g = Nat.card α
⊢ IsCyclic α ↔ ∃ (g : α), orderOf g = Nat.card α

Tactic:
simp_rw [isCyclic_iff_exists_zpowers_eq_top, ← card_eq_iff_eq_top, Nat.card_zpowers]

Premises used: isCyclic_iff_exists_zpowers_eq_top, Nat.card_zpowers, Subgroup.card_eq_iff_eq_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : Finite α
rw : (∃ (g : α), orderOf g = Nat.card α) ↔ ∃ (g : α), Nat.card α ≤ orderOf g
⊢ IsCyclic α ↔ ∃ (g : α), Nat.card α ≤ orderOf g

Tactic:
rw [isCyclic_iff_exists_orderOf_eq_natCard]

Premises used: isCyclic_iff_exists_orderOf_eq_natCard
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : Finite α
h : ∀ (a : α), orderOf a = Nat.card α ↔ Nat.card α ≤ orderOf a
⊢ (∃ (g : α), orderOf g = Nat.card α) ↔ ∃ (g : α), Nat.card α ≤ orderOf g

Tactic:
apply exists_congr

Premises used: exists_congr
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : Finite α
g : α
⊢ orderOf g = Nat.card α ↔ Nat.card α ≤ orderOf g

Tactic:
⟨Eq.ge, le_antisymm orderOf_le_card⟩

Premises used: Eq.ge, orderOf_le_card, le_antisymm, Iff.intro
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : Finite α
g : α
⊢ orderOf g = Nat.card α ↔ Nat.card α ≤ orderOf g

Tactic:
exact ⟨Eq.ge, le_antisymm orderOf_le_card⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : Finite α
x : α
hx : orderOf x = Nat.card α
⊢ IsCyclic α

Tactic:
isCyclic_iff_exists_orderOf_eq_natCard.mpr ⟨x, hx⟩

Premises used: Iff.mpr, isCyclic_iff_exists_orderOf_eq_natCard, Exists.intro
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : Finite α
x : α
hx : Nat.card α ≤ orderOf x
⊢ IsCyclic α

Tactic:
isCyclic_iff_exists_natCard_le_orderOf.mpr ⟨x, hx⟩

Premises used: Iff.mpr, isCyclic_iff_exists_natCard_le_orderOf, Exists.intro
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
hp : Fact (Nat.Prime (Nat.card G))
⊢ Finite G

Tactic:
have : Finite G := Nat.finite_of_card_ne_zero hp.1.ne_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
hp : Fact (Nat.Prime (Nat.card G))
this : Finite G
⊢ Nat.card.{u_2} ↥H ∣ Nat.card G

Tactic:
have := card_subgroup_dvd_card H
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
hp : Fact (Nat.Prime (Nat.card G))
this_1 : Finite G
this : Nat.card.{u_2} ↥H ∣ Nat.card G
rwa : ∀ (this : Nat.card.{u_2} ↥H = 1 ∨ Nat.card.{u_2} ↥H = Nat.card G), H = ⊥ ∨ H = ⊤
rwa₁ : ∀ (this : H = ⊥ ∨ Nat.card.{u_2} ↥H = Nat.card G), H = ⊥ ∨ H = ⊤
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (this : H = ⊥ ∨ H = ⊤), H = ⊥ ∨ H = ⊤
⊢ H = ⊥ ∨ H = ⊤

Tactic:
rwa [Nat.dvd_prime hp.1, ← eq_bot_iff_card, card_eq_iff_eq_top] at this

Premises used: Subgroup.eq_bot_iff_card, Nat.dvd_prime, Fact.out, Subgroup.card_eq_iff_eq_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g : G
hg : g ≠ 1
⊢ Fact (Nat.Prime (Nat.card G))

Tactic:
subst h
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
g : G
hg : g ≠ 1
hp : Fact (Nat.Prime (Nat.card G))
⊢ Eq (α := Subgroup G) (zpowers g) ⊥ ∨ Eq (α := Subgroup G) (zpowers g) ⊤

Tactic:
have := (zpowers g).eq_bot_or_eq_top_of_prime_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
g : G
hg : g ≠ 1
hp : Fact (Nat.Prime (Nat.card G))
this : Eq (α := Subgroup G) (zpowers g) ⊥ ∨ Eq (α := Subgroup G) (zpowers g) ⊤
rwa : ∀ (this : g = 1 ∨ Eq (α := Subgroup G) (zpowers g) ⊤), Eq (α := Subgroup G) (zpowers g) ⊤
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : Eq (α := Subgroup G) (zpowers g) ⊤), Eq (α := Subgroup G) (zpowers g) ⊤
⊢ Eq (α := Subgroup G) (zpowers g) ⊤

Tactic:
rwa [zpowers_eq_bot, or_iff_right hg] at this

Premises used: Subgroup.zpowers_eq_bot, or_iff_right
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g g' : G
hg : g ≠ 1
simp_rw : Membership.mem (γ := Subgroup G) ⊤ g'
⊢ Membership.mem (γ := Subgroup G) (zpowers g) g'

Tactic:
simp_rw [zpowers_eq_top_of_prime_card h hg, Subgroup.mem_top]

Premises used: zpowers_eq_top_of_prime_card, Subgroup.mem_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g g' : G
hg : g ≠ 1
⊢ Finite G

Tactic:
have : Finite G := Nat.finite_of_card_ne_zero (h ▸ hp.1.ne_zero)
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g g' : G
hg : g ≠ 1
this : Finite G
rw : Membership.mem (γ := Subgroup G) (zpowers g) g'
⊢ Membership.mem (γ := Submonoid G) (Submonoid.powers g) g'

Tactic:
rw [mem_powers_iff_mem_zpowers]

Premises used: mem_powers_iff_mem_zpowers
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g g' : G
hg : g ≠ 1
this : Finite G
⊢ Membership.mem (γ := Subgroup G) (zpowers g) g'

Tactic:
mem_zpowers_of_prime_card h hg

Premises used: mem_zpowers_of_prime_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g g' : G
hg : g ≠ 1
this : Finite G
⊢ Membership.mem (γ := Subgroup G) (zpowers g) g'

Tactic:
exact mem_zpowers_of_prime_card h hg

Premises used: mem_zpowers_of_prime_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g : G
hg : g ≠ 1
h₁ : ∀ (x : G), Membership.mem (γ := Submonoid G) (Submonoid.powers g) x ↔ Membership.mem (γ := Submonoid G) ⊤ x
⊢ Eq (α := Submonoid G) (Submonoid.powers g) ⊤

Tactic:
ext x
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g : G
hg : g ≠ 1
x : G
⊢ Membership.mem (γ := Submonoid G) (Submonoid.powers g) x ↔ Membership.mem (γ := Submonoid G) ⊤ x

Tactic:
simp [mem_powers_of_prime_card h hg]

Premises used: mem_powers_of_prime_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
⊢ Finite α

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

Tactic:
have : Nontrivial α := Finite.one_lt_card_iff_nontrivial.mp (h ▸ hp.1.one_lt)
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
this_1 : Finite α
this : Nontrivial α
⊢ ∃ (g : α), g ≠ 1

Tactic:
exists_ne 1

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
this_1 : Finite α
this : Nontrivial α
obtain : ∀ (g : α) (hg : g ≠ 1), IsCyclic α
⊢ IsCyclic α

Tactic:
obtain ⟨g, hg⟩ : ∃ g : α, g ≠ 1 := exists_ne 1

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
this_1 : Finite α
this : Nontrivial α
g : α
hg : g ≠ 1
⊢ IsCyclic α

Tactic:
⟨g, fun g' ↦ mem_zpowers_of_prime_card h hg⟩

Premises used: mem_zpowers_of_prime_card, Exists.intro, IsCyclic.mk
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
this_1 : Finite α
this : Nontrivial α
g : α
hg : g ≠ 1
⊢ IsCyclic α

Tactic:
exact ⟨g, fun g' ↦ mem_zpowers_of_prime_card h hg⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α ∣ p
inl : ∀ (h : Nat.card α = 1), IsCyclic α
inr : ∀ (h : Nat.card α = p), IsCyclic α
⊢ IsCyclic α

Tactic:
rcases (Nat.dvd_prime hp.out).mp h with h | h

Premises used: Nat.dvd_prime, Iff.mp, Fact.out
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h_1 : Nat.card α ∣ p
h : Nat.card α = 1
⊢ IsCyclic α

Tactic:
@isCyclic_of_subsingleton α _ (Nat.card_eq_one_iff_unique.mp h).1

Premises used: isCyclic_of_subsingleton
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h_1 : Nat.card α ∣ p
h : Nat.card α = 1
⊢ IsCyclic α

Tactic:
exact @isCyclic_of_subsingleton α _ (Nat.card_eq_one_iff_unique.mp h).1

Premises used: isCyclic_of_subsingleton
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h_1 : Nat.card α ∣ p
h : Nat.card α = p
⊢ IsCyclic α

Tactic:
isCyclic_of_prime_card h

Premises used: isCyclic_of_prime_card