awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
G : Type u_2
inst : Group G
simp_rw : ∀ (x : List.Vector G 1), x.head = 1 → x = 1 ::ᵥ Vector.nil
⊢ Eq (α := Set (List.Vector G 1)) (vectorsProdEqOne G 1) {1 ::ᵥ Vector.nil}

Tactic:
simp_rw [Set.eq_singleton_iff_unique_mem, mem_iff, List.Vector.toList_singleton,
    List.prod_singleton, List.Vector.head_cons, true_and]

Premises used: Equiv.Perm.VectorsProdEqOne.mem_iff, List.prod_singleton, List.Vector.head_cons, List.Vector.toList_singleton, Set.eq_singleton_iff_unique_mem, true_and
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
G : Type u_2
inst : Group G
⊢ ∀ (x : List.Vector G 1), x.head = 1 → x = 1 ::ᵥ Vector.nil

Tactic:
fun v hv => v.cons_head_tail.symm.trans (congr_arg₂ Vector.cons hv v.tail.eq_nil)

Premises used: List.Vector.eq_nil, List.Vector.cons_head_tail, Eq.symm, List.Vector.tail, List.Vector.cons, Eq.trans, congr_arg₂
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
G : Type u_2
inst : Group G
⊢ ∀ (x : List.Vector G 1), x.head = 1 → x = 1 ::ᵥ Vector.nil

Tactic:
exact fun v hv => v.cons_head_tail.symm.trans (congr_arg₂ Vector.cons hv v.tail.eq_nil)
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
G : Type u_2
inst_1 : Group G
n : ℕ
rw : Unique (↑{Vector.nil} : Type u_2)
⊢ Unique (↑(vectorsProdEqOne G 0) : Type u_2)

Tactic:
rw [zero_eq]

Premises used: Equiv.Perm.VectorsProdEqOne.zero_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
G : Type u_2
inst_1 : Group G
n : ℕ
⊢ Unique (↑{Vector.nil} : Type u_2)

Tactic:
exact Set.uniqueSingleton Vector.nil

Premises used: Set.uniqueSingleton, List.Vector.nil
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
G : Type u_2
inst_1 : Group G
n : ℕ
rw : Unique (↑{1 ::ᵥ Vector.nil} : Type u_2)
⊢ Unique (↑(vectorsProdEqOne G 1) : Type u_2)

Tactic:
rw [one_eq]

Premises used: Equiv.Perm.VectorsProdEqOne.one_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
G : Type u_2
inst_1 : Group G
n : ℕ
⊢ Unique (↑{1 ::ᵥ Vector.nil} : Type u_2)

Tactic:
exact Set.uniqueSingleton (Vector.nil.cons 1)

Premises used: Set.uniqueSingleton, List.Vector.nil, OfNat.ofNat, List.Vector.cons
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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
rw₃ rw₄ : Eq.{u_2 + 1} (α := G) 1 1
⊢ Membership.mem (γ := Set (List.Vector G (n + 1))) (vectorsProdEqOne G (n + 1)) (v.toList.prod⁻¹ ::ᵥ v)

Tactic:
rw [mem_iff, Vector.toList_cons, List.prod_cons, inv_mul_cancel]

Premises used: inv_mul_cancel, Equiv.Perm.VectorsProdEqOne.mem_iff, List.Vector.toList_cons, List.prod_cons
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
G : Type u_2
inst_1 : Group G
n : ℕ
v : (↑(vectorsProdEqOne G (n + 1)) : Type u_2)
rw : (↑v : List.Vector G (n + 1)).toList.prod = 1
⊢ (↑v : List.Vector G (n + 1)).head * (↑v : List.Vector G (n + 1)).tail.toList.prod = 1

Tactic:
rw [← List.prod_cons, ← Vector.toList_cons, v.1.cons_head_tail]

Premises used: List.Vector.toList_cons, List.Vector.cons_head_tail, Subtype.val, List.prod_cons
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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)).toList.prod = 1

Tactic:
v.2

Premises used: Set.Mem, Equiv.Perm.vectorsProdEqOne, setOf, Nat.pred, Subtype.property
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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)).toList.prod = 1

Tactic:
exact v.2

Premises used: Subtype.property
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
G : Type u_2
inst : Group G
n : ℕ
inst_1 : Fintype G
⊢ Fintype.card.{u_2} (↑(vectorsProdEqOne G n) : Type u_2) = Fintype.card G ^ (n - 1)

Tactic:
(Fintype.card_congr (equivVector G n)).trans (card_vector (n - 1))

Premises used: Fintype.card_congr, HSub.hSub, card_vector, Equiv.Perm.VectorsProdEqOne.equivVector, OfNat.ofNat, Eq.trans
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
G : Type u_2
inst : Group G
n : ℕ
v : (↑(vectorsProdEqOne G n) : Type u_2)
⊢ rotate v 0 = v

Tactic:
Subtype.ext (Subtype.ext v.1.1.rotate_zero)

Premises used: List.rotate_zero, Subtype.val, Subtype.ext
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
G : Type u_2
inst : Group G
n : ℕ
v : (↑(vectorsProdEqOne G n) : Type u_2)
j k : ℕ
⊢ rotate (rotate v j) k = rotate v (j + k)

Tactic:
Subtype.ext (Subtype.ext (v.1.1.rotate_rotate j k))

Premises used: List.rotate_rotate, Subtype.val, Subtype.ext
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
G : Type u_2
inst : Group G
n : ℕ
v : (↑(vectorsProdEqOne G n) : Type u_2)
⊢ rotate v n = v

Tactic:
Subtype.ext (Subtype.ext ((congr_arg _ v.1.2.symm).trans v.1.1.rotate_length))

Premises used: List.rotate_length, congr_arg, Eq.symm, Subtype.val, Eq.trans, Subtype.property, Subtype.ext
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
G : Type u_3
inst : Group G
inst_1 : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
⊢ p - 1 ≠ 0

Tactic:
have hp' : p - 1 ≠ 0 := mt tsub_eq_zero_iff_le.mp (not_le_of_gt hp.out.one_lt)
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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
⊢ 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
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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
⊢ ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f 0 v = v

Tactic:
have hf1 : ∀ v, f 0 v = v := VectorsProdEqOne.rotate_zero
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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
⊢ ∀ (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
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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
⊢ ∀ (v : (↑(vectorsProdEqOne G p) : Type u_3)), f p v = v

Tactic:
have hf3 : ∀ v, f p v = v := VectorsProdEqOne.rotate_length
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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
rw₂ rw₃ : s = s
⊢ f (p - 1) (f 1 s) = s

Tactic:
rw [hf2, add_tsub_cancel_of_le hp.out.one_lt.le, hf3]

Premises used: Nat.Prime.one_lt, LT.lt.le, add_tsub_cancel_of_le, Fact.out
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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
rw₂ rw₃ : s = s
⊢ f 1 (f (p - 1) s) = s

Tactic:
rw [hf2, tsub_add_cancel_of_le hp.out.one_lt.le, hf3]

Premises used: Nat.Prime.one_lt, tsub_add_cancel_of_le, LT.lt.le, Fact.out
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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)
rw : f k ((σ : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v) = f k (f 1 v)
⊢ (σ ^ k.succ : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v = f k.succ v

Tactic:
rw [pow_succ, Perm.mul_apply, hk (σ v), Nat.succ_eq_one_add, ← hf2 1 k]

Premises used: pow_succ, Nat.succ_eq_one_add, Equiv.Perm.mul_apply, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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)
⊢ f k ((σ : (a : (↑(vectorsProdEqOne G p) : Type u_3)) → (↑(vectorsProdEqOne G p) : Type u_3)) v) = f k (f 1 v)

Tactic:
simp only [σ, coe_fn_mk]

Premises used: Equiv.coe_fn_mk
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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 : ℕ) (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
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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
rw₃ rw₄ : v = 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))

Tactic:
rw [pow_one, hσ, hf3, one_apply]

Premises used: pow_one, Equiv.Perm.one_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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
⊢ σ ^ HPow.hPow (β := ℕ) p 1 = 1

Tactic:
replace hσ : σ ^ p ^ 1 = 1 := Perm.ext fun v => by rw [pow_one, hσ, hf3, one_apply]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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) ⋯
⊢ (σ : (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))
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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₀
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
⊢ ∃ (x : G), orderOf x = p

Tactic:
obtain ⟨v, hv1, hv2⟩ := exists_fixed_point_of_prime' Scard hσ hv₀

Premises used: Equiv.Perm.exists_fixed_point_of_prime'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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₀
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:
Exists.imp (fun g hg => orderOf_eq_prime ?_ fun hg' => hv2 ?_)
      (List.rotate_one_eq_self_iff_eq_replicate.mp (Subtype.ext_iff.mp (Subtype.ext_iff.mp hv1)))

Premises used: List.rotate_one_eq_self_iff_eq_replicate, orderOf_eq_prime, Exists.imp, Subtype.ext_iff, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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₀
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₀
refine_1 :
  ∀ (g : G) (hg : (↑(↑v : List.Vector G p) : List G) = List.replicate (↑(↑v : List.Vector G p) : List G).length g),
    g ^ p = 1
refine_2 :
  ∀ (g : G) (hg : (↑(↑v : List.Vector G p) : List G) = List.replicate (↑(↑v : List.Vector G p) : List G).length g)
    (hg' : g = 1), v = v₀
⊢ ∃ (x : G), orderOf x = p

Tactic:
refine
    Exists.imp (fun g hg => orderOf_eq_prime ?_ fun hg' => hv2 ?_)
      (List.rotate_one_eq_self_iff_eq_replicate.mp (Subtype.ext_iff.mp (Subtype.ext_iff.mp hv1)))

Premises used: List.rotate_one_eq_self_iff_eq_replicate, orderOf_eq_prime, Exists.imp, Subtype.ext_iff, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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₀
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₀
g : G
hg : (↑(↑v : List.Vector G p) : List G) = List.replicate (↑(↑v : List.Vector G p) : List G).length g
refine_1 : (List.replicate p g).prod = 1
refine_1₁ : (List.replicate (↑(↑v : List.Vector G p) : List G).length g).prod = 1
refine_1₂ : (↑(↑v : List.Vector G p) : List G).prod = 1
refine_1₃ refine_1₄ : Eq.{u_3 + 1} (α := G) 1 1
⊢ g ^ p = 1

Tactic:
rw [← List.prod_replicate, ← v.1.2, ← hg, show v.val.val.prod = 1 from v.2]

Premises used: Subtype.val, List.prod_replicate, Subtype.property