awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
G : Type u_2
inst_1 : Group G
n : ℕ
v : List.Vector G n
⊢ Membership.mem (γ := Set (List.Vector G (n + 1))) (vectorsProdEqOne G (n + 1)) (v.toList.prod⁻¹ ::ᵥ v)
have rw : (v.toList.prod⁻¹ ::ᵥ v).toList.prod = 1
Tactic: rw [mem_iff, Vector.toList_cons, List.prod_cons, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
G : Type u_2
inst_1 : Group G
n : ℕ
v : List.Vector G n
rw : (v.toList.prod⁻¹ ::ᵥ v).toList.prod = 1
⊢ Membership.mem (γ := Set (List.Vector G (n + 1))) (vectorsProdEqOne G (n + 1)) (v.toList.prod⁻¹ ::ᵥ v)
have rw₁ : (v.toList.prod⁻¹ :: v.toList).prod = 1
Tactic: rw [mem_iff, Vector.toList_cons, List.prod_cons, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
G : Type u_2
inst_1 : Group G
n : ℕ
v : List.Vector G n
rw : (v.toList.prod⁻¹ ::ᵥ v).toList.prod = 1
rw₁ : (v.toList.prod⁻¹ :: v.toList).prod = 1
⊢ Membership.mem (γ := Set (List.Vector G (n + 1))) (vectorsProdEqOne G (n + 1)) (v.toList.prod⁻¹ ::ᵥ v)
have rw₂ : v.toList.prod⁻¹ * v.toList.prod = 1
Tactic: rw [mem_iff, Vector.toList_cons, List.prod_cons, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
G : Type u_2
inst_1 : Group G
n : ℕ
v : List.Vector G n
rw : (v.toList.prod⁻¹ ::ᵥ v).toList.prod = 1
rw₁ : (v.toList.prod⁻¹ :: v.toList).prod = 1
rw₂ : v.toList.prod⁻¹ * v.toList.prod = 1
⊢ Membership.mem (γ := Set (List.Vector G (n + 1))) (vectorsProdEqOne G (n + 1)) (v.toList.prod⁻¹ ::ᵥ v)
have rw₃ : Eq.{u_2 + 1} (α := G) 1 1
Tactic: rw [mem_iff, Vector.toList_cons, List.prod_cons, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
G : Type u_2
inst_1 : Group G
n : ℕ
v : (↑(vectorsProdEqOne G (n + 1)) : Type u_2)
⊢ (↑v : List.Vector G (n + 1)).head * (↑v : List.Vector G (n + 1)).tail.toList.prod = 1
have rw : (↑v : List.Vector G (n + 1)).toList.prod = 1
Tactic: rw [← List.prod_cons, ← Vector.toList_cons, v.1.cons_head_tail]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
⊢ ∃ (x : G), orderOf x = p
have hp' : p - 1 ≠ 0
Tactic: have hp' : p - 1 ≠ 0 := mt tsub_eq_zero_iff_le.mp (not_le_of_gt hp.out.one_lt)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
⊢ ∃ (x : G), orderOf x = p
have Scard : p ∣ Fintype.card.{u_3} (↑(vectorsProdEqOne G p) : Type u_3)
Tactic: have Scard :=
    calc
      p ∣ Fintype.card G ^ (p - 1) := hdvd.trans (dvd_pow (dvd_refl _) hp')
      _ = Fintype.card (vectorsProdEqOne G p) := (VectorsProdEqOne.card G p).symm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card.{u_3} (↑(vectorsProdEqOne G p) : Type u_3)
f : ℕ → (↑(vectorsProdEqOne G p) : Type u_3) → (↑(vectorsProdEqOne G p) : Type u_3) :=
  fun (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)) ↦ VectorsProdEqOne.rotate v k
⊢ ∃ (x : G), orderOf x = p
have hf1 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f 0 v = v
Tactic: have hf1 : ∀ v, f 0 v = v := VectorsProdEqOne.rotate_zero
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card.{u_3} (↑(vectorsProdEqOne G p) : Type u_3)
f : ℕ → (↑(vectorsProdEqOne G p) : Type u_3) → (↑(vectorsProdEqOne G p) : Type u_3) :=
  fun (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)) ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f 0 v = v
⊢ ∃ (x : G), orderOf x = p
have hf2 : ∀ (j k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)), f k (f j v) = f (j + k) v
Tactic: have hf2 : ∀ j k v, f k (f j v) = f (j + k) v := fun j k v =>
    VectorsProdEqOne.rotate_rotate v j k
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card.{u_3} (↑(vectorsProdEqOne G p) : Type u_3)
f : ℕ → (↑(vectorsProdEqOne G p) : Type u_3) → (↑(vectorsProdEqOne G p) : Type u_3) :=
  fun (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)) ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)), f k (f j v) = f (j + k) v
⊢ ∃ (x : G), orderOf x = p
have hf3 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f p v = v
Tactic: have hf3 : ∀ v, f p v = v := VectorsProdEqOne.rotate_length
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card.{u_3} (↑(vectorsProdEqOne G p) : Type u_3)
f : ℕ → (↑(vectorsProdEqOne G p) : Type u_3) → (↑(vectorsProdEqOne G p) : Type u_3) :=
  fun (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)) ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f p v = v
s : (↑(vectorsProdEqOne G p) : Type u_3)
⊢ f (p - 1) (f 1 s) = s
have rw : f (1 + (p - 1)) s = s
Tactic: rw [hf2, add_tsub_cancel_of_le hp.out.one_lt.le, hf3]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card.{u_3} (↑(vectorsProdEqOne G p) : Type u_3)
f : ℕ → (↑(vectorsProdEqOne G p) : Type u_3) → (↑(vectorsProdEqOne G p) : Type u_3) :=
  fun (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)) ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f p v = v
s : (↑(vectorsProdEqOne G p) : Type u_3)
rw : f (1 + (p - 1)) s = s
⊢ f (p - 1) (f 1 s) = s
have rw₁ : f p s = s
Tactic: rw [hf2, add_tsub_cancel_of_le hp.out.one_lt.le, hf3]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card.{u_3} (↑(vectorsProdEqOne G p) : Type u_3)
f : ℕ → (↑(vectorsProdEqOne G p) : Type u_3) → (↑(vectorsProdEqOne G p) : Type u_3) :=
  fun (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)) ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f p v = v
s : (↑(vectorsProdEqOne G p) : Type u_3)
rw : f (1 + (p - 1)) s = s
rw₁ : f p s = s
⊢ f (p - 1) (f 1 s) = s
have rw₂ : s = s
Tactic: rw [hf2, add_tsub_cancel_of_le hp.out.one_lt.le, hf3]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card.{u_3} (↑(vectorsProdEqOne G p) : Type u_3)
f : ℕ → (↑(vectorsProdEqOne G p) : Type u_3) → (↑(vectorsProdEqOne G p) : Type u_3) :=
  fun (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)) ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f p v = v
s : (↑(vectorsProdEqOne G p) : Type u_3)
⊢ f 1 (f (p - 1) s) = s
have rw : f (p - 1 + 1) s = s
Tactic: rw [hf2, tsub_add_cancel_of_le hp.out.one_lt.le, hf3]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card.{u_3} (↑(vectorsProdEqOne G p) : Type u_3)
f : ℕ → (↑(vectorsProdEqOne G p) : Type u_3) → (↑(vectorsProdEqOne G p) : Type u_3) :=
  fun (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)) ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f p v = v
s : (↑(vectorsProdEqOne G p) : Type u_3)
rw : f (p - 1 + 1) s = s
⊢ f 1 (f (p - 1) s) = s
have rw₁ : f p s = s
Tactic: rw [hf2, tsub_add_cancel_of_le hp.out.one_lt.le, hf3]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card.{u_3} (↑(vectorsProdEqOne G p) : Type u_3)
f : ℕ → (↑(vectorsProdEqOne G p) : Type u_3) → (↑(vectorsProdEqOne G p) : Type u_3) :=
  fun (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)) ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f p v = v
s : (↑(vectorsProdEqOne G p) : Type u_3)
rw : f (p - 1 + 1) s = s
rw₁ : f p s = s
⊢ f 1 (f (p - 1) s) = s
have rw₂ : s = s
Tactic: rw [hf2, tsub_add_cancel_of_le hp.out.one_lt.le, hf3]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card.{u_3} (↑(vectorsProdEqOne G p) : Type u_3)
f : ℕ → (↑(vectorsProdEqOne G p) : Type u_3) → (↑(vectorsProdEqOne G p) : Type u_3) :=
  fun (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)) ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f p v = v
σ : (↑(vectorsProdEqOne G p) : Type u_3) ≃ (↑(vectorsProdEqOne G p) : Type u_3) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
k_1 k : ℕ
hk :
  ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)),
    (σ ^ k : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v = f k v
v : (↑(vectorsProdEqOne G p) : Type u_3)
⊢ (σ ^ k.succ : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v = f k.succ v
have rw : f k ((σ : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v) = f k (f 1 v)
Tactic: rw [pow_succ, Perm.mul_apply, hk (σ v), Nat.succ_eq_one_add, ← hf2 1 k]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card.{u_3} (↑(vectorsProdEqOne G p) : Type u_3)
f : ℕ → (↑(vectorsProdEqOne G p) : Type u_3) → (↑(vectorsProdEqOne G p) : Type u_3) :=
  fun (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)) ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f p v = v
σ : (↑(vectorsProdEqOne G p) : Type u_3) ≃ (↑(vectorsProdEqOne G p) : Type u_3) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
⊢ ∃ (x : G), orderOf x = p
have hσ : ∀ (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)),
  (σ ^ k : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v = f k v
Tactic: have hσ : ∀ k v, (σ ^ k) v = f k v := fun k =>
    Nat.rec (fun v => (hf1 v).symm) (fun k hk v => by
      rw [pow_succ, Perm.mul_apply, hk (σ v), Nat.succ_eq_one_add, ← hf2 1 k]
      simp only [σ, coe_fn_mk]) k
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card.{u_3} (↑(vectorsProdEqOne G p) : Type u_3)
f : ℕ → (↑(vectorsProdEqOne G p) : Type u_3) → (↑(vectorsProdEqOne G p) : Type u_3) :=
  fun (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)) ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f p v = v
σ : (↑(vectorsProdEqOne G p) : Type u_3) ≃ (↑(vectorsProdEqOne G p) : Type u_3) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
hσ :
  ∀ (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)),
    (σ ^ k : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v = f k v
v : (↑(vectorsProdEqOne G p) : Type u_3)
⊢ Eq (α := (↑(vectorsProdEqOne G p) : Type u_3))
    ((σ ^ HPow.hPow (β := ℕ) p 1 : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3))
        v :
      (↑(vectorsProdEqOne G p) : Type u_3))
    ((1 : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v :
      (↑(vectorsProdEqOne G p) : Type u_3))
have rw : Eq (α := (↑(vectorsProdEqOne G p) : Type u_3))
  ((σ ^ p : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v :
    (↑(vectorsProdEqOne G p) : Type u_3))
  ((1 : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v :
    (↑(vectorsProdEqOne G p) : Type u_3))
Tactic: rw [pow_one, hσ, hf3, one_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card.{u_3} (↑(vectorsProdEqOne G p) : Type u_3)
f : ℕ → (↑(vectorsProdEqOne G p) : Type u_3) → (↑(vectorsProdEqOne G p) : Type u_3) :=
  fun (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)) ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f p v = v
σ : (↑(vectorsProdEqOne G p) : Type u_3) ≃ (↑(vectorsProdEqOne G p) : Type u_3) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
hσ :
  ∀ (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)),
    (σ ^ k : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v = f k v
v : (↑(vectorsProdEqOne G p) : Type u_3)
rw :
  Eq (α := (↑(vectorsProdEqOne G p) : Type u_3))
    ((σ ^ p : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v :
      (↑(vectorsProdEqOne G p) : Type u_3))
    ((1 : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v :
      (↑(vectorsProdEqOne G p) : Type u_3))
⊢ Eq (α := (↑(vectorsProdEqOne G p) : Type u_3))
    ((σ ^ HPow.hPow (β := ℕ) p 1 : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3))
        v :
      (↑(vectorsProdEqOne G p) : Type u_3))
    ((1 : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v :
      (↑(vectorsProdEqOne G p) : Type u_3))
have rw₁ : f p v = (1 : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v
Tactic: rw [pow_one, hσ, hf3, one_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card.{u_3} (↑(vectorsProdEqOne G p) : Type u_3)
f : ℕ → (↑(vectorsProdEqOne G p) : Type u_3) → (↑(vectorsProdEqOne G p) : Type u_3) :=
  fun (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)) ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f p v = v
σ : (↑(vectorsProdEqOne G p) : Type u_3) ≃ (↑(vectorsProdEqOne G p) : Type u_3) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
hσ :
  ∀ (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)),
    (σ ^ k : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v = f k v
v : (↑(vectorsProdEqOne G p) : Type u_3)
rw :
  Eq (α := (↑(vectorsProdEqOne G p) : Type u_3))
    ((σ ^ p : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v :
      (↑(vectorsProdEqOne G p) : Type u_3))
    ((1 : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v :
      (↑(vectorsProdEqOne G p) : Type u_3))
rw₁ : f p v = (1 : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v
⊢ Eq (α := (↑(vectorsProdEqOne G p) : Type u_3))
    ((σ ^ HPow.hPow (β := ℕ) p 1 : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3))
        v :
      (↑(vectorsProdEqOne G p) : Type u_3))
    ((1 : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v :
      (↑(vectorsProdEqOne G p) : Type u_3))
have rw₂ : v = (1 : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v
Tactic: rw [pow_one, hσ, hf3, one_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card.{u_3} (↑(vectorsProdEqOne G p) : Type u_3)
f : ℕ → (↑(vectorsProdEqOne G p) : Type u_3) → (↑(vectorsProdEqOne G p) : Type u_3) :=
  fun (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)) ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f p v = v
σ : (↑(vectorsProdEqOne G p) : Type u_3) ≃ (↑(vectorsProdEqOne G p) : Type u_3) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
hσ :
  ∀ (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)),
    (σ ^ k : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v = f k v
v : (↑(vectorsProdEqOne G p) : Type u_3)
rw :
  Eq (α := (↑(vectorsProdEqOne G p) : Type u_3))
    ((σ ^ p : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v :
      (↑(vectorsProdEqOne G p) : Type u_3))
    ((1 : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v :
      (↑(vectorsProdEqOne G p) : Type u_3))
rw₁ : f p v = (1 : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v
rw₂ : v = (1 : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v
⊢ Eq (α := (↑(vectorsProdEqOne G p) : Type u_3))
    ((σ ^ HPow.hPow (β := ℕ) p 1 : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3))
        v :
      (↑(vectorsProdEqOne G p) : Type u_3))
    ((1 : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v :
      (↑(vectorsProdEqOne G p) : Type u_3))
have rw₃ : v = v
Tactic: rw [pow_one, hσ, hf3, one_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card.{u_3} (↑(vectorsProdEqOne G p) : Type u_3)
f : ℕ → (↑(vectorsProdEqOne G p) : Type u_3) → (↑(vectorsProdEqOne G p) : Type u_3) :=
  fun (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)) ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f p v = v
σ : (↑(vectorsProdEqOne G p) : Type u_3) ≃ (↑(vectorsProdEqOne G p) : Type u_3) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
hσ :
  ∀ (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)),
    (σ ^ k : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v = f k v
⊢ ∃ (x : G), orderOf x = p
have hσ₁ : σ ^ HPow.hPow (β := ℕ) p 1 = 1
Tactic: replace hσ : σ ^ p ^ 1 = 1 := Perm.ext fun v => by rw [pow_one, hσ, hf3, one_apply]
Cleared hypotheses: hσ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card.{u_3} (↑(vectorsProdEqOne G p) : Type u_3)
f : ℕ → (↑(vectorsProdEqOne G p) : Type u_3) → (↑(vectorsProdEqOne G p) : Type u_3) :=
  fun (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)) ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f p v = v
σ : (↑(vectorsProdEqOne G p) : Type u_3) ≃ (↑(vectorsProdEqOne G p) : Type u_3) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ HPow.hPow (β := ℕ) p 1 = 1
v₀ : (↑(vectorsProdEqOne G p) : Type u_3) :=
  Subtype.mk (p := fun (x : List.Vector G p) ↦ x ∈ vectorsProdEqOne G p) (List.Vector.replicate p 1) ⋯
⊢ ∃ (x : G), orderOf x = p
have hv₀ : (σ : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v₀ = v₀
Tactic: have hv₀ : σ v₀ = v₀ := Subtype.ext (Subtype.ext (List.rotate_replicate (1 : G) p 1))
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card.{u_3} (↑(vectorsProdEqOne G p) : Type u_3)
f : ℕ → (↑(vectorsProdEqOne G p) : Type u_3) → (↑(vectorsProdEqOne G p) : Type u_3) :=
  fun (k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)) ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : (↑(vectorsProdEqOne G p) : Type u_3)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f p v = v
σ : (↑(vectorsProdEqOne G p) : Type u_3) ≃ (↑(vectorsProdEqOne G p) : Type u_3) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ HPow.hPow (β := ℕ) p 1 = 1
v₀ : (↑(vectorsProdEqOne G p) : Type u_3) :=
  Subtype.mk (p := fun (x : List.Vector G p) ↦ x ∈ vectorsProdEqOne G p) (List.Vector.replicate p 1) ⋯
hv₀ : (σ : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v₀ = v₀
⊢ ∃ (x : G), orderOf x = p
have obtain : ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3))
  (hv1 : (σ : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v = v) (hv2 : v ≠ v₀),
  ∃ (x : G), orderOf x = p
Tactic: obtain ⟨v, hv1, hv2⟩ := exists_fixed_point_of_prime' Scard hσ hv₀