awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h : Nontrivial α
a b : α
hab : a ≠ b
habG : swap a b ∉ G
g : Perm α
⊢ g ∈ G ↔ g ∈ alternatingGroup α
have h : ∀ (g : Perm α) (x y : α) (hxy : x ≠ y) (ih : g ∈ G ↔ g ∈ alternatingGroup α),
  swap x y * g ∈ G ↔ swap x y * g ∈ alternatingGroup α
Tactic: refine swap_induction_on g (iff_of_true G.one_mem <| map_one _) fun g x y hxy ih ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h : 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 α
⊢ swap x y * g ∈ G ↔ swap x y * g ∈ alternatingGroup α
have h : (swap x y ∈ G ↔ g ∈ alternatingGroup α) ↔ (swap x y ∈ alternatingGroup α ↔ g ∈ alternatingGroup α)
Tactic: rw [mul_mem_iff_of_index_two hG, mul_mem_iff_of_index_two alternatingGroup.index_eq_two, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h : 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 α
⊢ (swap x y ∈ G ↔ g ∈ alternatingGroup α) ↔ (swap x y ∈ alternatingGroup α ↔ g ∈ alternatingGroup α)
have h : swap x y ∉ G
Tactic: refine iff_congr (iff_of_false ?_ (by cases (sign_swap hxy).symm.trans ·)) Iff.rfl
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h : 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 α
⊢ swap x y ∉ G
have h : ∀ (habG : swap x y ∈ G), swap a b ∈ G
Tactic: contrapose habG
Cleared hypotheses: habG
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
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
⊢ swap a b ∈ G
have h : Exists.choose (p := fun (c : Perm α) ↦ c * swap x y * c⁻¹ = swap a b) sorry * swap x y *
    (Exists.choose (p := fun (c : Perm α) ↦ c * swap x y * c⁻¹ = swap a b) sorry)⁻¹ ∈
  G
Tactic: rw [← (isConj_iff.mp <| isConj_swap hxy hab).choose_spec]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
⊢ alternatingGroup α ≤ G
have inl : ∀ (h : G.index = 0), alternatingGroup α ≤ G
Tactic: rcases G.index.eq_zero_or_pos with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
inl : ∀ (h : G.index = 0), alternatingGroup α ≤ G
⊢ alternatingGroup α ≤ G
have inr : ∀ (h : G.index > 0), alternatingGroup α ≤ G
Tactic: rcases G.index.eq_zero_or_pos with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h : G.index > 0
⊢ alternatingGroup α ≤ G
have inr : ∀ (h : G.index = Nat.succ 0), alternatingGroup α ≤ G
Tactic: rcases (Nat.succ_le_iff.mpr h).eq_or_lt' with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
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
⊢ alternatingGroup α ≤ G
have inr₁ : ∀ (h : Nat.succ 0 < G.index), alternatingGroup α ≤ G
Tactic: rcases (Nat.succ_le_iff.mpr h).eq_or_lt' with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
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
⊢ alternatingGroup α ≤ G
have inr : alternatingGroup α ≤ alternatingGroup α
Tactic: rw [eq_alternatingGroup_of_index_eq_two (hG.antisymm h)]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
φ : Perm α ≃* Perm α
⊢ comap φ.toMonoidHom (alternatingGroup α) = alternatingGroup α
have a : Nontrivial α
Tactic: nontriviality α
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
φ : Perm α ≃* Perm α
h : Nontrivial α
⊢ comap φ.toMonoidHom (alternatingGroup α) = alternatingGroup α
have hG : (comap φ.toMonoidHom (alternatingGroup α)).index = 2
Tactic: apply eq_alternatingGroup_of_index_eq_two
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
φ : Perm α ≃* Perm α
h : Nontrivial α
⊢ (comap φ.toMonoidHom (alternatingGroup α)).index = 2
have hG : (alternatingGroup α).index = 2
Tactic: rw [index_comap_of_surjective _ (Equiv.surjective _), alternatingGroup.index_eq_two]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
φ : Perm α ≃* Perm α
h : Nontrivial α
hG : (alternatingGroup α).index = 2
⊢ (comap φ.toMonoidHom (alternatingGroup α)).index = 2
have hG₁ : Eq (α := ℕ) 2 2
Tactic: rw [index_comap_of_surjective _ (Equiv.surjective _), alternatingGroup.index_eq_two]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
inst : Group α
⊢ IsCyclic α ↔ ∃ (g : α), Eq (α := Subgroup α) (zpowers g) ⊤
have simp : IsCyclic α ↔ ∃ (g : α), ∀ (x : α), ∃ (k : ℤ), g ^ k = x
Tactic: simp only [eq_top_iff', mem_zpowers_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
inst : Group α
H : Subgroup α
⊢ IsCyclic.{u_1} ↥H ↔ ∃ (g : α), zpowers g = H
have rw : (∃ (g : ↥H), Eq (α := Subgroup ↥H) (zpowers g) ⊤) ↔ ∃ (g : α), zpowers g = H
Tactic: rw [isCyclic_iff_exists_zpowers_eq_top]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
inst : Group α
H : Subgroup α
⊢ (∃ (g : ↥H), Eq (α := Subgroup ↥H) (zpowers g) ⊤) ↔ ∃ (g : α), zpowers g = H
have simp_rw : (∃ a ∈ H, zpowers a = H) ↔ ∃ (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]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
inst : Group α
nc : ¬IsCyclic α
⊢ Nontrivial α
have contrapose! : ∀ (nc : Subsingleton α), IsCyclic α
Tactic: contrapose! nc
Cleared hypotheses: nc
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
G : Type u_2
inst : Group G
h : IsCyclic G
σ : G →* G
⊢ ∃ (m : ℤ), ∀ (g : G), (σ : (a : G) → G) g = g ^ m
have obtain : ∀ (h : G) (hG : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers h) x),
  ∃ (m : ℤ), ∀ (g : G), (σ : (a : G) → G) g = g ^ m
Tactic: obtain ⟨h, hG⟩ := IsCyclic.exists_generator (α := G)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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 : ℤ), ∀ (g : G), (σ : (a : G) → G) g = g ^ m
have 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
Tactic: obtain ⟨m, hm⟩ := hG (σ h)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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
have refine : ∀ (g : G), (σ : (a : G) → G) g = g ^ m
Tactic: refine ⟨m, fun g => ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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
⊢ (σ : (a : G) → G) g = g ^ m
have obtain : ∀ (n : ℤ), (σ : (a : G) → G) ((fun (x : ℤ) ↦ h ^ x) n) = HPow.hPow (α := G) ((fun (x : ℤ) ↦ h ^ x) n) m
Tactic: obtain ⟨n, rfl⟩ := hG g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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 : ℤ
⊢ (σ : (a : G) → G) ((fun (x : ℤ) ↦ h ^ x) n) = HPow.hPow (α := G) ((fun (x : ℤ) ↦ h ^ x) n) m
have rw : HPow.hPow (α := G) ((σ : (a : G) → G) h : G) n = HPow.hPow (α := G) ((fun (x : ℤ) ↦ h ^ x) n) m
Tactic: rw [map_zpow, ← hm, ← zpow_mul, ← zpow_mul']
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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
⊢ (σ : (a : G) → G) ((fun (x : ℤ) ↦ h ^ x) n) = HPow.hPow (α := G) ((fun (x : ℤ) ↦ h ^ x) n) m
have rw₁ : HPow.hPow (α := G) ((fun (x : ℤ) ↦ h ^ x) m) n = HPow.hPow (α := G) ((fun (x : ℤ) ↦ h ^ x) n) m
Tactic: rw [map_zpow, ← hm, ← zpow_mul, ← zpow_mul']
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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
⊢ (σ : (a : G) → G) ((fun (x : ℤ) ↦ h ^ x) n) = HPow.hPow (α := G) ((fun (x : ℤ) ↦ h ^ x) n) m
have rw₂ : h ^ (m * n) = HPow.hPow (α := G) ((fun (x : ℤ) ↦ h ^ x) n) m
Tactic: rw [map_zpow, ← hm, ← zpow_mul, ← zpow_mul']
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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
⊢ (σ : (a : G) → G) ((fun (x : ℤ) ↦ h ^ x) n) = HPow.hPow (α := G) ((fun (x : ℤ) ↦ h ^ x) n) m
have rw₃ : h ^ (m * n) = h ^ (m * n)
Tactic: rw [map_zpow, ← hm, ← zpow_mul, ← zpow_mul']
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : Finite α
⊢ IsCyclic α ↔ ∃ (g : α), orderOf g = Nat.card α
have simp_rw : (∃ (g : α), Eq (α := Subgroup α) (zpowers g) ⊤) ↔ ∃ (g : α), orderOf g = Nat.card α
Tactic: simp_rw [isCyclic_iff_exists_zpowers_eq_top, ← card_eq_iff_eq_top, Nat.card_zpowers]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : Finite α
simp_rw : (∃ (g : α), Eq (α := Subgroup α) (zpowers g) ⊤) ↔ ∃ (g : α), orderOf g = Nat.card α
⊢ IsCyclic α ↔ ∃ (g : α), orderOf g = Nat.card α
have simp_rw₁ : (∃ (g : α), Nat.card.{u_1} ↥(zpowers g) = Nat.card α) ↔ ∃ (g : α), orderOf g = Nat.card α
Tactic: simp_rw [isCyclic_iff_exists_zpowers_eq_top, ← card_eq_iff_eq_top, Nat.card_zpowers]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : Finite α
⊢ IsCyclic α ↔ ∃ (g : α), Nat.card α ≤ orderOf g
have rw : (∃ (g : α), orderOf g = Nat.card α) ↔ ∃ (g : α), Nat.card α ≤ orderOf g
Tactic: rw [isCyclic_iff_exists_orderOf_eq_natCard]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : Finite α
⊢ (∃ (g : α), orderOf g = Nat.card α) ↔ ∃ (g : α), Nat.card α ≤ orderOf g
have h : ∀ (a : α), orderOf a = Nat.card α ↔ Nat.card α ≤ orderOf a
Tactic: apply exists_congr
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (hypothesis)
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
hp : Fact (Nat.Prime (Nat.card G))
⊢ H = ⊥ ∨ H = ⊤
have this : Finite G
Tactic: have : Finite G := Nat.finite_of_card_ne_zero hp.1.ne_zero
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (hypothesis)
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
hp : Fact (Nat.Prime (Nat.card G))
this : Finite G
⊢ H = ⊥ ∨ H = ⊤
have this₁ : Nat.card.{u_2} ↥H ∣ Nat.card G
Tactic: have := card_subgroup_dvd_card H
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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
⊢ H = ⊥ ∨ H = ⊤
have rwa : ∀ (this : Nat.card.{u_2} ↥H = 1 ∨ Nat.card.{u_2} ↥H = Nat.card G), H = ⊥ ∨ H = ⊤
Tactic: rwa [Nat.dvd_prime hp.1, ← eq_bot_iff_card, card_eq_iff_eq_top] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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 = ⊤
⊢ H = ⊥ ∨ H = ⊤
have rwa₁ : ∀ (this : H = ⊥ ∨ Nat.card.{u_2} ↥H = Nat.card G), H = ⊥ ∨ H = ⊤
Tactic: rwa [Nat.dvd_prime hp.1, ← eq_bot_iff_card, card_eq_iff_eq_top] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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 = ⊤
⊢ H = ⊥ ∨ H = ⊤
have rwa₂ : ∀ (this : H = ⊥ ∨ H = ⊤), H = ⊥ ∨ H = ⊤
Tactic: rwa [Nat.dvd_prime hp.1, ← eq_bot_iff_card, card_eq_iff_eq_top] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (hypothesis)
Goal:
G : Type u_2
inst : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g : G
hg : g ≠ 1
⊢ Eq (α := Subgroup G) (zpowers g) ⊤
have hp₁ : Fact (Nat.Prime (Nat.card G))
Tactic: subst h
Cleared hypotheses: p, hp, h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (hypothesis)
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) ⊤
have this : Eq (α := Subgroup G) (zpowers g) ⊥ ∨ Eq (α := Subgroup G) (zpowers g) ⊤
Tactic: have := (zpowers g).eq_bot_or_eq_top_of_prime_card
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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) ⊤
⊢ Eq (α := Subgroup G) (zpowers g) ⊤
have rwa : ∀ (this : g = 1 ∨ Eq (α := Subgroup G) (zpowers g) ⊤), Eq (α := Subgroup G) (zpowers g) ⊤
Tactic: rwa [zpowers_eq_bot, or_iff_right hg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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) ⊤
⊢ Eq (α := Subgroup G) (zpowers g) ⊤
have rwa₁ : ∀ (this : Eq (α := Subgroup G) (zpowers g) ⊤), Eq (α := Subgroup G) (zpowers g) ⊤
Tactic: rwa [zpowers_eq_bot, or_iff_right hg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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
⊢ Membership.mem (γ := Subgroup G) (zpowers g) g'
have simp_rw : Membership.mem (γ := Subgroup G) ⊤ g'
Tactic: simp_rw [zpowers_eq_top_of_prime_card h hg, Subgroup.mem_top]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (hypothesis)
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
⊢ Membership.mem (γ := Submonoid G) (Submonoid.powers g) g'
have this : Finite G
Tactic: have : Finite G := Nat.finite_of_card_ne_zero (h ▸ hp.1.ne_zero)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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 (γ := Submonoid G) (Submonoid.powers g) g'
have rw : Membership.mem (γ := Subgroup G) (zpowers g) g'
Tactic: rw [mem_powers_iff_mem_zpowers]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
G : Type u_2
inst : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g : G
hg : g ≠ 1
⊢ Eq (α := Submonoid G) (Submonoid.powers g) ⊤
have h₁ : ∀ (x : G), Membership.mem (γ := Submonoid G) (Submonoid.powers g) x ↔ Membership.mem (γ := Submonoid G) ⊤ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (hypothesis)
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
⊢ IsCyclic α
have this : Finite α
Tactic: have : Finite α := Nat.finite_of_card_ne_zero (h ▸ hp.1.ne_zero)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (hypothesis)
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
this : Finite α
⊢ IsCyclic α
have this₁ : Nontrivial α
Tactic: have : Nontrivial α := Finite.one_lt_card_iff_nontrivial.mp (h ▸ hp.1.one_lt)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
this_1 : Finite α
this : Nontrivial α
⊢ IsCyclic α
have obtain : ∀ (g : α) (hg : g ≠ 1), IsCyclic α
Tactic: obtain ⟨g, hg⟩ : ∃ g : α, g ≠ 1 := exists_ne 1
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α ∣ p
⊢ IsCyclic α
have inl : ∀ (h : Nat.card α = 1), IsCyclic α
Tactic: rcases (Nat.dvd_prime hp.out).mp h with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α ∣ p
inl : ∀ (h : Nat.card α = 1), IsCyclic α
⊢ IsCyclic α
have inr : ∀ (h : Nat.card α = p), IsCyclic α
Tactic: rcases (Nat.dvd_prime hp.out).mp h with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
F : Type u_4
hH : IsCyclic G'
inst_2 : FunLike F G' G
inst_3 : MonoidHomClass F G' G
f : F
hf : Function.Surjective.{u_3 + 1, u_2 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
⊢ IsCyclic G
have obtain : ∀ (x : G') (hx : Function.Surjective.{1, u_3 + 1} (β := G') fun (x_1 : ℤ) ↦ x ^ x_1), IsCyclic G
Tactic: obtain ⟨x, hx⟩ := hH
Cleared hypotheses: hH
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
F : Type u_4
inst_2 : FunLike F G' G
inst_3 : MonoidHomClass F G' G
f : F
hf : Function.Surjective.{u_3 + 1, u_2 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
x : G'
hx : Function.Surjective.{1, u_3 + 1} (β := G') fun (x_1 : ℤ) ↦ x ^ x_1
⊢ IsCyclic G
have refine : ∀ (a : G), ∃ (a_1 : ℤ), (fun (x_1 : ℤ) ↦ HPow.hPow (α := G) ((f : (a : G') → G) x : G) x_1) a_1 = a
Tactic: refine ⟨f x, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
F : Type u_4
inst_2 : FunLike F G' G
inst_3 : MonoidHomClass F G' G
f : F
hf : Function.Surjective.{u_3 + 1, u_2 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
x : G'
hx : Function.Surjective.{1, u_3 + 1} (β := G') fun (x_1 : ℤ) ↦ x ^ x_1
a : G
⊢ ∃ (a_1 : ℤ), (fun (x_1 : ℤ) ↦ HPow.hPow (α := G) ((f : (a : G') → G) x : G) x_1) a_1 = a
have obtain : ∀ (a : G'),
  ∃ (a_1 : ℤ),
    Eq.{u_2 + 1} (α := G) ((fun (x_1 : ℤ) ↦ HPow.hPow (α := G) ((f : (a : G') → G) x : G) x_1) a_1 : G)
      ((f : (a : G') → G) a : G)
Tactic: obtain ⟨a, rfl⟩ := hf a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
F : Type u_4
inst_2 : FunLike F G' G
inst_3 : MonoidHomClass F G' G
f : F
hf : Function.Surjective.{u_3 + 1, u_2 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
x : G'
hx : Function.Surjective.{1, u_3 + 1} (β := G') fun (x_1 : ℤ) ↦ x ^ x_1
a : G'
⊢ ∃ (a_1 : ℤ),
    Eq.{u_2 + 1} (α := G) ((fun (x_1 : ℤ) ↦ HPow.hPow (α := G) ((f : (a : G') → G) x : G) x_1) a_1 : G)
      ((f : (a : G') → G) a : G)
have obtain : ∀ (n : ℤ),
  ∃ (a : ℤ),
    Eq.{u_2 + 1} (α := G) ((fun (x_1 : ℤ) ↦ HPow.hPow (α := G) ((f : (a : G') → G) x : G) x_1) a : G)
      ((f : (a : G') → G) ((fun (x_1 : ℤ) ↦ x ^ x_1) n) : G)
Tactic: obtain ⟨n, rfl⟩ := hx a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
inst : Group α
g : α
hx : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
⊢ orderOf g = Nat.card α
have rw : Nat.card.{u_1} ↥(zpowers g) = Nat.card α
Tactic: rw [← Nat.card_zpowers, (zpowers g).eq_top_iff'.mpr hx, card_top]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
inst : Group α
g : α
hx : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
rw : Nat.card.{u_1} ↥(zpowers g) = Nat.card α
⊢ orderOf g = Nat.card α
have rw₁ : Nat.card.{u_1} ↥⊤ = Nat.card α
Tactic: rw [← Nat.card_zpowers, (zpowers g).eq_top_iff'.mpr hx, card_top]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
inst : Group α
g : α
hx : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
rw : Nat.card.{u_1} ↥(zpowers g) = Nat.card α
rw₁ : Nat.card.{u_1} ↥⊤ = Nat.card α
⊢ orderOf g = Nat.card α
have rw₂ : Nat.card α = Nat.card α
Tactic: rw [← Nat.card_zpowers, (zpowers g).eq_top_iff'.mpr hx, card_top]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
inst : Group α
g : α
hx : ∀ (x : α), Membership.mem (γ := Submonoid α) (Submonoid.powers g) x
⊢ orderOf g = Nat.card α
have rw : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
Tactic: rw [orderOf_eq_card_of_forall_mem_zpowers]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (hypothesis)
Goal:
G : Type u_2
inst : Group G
G_cyclic : IsCyclic G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card G
⊢ ∃ (a : G), a ^ k ≠ 1
have this : Finite G
Tactic: have : Finite G := Nat.finite_of_card_ne_zero (Nat.ne_zero_of_lt k_lt_card_G)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
G : Type u_2
inst : Group G
G_cyclic : IsCyclic G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card G
this : Finite G
⊢ ∃ (a : G), a ^ k ≠ 1
have rcases : ∀ (a : G) (ha : Function.Surjective.{1, u_2 + 1} (β := G) fun (x : ℤ) ↦ a ^ x), ∃ (a : G), a ^ k ≠ 1
Tactic: rcases G_cyclic with ⟨a, ha⟩
Cleared hypotheses: G_cyclic