awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hn2 : Fintype.card α < #c.support + 2
hng : #c.support ∈ (c * g').cycleType
g'1 : g' = 1
rw : c.cycleType + g'.cycleType = {#c.support}
rw₁ : {#c.support} + g'.cycleType = {#c.support}
rw₂ : {#c.support} + cycleType.{u_1} (α := α) 1 = {#c.support}
rw₃ : HAdd.hAdd (α := Multiset ℕ) {#c.support} 0 = {#c.support}
rw₄ rw₅ : Eq (α := Multiset ℕ) {#c.support} {#c.support}
⊢ (c * g').cycleType = {#c.support}

Tactic:
rw [hd.cycleType_mul, hc.cycleType, g'1, cycleType_one, add_zero]

Premises used: Equiv.Perm.IsCycle.cycleType, Equiv.Perm.cycleType_one, Equiv.Perm.Disjoint.cycleType_mul, add_zero
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hn2 : Fintype.card α < #c.support + 2
hng : #c.support ∈ (c * g').cycleType
suffices : g' = 1
⊢ (c * g').cycleType = {#c.support}

Tactic:
suffices g'1 : g' = 1 by
    rw [hd.cycleType_mul, hc.cycleType, g'1, cycleType_one, add_zero]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hn2 : Fintype.card α < #c.support + 2
hng : #c.support ∈ (c * g').cycleType
contrapose! : ∀ (g'1 : g' ≠ 1), #c.support + 2 ≤ Fintype.card α
⊢ g' = 1

Tactic:
contrapose! hn2 with g'1
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
c g' : Perm α
hd : c.Disjoint g'
hc : c.IsCycle
hng : #c.support ∈ (c * g').cycleType
g'1 : g' ≠ 1
grw : #c.support + 2 ≤ #(c * g').support
grw₁ : #c.support + 2 ≤ #c.support + #g'.support
grw₂ grw₃ : #c.support + #g'.support ≤ #c.support + #g'.support
⊢ #c.support + 2 ≤ Fintype.card α

Tactic:
grw [← (c * g').support.card_le_univ, hd.card_support_mul, two_le_card_support_of_ne_one g'1]

Premises used: Equiv.Perm.support, HMul.hMul, Equiv.Perm.Disjoint.card_support_mul, Equiv.Perm.two_le_card_support_of_ne_one, Finset.card_le_univ
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
rw :
  (-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)
⊢ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ =
    if Odd n then 1
    else
      HPow.hPow (α := ℤˣ) (-1)
        ((Fintype.card α - Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1)) / n)

Tactic:
rw [sign_of_cycleType', hσ, Multiset.map_replicate, Multiset.prod_replicate]

Premises used: Multiset.prod_replicate, Multiset.map_replicate, Equiv.Perm.sign_of_cycleType'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
inl :
  ∀ (h : Even 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)
inr :
  ∀ (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)
⊢ (-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)

Tactic:
obtain h | h := Nat.even_or_odd n

Premises used: Nat.even_or_odd
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Even n
rw : (Multiset.replicate σ.cycleType.card n).sum = (Multiset.replicate σ.cycleType.card n).card * n
⊢ σ.cycleType.sum = σ.cycleType.card * n

Tactic:
rw [hσ]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Even n
⊢ (Multiset.replicate σ.cycleType.card n).sum = (Multiset.replicate σ.cycleType.card n).card * n

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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)
inl₅ inl₆ : HPow.hPow (α := ℤˣ) (-1) σ.cycleType.card = HPow.hPow (α := ℤˣ) (-1) σ.cycleType.card
⊢ (-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)

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]

Premises used: Iff.mpr, Nat.sub_sub_self, Nat.mul_div_cancel, Nat.not_odd_iff_even, Even.neg_one_pow, Equiv.Perm.sum_cycleType_le, Equiv.Perm.card_fixedPoints, if_neg
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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
inr₃ inr₄ : Eq (α := ℤˣ) 1 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)

Tactic:
rw [if_pos h, h.neg_one_pow, neg_neg, one_pow]

Premises used: one_pow, neg_neg, if_pos, Odd.neg_one_pow
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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)
rw₁ 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)
⊢ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ =
    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)]

Premises used: Iff.mpr, Equiv.Perm.sign_of_cycleType_eq_replicate, Nat.not_odd_iff, Equiv.Perm.cycleType_of_pow_prime_eq_one, zero_lt_two, if_neg
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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
rw₁ : #σ.supportᶜ ≤ Fintype.card α
⊢ #σ.supportᶜ ≡ Fintype.card α [MOD p]

Tactic:
rw [Nat.modEq_iff_dvd', ← Finset.card_compl, compl_compl, ← sum_cycleType]

Premises used: compl_compl, Finset.card_compl, Nat.modEq_iff_dvd', Equiv.Perm.sum_cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ p ∣ σ.cycleType.sum

Tactic:
Multiset.dvd_sum fun k hk => ?_

Premises used: Multiset.dvd_sum
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
refine : ∀ (k : ℕ) (hk : k ∈ σ.cycleType), p ∣ k
⊢ p ∣ σ.cycleType.sum

Tactic:
refine Multiset.dvd_sum fun k hk => ?_

Premises used: Multiset.dvd_sum
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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
obtain : ∀ (m : ℕ) (hm : orderOf σ = p ^ m), p ∣ k
⊢ p ∣ k

Tactic:
obtain ⟨m, -, hm⟩ := (Nat.dvd_prime_pow hp.out).mp (orderOf_dvd_of_pow_eq_one hσ)

Premises used: orderOf_dvd_of_pow_eq_one, Iff.mp, Fact.out, Nat.dvd_prime_pow
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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
obtain : ∀ (l : ℕ) (hk : p ^ l ∈ σ.cycleType), p ∣ p ^ l
⊢ p ∣ k

Tactic:
obtain ⟨l, -, rfl⟩ := (Nat.dvd_prime_pow hp.out).mp
      ((congr_arg _ hm).mp (dvd_of_mem_cycleType hk))

Premises used: Eq.mp, congr_arg, Equiv.Perm.dvd_of_mem_cycleType, Iff.mp, rfl, Fact.out, Nat.dvd_prime_pow
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ 1 = p ^ l

Tactic:
rw [h, pow_zero]

Premises used: pow_zero
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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
⊢ p ∣ p ^ l

Tactic:
exact dvd_pow_self _ fun h => (one_lt_of_mem_cycleType hk).ne <| by rw [h, pow_zero]

Premises used: dvd_pow_self, Equiv.Perm.one_lt_of_mem_cycleType, LT.lt.ne
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ #σ.supportᶜ ≤ Fintype.card α

Tactic:
Finset.card_le_univ _

Premises used: Finset.card_le_univ
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ #σ.supportᶜ ≤ Fintype.card α

Tactic:
exact Finset.card_le_univ _

Premises used: Finset.card_le_univ
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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 := ⋯ }
rw : Eq (α := (a : α) → α) (⇑σ : (a : α) → α)^[p ^ n] (⇑1 : (a : α) → α)
⊢ σ ^ p ^ n = 1

Tactic:
rw [DFunLike.ext'_iff, coe_pow]

Premises used: DFunLike.ext'_iff, Equiv.Perm.coe_pow
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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 := ⋯ }
⊢ Eq (α := (a : α) → α) (⇑σ : (a : α) → α)^[p ^ n] (⇑1 : (a : α) → α)

Tactic:
(hom_coe_pow (fun g : Function.End α ↦ g) rfl (fun g h ↦ rfl) f (p ^ n)).symm.trans hf

Premises used: hom_coe_pow, HPow.hPow, Eq.symm, rfl, Eq.trans
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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 := ⋯ }
⊢ Eq (α := (a : α) → α) (⇑σ : (a : α) → α)^[p ^ n] (⇑1 : (a : α) → α)

Tactic:
exact (hom_coe_pow (fun g : Function.End α ↦ g) rfl (fun g h ↦ rfl) f (p ^ n)).symm.trans hf

Premises used: hom_coe_pow, HPow.hPow, Eq.symm, rfl, Eq.trans
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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

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
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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
suffices : Fintype.card.{u_1} (↑(fixedPoints f) : Type u_1) = #(support σ)ᶜ
⊢ Fintype.card α ≡ Fintype.card.{u_1} (↑(fixedPoints f) : Type u_1) [MOD p]

Tactic:
suffices Fintype.card f.fixedPoints = (support σ)ᶜ.card from
    this ▸ (card_compl_support_modEq hσ).symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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 α)
simp : Fintype.card.{u_1} (↑(↑(support σ)ᶜ : Set α) : Type u_1) = #(support σ)ᶜ
⊢ Fintype.card.{u_1} (↑(fixedPoints f) : Type u_1) = #(support σ)ᶜ

Tactic:
simp only [this]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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} (↑(↑(support σ)ᶜ : Set α) : Type u_1) = #(support σ)ᶜ

Tactic:
apply Fintype.card_coe

Premises used: Fintype.card_coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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
suffices : fixedPoints f = (↑(support σ)ᶜ : Set α)
⊢ Fintype.card.{u_1} (↑(fixedPoints f) : Type u_1) = #(support σ)ᶜ

Tactic:
suffices f.fixedPoints = (support σ)ᶜ by
    simp only [this]; apply Fintype.card_coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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
⊢ fixedPoints f = (↑(support σ)ᶜ : Set α)

Tactic:
simp [σ, Set.ext_iff, IsFixedPt]

Premises used: Set.ext_iff, Function.IsFixedPt
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : ¬p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
contrapose! : ∀ (hα : ∀ (a : α), (σ : (a : α) → α) a ≠ a), p ∣ Fintype.card α
⊢ ∃ (a : α), (σ : (a : α) → α) a = a

Tactic:
contrapose! hα
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
hα : ∀ (a : α), (σ : (a : α) → α) a ≠ a
⊢ σ.support = Finset.univ

Tactic:
simp_rw [← mem_support, ← Finset.eq_univ_iff_forall] at hα

Premises used: Finset.eq_univ_iff_forall, Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
hα : σ.support = Finset.univ
⊢ p ∣ Fintype.card α

Tactic:
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)

Premises used: Iff.mpr, Eq.mp, Equiv.Perm.card_compl_support_modEq, congr_arg, Nat.ModEq.symm, Finset.card_eq_zero, Iff.mp, compl_eq_bot, Nat.modEq_zero_iff_dvd
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
hα : σ.support = Finset.univ
⊢ p ∣ Fintype.card α

Tactic:
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)

Premises used: Iff.mpr, Eq.mp, Equiv.Perm.card_compl_support_modEq, congr_arg, Nat.ModEq.symm, Finset.card_eq_zero, Iff.mp, compl_eq_bot, Nat.modEq_zero_iff_dvd
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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 α
contrapose!₅ : ∀ (hα : σ.support = Finset.univ), 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)

Premises used: Finset.eq_univ_iff_forall, Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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
rw₂ rw₃ : (σ : (a : α) → α) b = b ↔ (σ : (a : α) → α) b = b
⊢ b ∈ σ.supportᶜ ↔ (σ : (a : α) → α) b = b

Tactic:
rw [Finset.mem_compl, mem_support, Classical.not_not]

Premises used: Classical.not_not, Equiv.Perm.mem_support, Finset.mem_compl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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

Tactic:
have h : ∀ b : α, b ∈ σ.supportᶜ ↔ σ b = b := fun b => by
      rw [Finset.mem_compl, mem_support, Classical.not_not]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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
obtain : ∀ (b : α) (hb1 : b ∈ σ.supportᶜ) (hb2 : b ≠ a), ∃ (b : α), (σ : (a : α) → α) b = b ∧ 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

Premises used: Iff.mpr, Nat.Prime.one_lt, Equiv.Perm.card_compl_support_modEq, Finset.exists_mem_ne, LT.lt.trans_le, Exists.intro, Iff.mp, Finset.card_pos, Nat.modEq_zero_iff_dvd, Nat.le_of_dvd, Nat.ModEq.trans, Fact.out
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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 : α
hb1 : b ∈ σ.supportᶜ
hb2 : b ≠ a
⊢ ∃ (b : α), (σ : (a : α) → α) b = b ∧ b ≠ a

Tactic:
⟨b, (h b).mp hb1, hb2⟩

Premises used: And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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 : α
hb1 : b ∈ σ.supportᶜ
hb2 : b ≠ a
⊢ ∃ (b : α), (σ : (a : α) → α) b = b ∧ b ≠ a

Tactic:
exact ⟨b, (h b).mp hb1, hb2⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
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
have₃ :
  ∀ (h : ∀ (b : α), b ∈ σ.supportᶜ ↔ (σ : (a : α) → α) b = b) (b : α) (hb1 : b ∈ σ.supportᶜ) (hb2 : b ≠ a),
    ∃ (b : α), (σ : (a : α) → α) b = b ∧ 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⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : Fintype.card α < 2 * orderOf σ
⊢ σ.IsCycle

Tactic:
isCycle_of_prime_order h1 (lt_of_le_of_lt σ.support.card_le_univ h2)

Premises used: Equiv.Perm.support, lt_of_le_of_lt, Finset.card_le_univ, Equiv.Perm.isCycle_of_prime_order
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : Fintype.card α < 2 * orderOf σ
⊢ σ.IsCycle

Tactic:
exact isCycle_of_prime_order h1 (lt_of_le_of_lt σ.support.card_le_univ h2)

Premises used: Equiv.Perm.support, lt_of_le_of_lt, Finset.card_le_univ, Equiv.Perm.isCycle_of_prime_order
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : Fintype.card α < 2 * orderOf σ
⊢ σ.IsCycle

Tactic:
classical exact isCycle_of_prime_order h1 (lt_of_le_of_lt σ.support.card_le_univ h2)
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
σ : Perm α
h1 : Nat.Prime (Fintype.card α)
h2 : orderOf σ = Fintype.card α
rw : LT.lt (α := ℕ) 1 2
⊢ Fintype.card α < 2 * orderOf σ

Tactic:
rw [← one_mul (Fintype.card α), ← h2, mul_lt_mul_iff_left₀ (orderOf_pos σ)]

Premises used: Fintype.card, orderOf_pos, one_mul, mul_lt_mul_iff_left₀
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
σ : Perm α
h1 : Nat.Prime (Fintype.card α)
h2 : orderOf σ = Fintype.card α
⊢ LT.lt (α := ℕ) 1 2

Tactic:
one_lt_two

Premises used: one_lt_two
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
σ : Perm α
h1 : Nat.Prime (Fintype.card α)
h2 : orderOf σ = Fintype.card α
⊢ LT.lt (α := ℕ) 1 2

Tactic:
exact one_lt_two

Premises used: one_lt_two
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
G : Type u_2
inst : Group G
n : ℕ
v : List.Vector G n
⊢ v ∈ vectorsProdEqOne G n ↔ v.toList.prod = 1

Tactic:
Iff.rfl

Premises used: Set.Mem, Equiv.Perm.vectorsProdEqOne, Iff.rfl, setOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
G : Type u_2
inst : Group G
⊢ Eq (α := Set (List.Vector G 0)) (vectorsProdEqOne G 0) {Vector.nil}

Tactic:
Set.eq_singleton_iff_unique_mem.mpr ⟨Eq.refl (1 : G), fun v _ => v.eq_nil⟩

Premises used: Iff.mpr, List.Vector.eq_nil, And.intro, Eq.refl, Set.eq_singleton_iff_unique_mem, OfNat.ofNat