awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₀
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
have 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
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)))
-- 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₀
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
⊢ ∃ (x : G), orderOf x = p
have 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₀
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)))
-- 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₀
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
⊢ g ^ p = 1
have refine_1 : (List.replicate p g).prod = 1
Tactic: rw [← List.prod_replicate, ← v.1.2, ← hg, show v.val.val.prod = 1 from v.2]
-- 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₀
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
⊢ g ^ p = 1
have refine_1₁ : (List.replicate (↑(↑v : List.Vector G p) : List G).length g).prod = 1
Tactic: rw [← List.prod_replicate, ← v.1.2, ← hg, show v.val.val.prod = 1 from v.2]
-- 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₀
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
⊢ g ^ p = 1
have refine_1₂ : (↑(↑v : List.Vector G p) : List G).prod = 1
Tactic: rw [← List.prod_replicate, ← v.1.2, ← hg, show v.val.val.prod = 1 from v.2]
-- 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₀
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
⊢ g ^ p = 1
have refine_1₃ : Eq.{u_3 + 1} (α := G) 1 1
Tactic: rw [← List.prod_replicate, ← v.1.2, ← hg, show v.val.val.prod = 1 from v.2]
-- 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₀
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
hg' : g = 1
⊢ v = v₀
have refine_2 : List.replicate p 1 = (↑(↑v₀ : List.Vector G p) : List G)
Tactic: rw [Subtype.ext_iff, Subtype.ext_iff, hg, hg', v.1.2]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Nat.card G
⊢ ∃ (x : G), orderOf x = p
have have : ∀ (this : Fintype G), ∃ (x : G), orderOf x = p
Tactic: have := Fintype.ofFinite G
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Nat.card G
this : Fintype G
⊢ ∃ (x : G), orderOf x = p
have hdvd₁ : p ∣ Fintype.card G
Tactic: rw [Nat.card_eq_fintype_card] at hdvd
Cleared hypotheses: hdvd
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun (x : Perm α) ↦ x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card.{u_1} ↥H
h2 : τ ∈ H
h3 : τ.IsSwap
⊢ H = ⊤
have this : Fact (Nat.Prime (Fintype.card α))
Tactic: haveI : Fact (Fintype.card α).Prime := ⟨h0⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun (x : Perm α) ↦ x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card.{u_1} ↥H
h2 : τ ∈ H
h3 : τ.IsSwap
this : Fact (Nat.Prime (Fintype.card α))
⊢ H = ⊤
have obtain : ∀ (σ : ↥H) (hσ : orderOf σ = Fintype.card α), H = ⊤
Tactic: obtain ⟨σ, hσ⟩ := exists_prime_orderOf_dvd_card (Fintype.card α) h1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun (x : Perm α) ↦ x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card.{u_1} ↥H
h2 : τ ∈ H
h3 : τ.IsSwap
this : Fact (Nat.Prime (Fintype.card α))
σ : ↥H
hσ : orderOf σ = Fintype.card α
⊢ H = ⊤
have hσ1 : orderOf (↑σ : Perm α) = Fintype.card α
Tactic: have hσ1 : orderOf (σ : Perm α) = Fintype.card α := (Subgroup.orderOf_coe σ).trans hσ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun (x : Perm α) ↦ x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card.{u_1} ↥H
h2 : τ ∈ H
h3 : τ.IsSwap
this : Fact (Nat.Prime (Fintype.card α))
σ : ↥H
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf (↑σ : Perm α) = Fintype.card α
⊢ H = ⊤
have hσ2 : (↑σ : Perm α).IsCycle
Tactic: have hσ2 : IsCycle ↑σ := isCycle_of_prime_order'' h0 hσ1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun (x : Perm α) ↦ x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card.{u_1} ↥H
h2 : τ ∈ H
h3 : τ.IsSwap
this : Fact (Nat.Prime (Fintype.card α))
σ : ↥H
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf (↑σ : Perm α) = Fintype.card α
hσ2 : (↑σ : Perm α).IsCycle
⊢ H = ⊤
have hσ3 : (↑σ : Perm α).support = ⊤
Tactic: have hσ3 : (σ : Perm α).support = ⊤ :=
    Finset.eq_univ_of_card (σ : Perm α).support (hσ2.orderOf.symm.trans hσ1)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun (x : Perm α) ↦ x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card.{u_1} ↥H
h2 : τ ∈ H
h3 : τ.IsSwap
this : Fact (Nat.Prime (Fintype.card α))
σ : ↥H
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf (↑σ : Perm α) = Fintype.card α
hσ2 : (↑σ : Perm α).IsCycle
hσ3 : (↑σ : Perm α).support = ⊤
⊢ H = ⊤
have hσ4 : Eq (α := Subgroup (Perm α)) (Subgroup.closure {(↑σ : Perm α), τ}) ⊤
Tactic: have hσ4 : Subgroup.closure {↑σ, τ} = ⊤ := closure_prime_cycle_swap h0 hσ2 hσ3 h3
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun (x : Perm α) ↦ x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card.{u_1} ↥H
h2 : τ ∈ H
h3 : τ.IsSwap
this : Fact (Nat.Prime (Fintype.card α))
σ : ↥H
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf (↑σ : Perm α) = Fintype.card α
hσ2 : (↑σ : Perm α).IsCycle
hσ3 : (↑σ : Perm α).support = ⊤
hσ4 : Eq (α := Subgroup (Perm α)) (Subgroup.closure {(↑σ : Perm α), τ}) ⊤
⊢ H = ⊤
have rw : (↑σ : Perm α) ∈ (↑H : Set (Perm α)) ∧ τ ∈ (↑H : Set (Perm α))
Tactic: rw [eq_top_iff, ← hσ4, Subgroup.closure_le, Set.insert_subset_iff, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn : n ∈ σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1
⊢ 0 < n
have inl : ∀ (hn : n ∈ σ.cycleType), 0 < n
Tactic: rcases mem_add.mp hn with hn | hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn : n ∈ σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1
inl : ∀ (hn : n ∈ σ.cycleType), 0 < n
⊢ 0 < n
have inr : ∀ (hn : Membership.mem (γ := Multiset ℕ) (Multiset.replicate (Fintype.card α - #σ.support) 1) n), 0 < n
Tactic: rcases mem_add.mp hn with hn | hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
⊢ (σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1).sum = Fintype.card α
have rw : σ.cycleType.sum + Multiset.sum (Multiset.replicate (Fintype.card α - #σ.support) 1) = Fintype.card α
Tactic: rw [sum_add, sum_cycleType, Multiset.sum_replicate, nsmul_eq_mul, Nat.cast_id, mul_one,
      add_tsub_cancel_of_le σ.support.card_le_univ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
rw : σ.cycleType.sum + Multiset.sum (Multiset.replicate (Fintype.card α - #σ.support) 1) = Fintype.card α
⊢ (σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1).sum = Fintype.card α
have rw₁ : #σ.support + Multiset.sum (Multiset.replicate (Fintype.card α - #σ.support) 1) = Fintype.card α
Tactic: rw [sum_add, sum_cycleType, Multiset.sum_replicate, nsmul_eq_mul, Nat.cast_id, mul_one,
      add_tsub_cancel_of_le σ.support.card_le_univ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
rw : σ.cycleType.sum + Multiset.sum (Multiset.replicate (Fintype.card α - #σ.support) 1) = Fintype.card α
rw₁ : #σ.support + Multiset.sum (Multiset.replicate (Fintype.card α - #σ.support) 1) = Fintype.card α
⊢ (σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1).sum = Fintype.card α
have rw₂ : #σ.support + HSMul.hSMul (β := ℕ) (Fintype.card α - #σ.support) 1 = Fintype.card α
Tactic: rw [sum_add, sum_cycleType, Multiset.sum_replicate, nsmul_eq_mul, Nat.cast_id, mul_one,
      add_tsub_cancel_of_le σ.support.card_le_univ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
rw : σ.cycleType.sum + Multiset.sum (Multiset.replicate (Fintype.card α - #σ.support) 1) = Fintype.card α
rw₁ : #σ.support + Multiset.sum (Multiset.replicate (Fintype.card α - #σ.support) 1) = Fintype.card α
rw₂ : #σ.support + HSMul.hSMul (β := ℕ) (Fintype.card α - #σ.support) 1 = Fintype.card α
⊢ (σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1).sum = Fintype.card α
have rw₃ : #σ.support + HMul.hMul (α := ℕ) (↑(Fintype.card α - #σ.support) : ℕ) 1 = Fintype.card α
Tactic: rw [sum_add, sum_cycleType, Multiset.sum_replicate, nsmul_eq_mul, Nat.cast_id, mul_one,
      add_tsub_cancel_of_le σ.support.card_le_univ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
rw : σ.cycleType.sum + Multiset.sum (Multiset.replicate (Fintype.card α - #σ.support) 1) = Fintype.card α
rw₁ : #σ.support + Multiset.sum (Multiset.replicate (Fintype.card α - #σ.support) 1) = Fintype.card α
rw₂ : #σ.support + HSMul.hSMul (β := ℕ) (Fintype.card α - #σ.support) 1 = Fintype.card α
rw₃ : #σ.support + HMul.hMul (α := ℕ) (↑(Fintype.card α - #σ.support) : ℕ) 1 = Fintype.card α
⊢ (σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1).sum = Fintype.card α
have rw₄ : #σ.support + (Fintype.card α - #σ.support) * 1 = Fintype.card α
Tactic: rw [sum_add, sum_cycleType, Multiset.sum_replicate, nsmul_eq_mul, Nat.cast_id, mul_one,
      add_tsub_cancel_of_le σ.support.card_le_univ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
rw : σ.cycleType.sum + Multiset.sum (Multiset.replicate (Fintype.card α - #σ.support) 1) = Fintype.card α
rw₁ : #σ.support + Multiset.sum (Multiset.replicate (Fintype.card α - #σ.support) 1) = Fintype.card α
rw₂ : #σ.support + HSMul.hSMul (β := ℕ) (Fintype.card α - #σ.support) 1 = Fintype.card α
rw₃ : #σ.support + HMul.hMul (α := ℕ) (↑(Fintype.card α - #σ.support) : ℕ) 1 = Fintype.card α
rw₄ : #σ.support + (Fintype.card α - #σ.support) * 1 = Fintype.card α
⊢ (σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1).sum = Fintype.card α
have rw₅ : #σ.support + (Fintype.card α - #σ.support) = Fintype.card α
Tactic: rw [sum_add, sum_cycleType, Multiset.sum_replicate, nsmul_eq_mul, Nat.cast_id, mul_one,
      add_tsub_cancel_of_le σ.support.card_le_univ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
rw : σ.cycleType.sum + Multiset.sum (Multiset.replicate (Fintype.card α - #σ.support) 1) = Fintype.card α
rw₁ : #σ.support + Multiset.sum (Multiset.replicate (Fintype.card α - #σ.support) 1) = Fintype.card α
rw₂ : #σ.support + HSMul.hSMul (β := ℕ) (Fintype.card α - #σ.support) 1 = Fintype.card α
rw₃ : #σ.support + HMul.hMul (α := ℕ) (↑(Fintype.card α - #σ.support) : ℕ) 1 = Fintype.card α
rw₄ : #σ.support + (Fintype.card α - #σ.support) * 1 = Fintype.card α
rw₅ : #σ.support + (Fintype.card α - #σ.support) = Fintype.card α
⊢ (σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1).sum = Fintype.card α
have rw₆ : Fintype.card α = Fintype.card α
Tactic: rw [sum_add, sum_cycleType, Multiset.sum_replicate, nsmul_eq_mul, Nat.cast_id, mul_one,
      add_tsub_cancel_of_le σ.support.card_le_univ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
⊢ Multiset.filter (fun (n : ℕ) ↦ 2 ≤ n) (Nat.Partition.parts (n := Fintype.card α) σ.partition) = σ.cycleType
have rw : ∀ (a : ℕ) (h : Membership.mem (γ := Multiset ℕ) (Multiset.replicate (Fintype.card α - #σ.support) 1) a), ¬2 ≤ a
Tactic: rw [parts_partition, filter_add, Multiset.filter_eq_self.2 fun _ => two_le_of_mem_cycleType,
    Multiset.filter_eq_nil.2 fun a h => ?_, add_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
a : ℕ
h : Membership.mem (γ := Multiset ℕ) (Multiset.replicate (Fintype.card α - #σ.support) 1) a
⊢ ¬2 ≤ a
have rw : ¬LE.le (α := ℕ) 2 1
Tactic: rw [Multiset.eq_of_mem_replicate h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
⊢ IsConj σ τ ↔ Eq (α := (Fintype.card α).Partition) σ.partition τ.partition
have rw : σ.cycleType = τ.cycleType ↔ Eq (α := (Fintype.card α).Partition) σ.partition τ.partition
Tactic: rw [isConj_iff_cycleType_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
⊢ σ.cycleType = τ.cycleType ↔ Eq (α := (Fintype.card α).Partition) σ.partition τ.partition
have refine_1 : ∀ (h : σ.cycleType = τ.cycleType), Eq (α := (Fintype.card α).Partition) σ.partition τ.partition
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
refine_1 : ∀ (h : σ.cycleType = τ.cycleType), Eq (α := (Fintype.card α).Partition) σ.partition τ.partition
⊢ σ.cycleType = τ.cycleType ↔ Eq (α := (Fintype.card α).Partition) σ.partition τ.partition
have refine_2 : ∀ (h : Eq (α := (Fintype.card α).Partition) σ.partition τ.partition), σ.cycleType = τ.cycleType
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
h : σ.cycleType = τ.cycleType
⊢ Eq (α := (Fintype.card α).Partition) σ.partition τ.partition
have refine_1 : Nat.Partition.parts (n := Fintype.card α) σ.partition = Nat.Partition.parts (n := Fintype.card α) τ.partition
Tactic: rw [Nat.Partition.ext_iff, parts_partition, parts_partition, ← sum_cycleType, ← sum_cycleType,
      h]