awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Even n
inl :
  (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card =
    HPow.hPow (α := ℤˣ) (-1)
      ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
⊢ (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card =
    if Odd n then 1
    else
      HPow.hPow (α := ℤˣ) (-1)
        ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
have inl₁ : HPow.hPow (α := ℤˣ) (-1) σ.cycleType.card =
  HPow.hPow (α := ℤˣ) (-1)
    ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
Tactic: rw [if_neg (Nat.not_odd_iff_even.mpr h), h.neg_one_pow, σ.card_fixedPoints,
      Nat.sub_sub_self σ.sum_cycleType_le,
      show σ.cycleType.sum = σ.cycleType.card * n by rw [hσ]; simp,
        Nat.mul_div_cancel _ hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Even n
inl :
  (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card =
    HPow.hPow (α := ℤˣ) (-1)
      ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
inl₁ :
  HPow.hPow (α := ℤˣ) (-1) σ.cycleType.card =
    HPow.hPow (α := ℤˣ) (-1)
      ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
⊢ (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card =
    if Odd n then 1
    else
      HPow.hPow (α := ℤˣ) (-1)
        ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
have inl₂ : HPow.hPow (α := ℤˣ) (-1) σ.cycleType.card =
  HPow.hPow (α := ℤˣ) (-1) ((Fintype.card α - (Fintype.card α - σ.cycleType.sum)) / n)
Tactic: rw [if_neg (Nat.not_odd_iff_even.mpr h), h.neg_one_pow, σ.card_fixedPoints,
      Nat.sub_sub_self σ.sum_cycleType_le,
      show σ.cycleType.sum = σ.cycleType.card * n by rw [hσ]; simp,
        Nat.mul_div_cancel _ hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Even n
inl :
  (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card =
    HPow.hPow (α := ℤˣ) (-1)
      ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
inl₁ :
  HPow.hPow (α := ℤˣ) (-1) σ.cycleType.card =
    HPow.hPow (α := ℤˣ) (-1)
      ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
inl₂ :
  HPow.hPow (α := ℤˣ) (-1) σ.cycleType.card =
    HPow.hPow (α := ℤˣ) (-1) ((Fintype.card α - (Fintype.card α - σ.cycleType.sum)) / n)
⊢ (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card =
    if Odd n then 1
    else
      HPow.hPow (α := ℤˣ) (-1)
        ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
have inl₃ : HPow.hPow (α := ℤˣ) (-1) σ.cycleType.card = HPow.hPow (α := ℤˣ) (-1) (σ.cycleType.sum / n)
Tactic: rw [if_neg (Nat.not_odd_iff_even.mpr h), h.neg_one_pow, σ.card_fixedPoints,
      Nat.sub_sub_self σ.sum_cycleType_le,
      show σ.cycleType.sum = σ.cycleType.card * n by rw [hσ]; simp,
        Nat.mul_div_cancel _ hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Even n
inl :
  (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card =
    HPow.hPow (α := ℤˣ) (-1)
      ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
inl₁ :
  HPow.hPow (α := ℤˣ) (-1) σ.cycleType.card =
    HPow.hPow (α := ℤˣ) (-1)
      ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
inl₂ :
  HPow.hPow (α := ℤˣ) (-1) σ.cycleType.card =
    HPow.hPow (α := ℤˣ) (-1) ((Fintype.card α - (Fintype.card α - σ.cycleType.sum)) / n)
inl₃ : HPow.hPow (α := ℤˣ) (-1) σ.cycleType.card = HPow.hPow (α := ℤˣ) (-1) (σ.cycleType.sum / n)
⊢ (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card =
    if Odd n then 1
    else
      HPow.hPow (α := ℤˣ) (-1)
        ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
have inl₄ : HPow.hPow (α := ℤˣ) (-1) σ.cycleType.card = HPow.hPow (α := ℤˣ) (-1) (σ.cycleType.card * n / n)
Tactic: rw [if_neg (Nat.not_odd_iff_even.mpr h), h.neg_one_pow, σ.card_fixedPoints,
      Nat.sub_sub_self σ.sum_cycleType_le,
      show σ.cycleType.sum = σ.cycleType.card * n by rw [hσ]; simp,
        Nat.mul_div_cancel _ hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Even n
inl :
  (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card =
    HPow.hPow (α := ℤˣ) (-1)
      ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
inl₁ :
  HPow.hPow (α := ℤˣ) (-1) σ.cycleType.card =
    HPow.hPow (α := ℤˣ) (-1)
      ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
inl₂ :
  HPow.hPow (α := ℤˣ) (-1) σ.cycleType.card =
    HPow.hPow (α := ℤˣ) (-1) ((Fintype.card α - (Fintype.card α - σ.cycleType.sum)) / n)
inl₃ : HPow.hPow (α := ℤˣ) (-1) σ.cycleType.card = HPow.hPow (α := ℤˣ) (-1) (σ.cycleType.sum / n)
inl₄ : HPow.hPow (α := ℤˣ) (-1) σ.cycleType.card = HPow.hPow (α := ℤˣ) (-1) (σ.cycleType.card * n / n)
⊢ (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card =
    if Odd n then 1
    else
      HPow.hPow (α := ℤˣ) (-1)
        ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
have inl₅ : HPow.hPow (α := ℤˣ) (-1) σ.cycleType.card = HPow.hPow (α := ℤˣ) (-1) σ.cycleType.card
Tactic: rw [if_neg (Nat.not_odd_iff_even.mpr h), h.neg_one_pow, σ.card_fixedPoints,
      Nat.sub_sub_self σ.sum_cycleType_le,
      show σ.cycleType.sum = σ.cycleType.card * n by rw [hσ]; simp,
        Nat.mul_div_cancel _ hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Odd n
⊢ (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card =
    if Odd n then 1
    else
      HPow.hPow (α := ℤˣ) (-1)
        ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
have inr : (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card = 1
Tactic: rw [if_pos h, h.neg_one_pow, neg_neg, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Odd n
inr : (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card = 1
⊢ (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card =
    if Odd n then 1
    else
      HPow.hPow (α := ℤˣ) (-1)
        ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
have inr₁ : HPow.hPow (α := ℤˣ) (- -1) σ.cycleType.card = 1
Tactic: rw [if_pos h, h.neg_one_pow, neg_neg, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Odd n
inr : (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card = 1
inr₁ : HPow.hPow (α := ℤˣ) (- -1) σ.cycleType.card = 1
⊢ (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card =
    if Odd n then 1
    else
      HPow.hPow (α := ℤˣ) (-1)
        ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
have inr₂ : HPow.hPow (α := ℤˣ) 1 σ.cycleType.card = 1
Tactic: rw [if_pos h, h.neg_one_pow, neg_neg, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Odd n
inr : (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card = 1
inr₁ : HPow.hPow (α := ℤˣ) (- -1) σ.cycleType.card = 1
inr₂ : HPow.hPow (α := ℤˣ) 1 σ.cycleType.card = 1
⊢ (-HPow.hPow (α := ℤˣ) (-1) n) ^ σ.cycleType.card =
    if Odd n then 1
    else
      HPow.hPow (α := ℤˣ) (-1)
        ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)
have inr₃ : Eq (α := ℤˣ) 1 1
Tactic: rw [if_pos h, h.neg_one_pow, neg_neg, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : HPow.hPow (β := ℕ) σ 2 = 1
⊢ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ =
    HPow.hPow (α := ℤˣ) (-1)
      ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / 2)
have rw : (if Odd (α := ℕ) 2 then 1
  else
    HPow.hPow (α := ℤˣ) (-1)
      ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / 2)) =
  HPow.hPow (α := ℤˣ) (-1)
    ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / 2)
Tactic: rw [sign_of_cycleType_eq_replicate zero_lt_two (cycleType_of_pow_prime_eq_one hσ),
    if_neg (Nat.not_odd_iff.mpr rfl)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : HPow.hPow (β := ℕ) σ 2 = 1
rw :
  (if Odd (α := ℕ) 2 then 1
    else
      HPow.hPow (α := ℤˣ) (-1)
        ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / 2)) =
    HPow.hPow (α := ℤˣ) (-1)
      ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / 2)
⊢ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ =
    HPow.hPow (α := ℤˣ) (-1)
      ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / 2)
have rw₁ : HPow.hPow (α := ℤˣ) (-1)
    ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / 2) =
  HPow.hPow (α := ℤˣ) (-1)
    ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / 2)
Tactic: rw [sign_of_cycleType_eq_replicate zero_lt_two (cycleType_of_pow_prime_eq_one hσ),
    if_neg (Nat.not_odd_iff.mpr rfl)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ #σ.supportᶜ ≡ Fintype.card α [MOD p]
have rw : p ∣ σ.cycleType.sum
Tactic: rw [Nat.modEq_iff_dvd', ← Finset.card_compl, compl_compl, ← sum_cycleType]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
rw : p ∣ σ.cycleType.sum
⊢ #σ.supportᶜ ≡ Fintype.card α [MOD p]
have rw₁ : #σ.supportᶜ ≤ Fintype.card α
Tactic: rw [Nat.modEq_iff_dvd', ← Finset.card_compl, compl_compl, ← sum_cycleType]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ p ∣ σ.cycleType.sum
have refine : ∀ (k : ℕ) (hk : k ∈ σ.cycleType), p ∣ k
Tactic: refine Multiset.dvd_sum fun k hk => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
k : ℕ
hk : k ∈ σ.cycleType
⊢ p ∣ k
have obtain : ∀ (m : ℕ) (hm : orderOf σ = p ^ m), p ∣ k
Tactic: obtain ⟨m, -, hm⟩ := (Nat.dvd_prime_pow hp.out).mp (orderOf_dvd_of_pow_eq_one hσ)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
k : ℕ
hk : k ∈ σ.cycleType
m : ℕ
hm : orderOf σ = p ^ m
⊢ p ∣ k
have obtain : ∀ (l : ℕ) (hk : p ^ l ∈ σ.cycleType), p ∣ p ^ l
Tactic: obtain ⟨l, -, rfl⟩ := (Nat.dvd_prime_pow hp.out).mp
      ((congr_arg _ hm).mp (dvd_of_mem_cycleType hk))
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
m : ℕ
hm : orderOf σ = p ^ m
l : ℕ
hk : p ^ l ∈ σ.cycleType
h : l = 0
⊢ 1 = p ^ l
have rw : 1 = HPow.hPow (β := ℕ) p 0
Tactic: rw [h, pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
m : ℕ
hm : orderOf σ = p ^ m
l : ℕ
hk : p ^ l ∈ σ.cycleType
h : l = 0
rw : 1 = HPow.hPow (β := ℕ) p 0
⊢ 1 = p ^ l
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [h, pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
⊢ σ ^ p ^ n = 1
have rw : Eq (α := (a : α) → α) (⇑σ : (a : α) → α)^[p ^ n] (⇑1 : (a : α) → α)
Tactic: rw [DFunLike.ext'_iff, coe_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
⊢ Fintype.card α ≡ Fintype.card.{u_1} (↑(fixedPoints f) : Type u_1) [MOD p]
have hσ : σ ^ p ^ n = 1
Tactic: have hσ : σ ^ p ^ n = 1 := by
    rw [DFunLike.ext'_iff, coe_pow]
    exact (hom_coe_pow (fun g : Function.End α ↦ g) rfl (fun g h ↦ rfl) f (p ^ n)).symm.trans hf
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ n = 1
⊢ Fintype.card α ≡ Fintype.card.{u_1} (↑(fixedPoints f) : Type u_1) [MOD p]
have suffices : Fintype.card.{u_1} (↑(fixedPoints f) : Type u_1) = #(support σ)ᶜ
Tactic: suffices Fintype.card f.fixedPoints = (support σ)ᶜ.card from
    this ▸ (card_compl_support_modEq hσ).symm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ n = 1
this : fixedPoints f = (↑(support σ)ᶜ : Set α)
⊢ Fintype.card.{u_1} (↑(fixedPoints f) : Type u_1) = #(support σ)ᶜ
have simp : Fintype.card.{u_1} (↑(↑(support σ)ᶜ : Set α) : Type u_1) = #(support σ)ᶜ
Tactic: simp only [this]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ n = 1
⊢ Fintype.card.{u_1} (↑(fixedPoints f) : Type u_1) = #(support σ)ᶜ
have suffices : fixedPoints f = (↑(support σ)ᶜ : Set α)
Tactic: suffices f.fixedPoints = (support σ)ᶜ by
    simp only [this]; apply Fintype.card_coe
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : ¬p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ ∃ (a : α), (σ : (a : α) → α) a = a
have contrapose! : ∀ (hα : ∀ (a : α), (σ : (a : α) → α) a ≠ a), p ∣ Fintype.card α
Tactic: contrapose! hα
Cleared hypotheses: hα
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
hα : ∀ (a : α), (σ : (a : α) → α) a ≠ a
⊢ p ∣ Fintype.card α
have hα₁ : σ.support = Finset.univ
Tactic: simp_rw [← mem_support, ← Finset.eq_univ_iff_forall] at hα
Cleared hypotheses: hα
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : ¬p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ ∃ (a : α), (σ : (a : α) → α) a = a
have contrapose! : ∀ (hα : ¬p ∣ Fintype.card α), ∃ (a : α), (σ : (a : α) → α) a = a
Tactic: classical
    contrapose! hα
    simp_rw [← mem_support, ← Finset.eq_univ_iff_forall] at hα
    exact Nat.modEq_zero_iff_dvd.1 ((congr_arg _ (Finset.card_eq_zero.2 (compl_eq_bot.2 hα))).mp
      (card_compl_support_modEq hσ).symm)
Cleared hypotheses: hα
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : ¬p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
contrapose! contrapose!₁ : ∀ (hα : ¬p ∣ Fintype.card α), ∃ (a : α), (σ : (a : α) → α) a = a
⊢ ∃ (a : α), (σ : (a : α) → α) a = a
have contrapose!₂ : (∀ (a : α), (σ : (a : α) → α) a ≠ a) → p ∣ Fintype.card α
Tactic: classical
    contrapose! hα
    simp_rw [← mem_support, ← Finset.eq_univ_iff_forall] at hα
    exact Nat.modEq_zero_iff_dvd.1 ((congr_arg _ (Finset.card_eq_zero.2 (compl_eq_bot.2 hα))).mp
      (card_compl_support_modEq hσ).symm)
Cleared hypotheses: hα
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : ¬p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
contrapose! contrapose!₁ : ∀ (hα : ¬p ∣ Fintype.card α), ∃ (a : α), (σ : (a : α) → α) a = a
contrapose!₂ contrapose!₃ contrapose!₄ : ∀ (hα : ∀ (a : α), (σ : (a : α) → α) a ≠ a), p ∣ Fintype.card α
⊢ ∃ (a : α), (σ : (a : α) → α) a = a
have contrapose!₅ : ∀ (hα : σ.support = Finset.univ), p ∣ Fintype.card α
Tactic: classical
    contrapose! hα
    simp_rw [← mem_support, ← Finset.eq_univ_iff_forall] at hα
    exact Nat.modEq_zero_iff_dvd.1 ((congr_arg _ (Finset.card_eq_zero.2 (compl_eq_bot.2 hα))).mp
      (card_compl_support_modEq hσ).symm)
Cleared hypotheses: hα
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : (σ : (a : α) → α) a = a
b : α
⊢ b ∈ σ.supportᶜ ↔ (σ : (a : α) → α) b = b
have rw : b ∉ σ.support ↔ (σ : (a : α) → α) b = b
Tactic: rw [Finset.mem_compl, mem_support, Classical.not_not]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : (σ : (a : α) → α) a = a
b : α
rw : b ∉ σ.support ↔ (σ : (a : α) → α) b = b
⊢ b ∈ σ.supportᶜ ↔ (σ : (a : α) → α) b = b
have rw₁ : ¬(σ : (a : α) → α) b ≠ b ↔ (σ : (a : α) → α) b = b
Tactic: rw [Finset.mem_compl, mem_support, Classical.not_not]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : (σ : (a : α) → α) a = a
b : α
rw : b ∉ σ.support ↔ (σ : (a : α) → α) b = b
rw₁ : ¬(σ : (a : α) → α) b ≠ b ↔ (σ : (a : α) → α) b = b
⊢ b ∈ σ.supportᶜ ↔ (σ : (a : α) → α) b = b
have rw₂ : (σ : (a : α) → α) b = b ↔ (σ : (a : α) → α) b = b
Tactic: rw [Finset.mem_compl, mem_support, Classical.not_not]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : (σ : (a : α) → α) a = a
⊢ ∃ (b : α), (σ : (a : α) → α) b = b ∧ b ≠ a
have h : ∀ (b : α), b ∈ σ.supportᶜ ↔ (σ : (a : α) → α) b = b
Tactic: have h : ∀ b : α, b ∈ σ.supportᶜ ↔ σ b = b := fun b => by
      rw [Finset.mem_compl, mem_support, Classical.not_not]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : (σ : (a : α) → α) a = a
h : ∀ (b : α), b ∈ σ.supportᶜ ↔ (σ : (a : α) → α) b = b
⊢ ∃ (b : α), (σ : (a : α) → α) b = b ∧ b ≠ a
have obtain : ∀ (b : α) (hb1 : b ∈ σ.supportᶜ) (hb2 : b ≠ a), ∃ (b : α), (σ : (a : α) → α) b = b ∧ b ≠ a
Tactic: obtain ⟨b, hb1, hb2⟩ := Finset.exists_mem_ne (hp.out.one_lt.trans_le
      (Nat.le_of_dvd (Finset.card_pos.mpr ⟨a, (h a).mpr ha⟩) (Nat.modEq_zero_iff_dvd.mp
        ((card_compl_support_modEq hσ).trans (Nat.modEq_zero_iff_dvd.mpr hα))))) a
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : (σ : (a : α) → α) a = a
⊢ ∃ (b : α), (σ : (a : α) → α) b = b ∧ b ≠ a
have have : ∀ (h : ∀ (b : α), b ∈ σ.supportᶜ ↔ (σ : (a : α) → α) b = b), ∃ (b : α), (σ : (a : α) → α) b = b ∧ b ≠ a
Tactic: classical
    have h : ∀ b : α, b ∈ σ.supportᶜ ↔ σ b = b := fun b => by
      rw [Finset.mem_compl, mem_support, Classical.not_not]
    obtain ⟨b, hb1, hb2⟩ := Finset.exists_mem_ne (hp.out.one_lt.trans_le
      (Nat.le_of_dvd (Finset.card_pos.mpr ⟨a, (h a).mpr ha⟩) (Nat.modEq_zero_iff_dvd.mp
        ((card_compl_support_modEq hσ).trans (Nat.modEq_zero_iff_dvd.mpr hα))))) a
    exact ⟨b, (h b).mp hb1, hb2⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : (σ : (a : α) → α) a = a
have have₁ have₂ :
  ∀ (h : ∀ (b : α), b ∈ σ.supportᶜ ↔ (σ : (a : α) → α) b = b), ∃ (b : α), (σ : (a : α) → α) b = b ∧ b ≠ a
⊢ ∃ (b : α), (σ : (a : α) → α) b = b ∧ b ≠ a
have have₃ : ∀ (h : ∀ (b : α), b ∈ σ.supportᶜ ↔ (σ : (a : α) → α) b = b) (b : α) (hb1 : b ∈ σ.supportᶜ) (hb2 : b ≠ a),
  ∃ (b : α), (σ : (a : α) → α) b = b ∧ b ≠ a
Tactic: classical
    have h : ∀ b : α, b ∈ σ.supportᶜ ↔ σ b = b := fun b => by
      rw [Finset.mem_compl, mem_support, Classical.not_not]
    obtain ⟨b, hb1, hb2⟩ := Finset.exists_mem_ne (hp.out.one_lt.trans_le
      (Nat.le_of_dvd (Finset.card_pos.mpr ⟨a, (h a).mpr ha⟩) (Nat.modEq_zero_iff_dvd.mp
        ((card_compl_support_modEq hσ).trans (Nat.modEq_zero_iff_dvd.mpr hα))))) a
    exact ⟨b, (h b).mp hb1, hb2⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
σ : Perm α
h1 : Nat.Prime (Fintype.card α)
h2 : orderOf σ = Fintype.card α
⊢ Fintype.card α < 2 * orderOf σ
have rw : LT.lt (α := ℕ) 1 2
Tactic: rw [← one_mul (Fintype.card α), ← h2, mul_lt_mul_iff_left₀ (orderOf_pos σ)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
G : Type u_2
inst : Group G
⊢ Eq (α := Set (List.Vector G 1)) (vectorsProdEqOne G 1) {1 ::ᵥ Vector.nil}
have simp_rw : ∀ (x : List.Vector G 1), x.head = 1 → x = 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]
-- 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 : ℕ
⊢ Unique (↑(vectorsProdEqOne G 0) : Type u_2)
have rw : Unique (↑{Vector.nil} : Type u_2)
Tactic: rw [zero_eq]
-- 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 : ℕ
⊢ Unique (↑(vectorsProdEqOne G 1) : Type u_2)
have rw : Unique (↑{1 ::ᵥ Vector.nil} : Type u_2)
Tactic: rw [one_eq]