awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ σ.cycleType
⊢ ∃ (a : Perm α),
    (a.IsCycle ∧ ∀ a_1 ∈ a.support, Eq (α := α) ((a : (a : α) → α) a_1 : α) ((σ : (a : α) → α) a_1 : α)) ∧
      #a.support = n

Tactic:
simp only [cycleType_def, ← Finset.mem_def, Function.comp_apply, Multiset.mem_map,
    mem_cycleFactorsFinset_iff] at h

Premises used: Multiset.mem_map, Equiv.Perm.mem_cycleFactorsFinset_iff, Function.comp_apply, Equiv.Perm.cycleType_def, Finset.mem_def
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
h :
  ∃ (a : Perm α),
    (a.IsCycle ∧ ∀ a_1 ∈ a.support, Eq (α := α) ((a : (a : α) → α) a_1 : α) ((σ : (a : α) → α) a_1 : α)) ∧
      #a.support = n
obtain : ∀ (w : Perm α) (hc : w.IsCycle), 2 ≤ #w.support
⊢ 2 ≤ n

Tactic:
obtain ⟨_, ⟨hc, -⟩, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ w : Perm α
hc : w.IsCycle
⊢ 2 ≤ #w.support

Tactic:
hc.two_le_card_support

Premises used: Equiv.Perm.IsCycle.two_le_card_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ w : Perm α
hc : w.IsCycle
⊢ 2 ≤ #w.support

Tactic:
exact hc.two_le_card_support

Premises used: Equiv.Perm.IsCycle.two_le_card_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ σ.cycleType
⊢ 1 < n

Tactic:
two_le_of_mem_cycleType h

Premises used: Equiv.Perm.two_le_of_mem_cycleType, Nat.lt
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
⊢ σ.cycleType = {#σ.support}

Tactic:
cycleType_eq [σ] (mul_one σ) (fun _τ hτ => (congr_arg IsCycle (List.mem_singleton.mp hτ)).mpr hσ)
    (List.pairwise_singleton Disjoint σ)

Premises used: Eq.mpr, Equiv.Perm.cycleType_eq, List.map, Multiset.cons, List.mem_singleton, List.cons, congr_arg, Multiset.ofList, Equiv.Perm.IsCycle, Iff.mp, Finset.card, Multiset.card, List.pairwise_singleton, mul_one, Equiv.Perm.Disjoint, List.nil
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
rw : (∃ (a : ℕ), σ.cycleType = {a}) ↔ σ.IsCycle
⊢ σ.cycleType.card = 1 ↔ σ.IsCycle

Tactic:
rw [card_eq_one]

Premises used: Multiset.card_eq_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
simp_rw : (∃ (a : ℕ) (a_1 : Perm α), (σ.IsCycle ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a) ↔ σ.IsCycle
⊢ (∃ (a : ℕ), σ.cycleType = {a}) ↔ σ.IsCycle

Tactic:
simp_rw [cycleType_def, Multiset.map_eq_singleton, ← Finset.singleton_val, Finset.val_inj,
    cycleFactorsFinset_eq_singleton_iff]

Premises used: Finset.singleton_val, Equiv.Perm.cycleFactorsFinset_eq_singleton_iff, Equiv.Perm.cycleType_def, Finset.val_inj, Multiset.map_eq_singleton
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
⊢ (∃ (a : ℕ) (a_1 : Perm α), (σ.IsCycle ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a) ↔ σ.IsCycle

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
h : σ.Disjoint τ
rw : _root_.Disjoint σ.cycleFactorsFinset.val τ.cycleFactorsFinset.val
⊢ (σ * τ).cycleType = σ.cycleType + τ.cycleType

Tactic:
rw [cycleType_def, cycleType_def, cycleType_def, h.cycleFactorsFinset_mul_eq_union, ←
    Multiset.map_add, Finset.union_val, Multiset.add_eq_union_iff_disjoint.mpr _]

Premises used: Iff.mpr, Multiset.add_eq_union_iff_disjoint, Finset.union_val, Equiv.Perm.cycleType_def, Equiv.Perm.Disjoint.cycleFactorsFinset_mul_eq_union, Multiset.map_add
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
h : σ.Disjoint τ
⊢ _root_.Disjoint σ.cycleFactorsFinset.val τ.cycleFactorsFinset.val

Tactic:
Finset.disjoint_val.2 h.disjoint_cycleFactorsFinset

Premises used: Iff.mpr, Equiv.Perm.Disjoint.disjoint_cycleFactorsFinset, Finset.disjoint_val
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
h : σ.Disjoint τ
⊢ _root_.Disjoint σ.cycleFactorsFinset.val τ.cycleFactorsFinset.val

Tactic:
exact Finset.disjoint_val.2 h.disjoint_cycleFactorsFinset

Premises used: Iff.mpr, Equiv.Perm.Disjoint.disjoint_cycleFactorsFinset, Finset.disjoint_val
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ_1 σ : Perm α
hσ : σ.IsCycle
⊢ (fun (τ : Perm α) ↦ τ⁻¹.cycleType = τ.cycleType) σ

Tactic:
simp only [hσ.cycleType, hσ.inv.cycleType, support_inv]

Premises used: Equiv.Perm.IsCycle.cycleType, Equiv.Perm.support_inv, Equiv.Perm.IsCycle.inv
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ_1 σ τ : Perm α
hστ : σ.Disjoint τ
h : σ.IsCycle
hσ : (fun (τ : Perm α) ↦ τ⁻¹.cycleType = τ.cycleType) σ
hτ : (fun (τ : Perm α) ↦ τ⁻¹.cycleType = τ.cycleType) τ
⊢ (fun (τ : Perm α) ↦ τ⁻¹.cycleType = τ.cycleType) (σ * τ)

Tactic:
simp only [mul_inv_rev, hστ.cycleType_mul, hστ.symm.inv_left.inv_right.cycleType_mul, hσ, hτ,
        add_comm]

Premises used: Equiv.Perm.Disjoint.symm, Equiv.Perm.Disjoint.inv_right, add_comm, Equiv.Perm.Disjoint.inv_left, Equiv.Perm.Disjoint.cycleType_mul, mul_inv_rev
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
τ : Perm α
⊢ (τ * 1 * τ⁻¹).cycleType = cycleType.{u_1} (α := α) 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
τ σ : Perm α
hσ : σ.IsCycle
base_cycles : (τ * σ * τ⁻¹).cycleType = {#σ.support}
base_cycles₁ : Eq (α := Multiset ℕ) {#(τ * σ * τ⁻¹).support} {#σ.support}
base_cycles₂ base_cycles₃ : Eq (α := Multiset ℕ) {#σ.support} {#σ.support}
⊢ (τ * σ * τ⁻¹).cycleType = σ.cycleType

Tactic:
rw [hσ.cycleType, hσ.conj.cycleType, card_support_conj]

Premises used: Equiv.Perm.IsCycle.conj, Equiv.Perm.IsCycle.cycleType, Equiv.Perm.card_support_conj
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
τ σ π : Perm α
hd : σ.Disjoint π
h : σ.IsCycle
hσ : (τ * σ * τ⁻¹).cycleType = σ.cycleType
hπ : (τ * π * τ⁻¹).cycleType = π.cycleType
induction_disjoint : (τ * σ * τ⁻¹ * (τ * π * τ⁻¹)).cycleType = (σ * π).cycleType
induction_disjoint₁ : (τ * σ * τ⁻¹ * (τ * π * τ⁻¹)).cycleType = σ.cycleType + π.cycleType
induction_disjoint₂ : (τ * σ * τ⁻¹).cycleType + (τ * π * τ⁻¹).cycleType = σ.cycleType + π.cycleType
induction_disjoint₃ : σ.cycleType + (τ * π * τ⁻¹).cycleType = σ.cycleType + π.cycleType
induction_disjoint₄ induction_disjoint₅ : σ.cycleType + π.cycleType = σ.cycleType + π.cycleType
⊢ (τ * (σ * π) * τ⁻¹).cycleType = (σ * π).cycleType

Tactic:
rw [← conj_mul, hd.cycleType_mul, (hd.conj _).cycleType_mul, hσ, hπ]

Premises used: conj_mul, Equiv.Perm.Disjoint.conj, Equiv.Perm.Disjoint.cycleType_mul
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
base_one : (τ * 1 * τ⁻¹).cycleType = cycleType.{u_1} (α := α) 1
base_cycles : ∀ (σ : Perm α) (hσ : σ.IsCycle), (τ * σ * τ⁻¹).cycleType = σ.cycleType
induction_disjoint :
  ∀ (σ π : Perm α) (hd : σ.Disjoint π),
    σ.IsCycle →
      ∀ (hσ : (τ * σ * τ⁻¹).cycleType = σ.cycleType) (hπ : (τ * π * τ⁻¹).cycleType = π.cycleType),
        (τ * (σ * π) * τ⁻¹).cycleType = (σ * π).cycleType
⊢ (τ * σ * τ⁻¹).cycleType = σ.cycleType

Tactic:
induction σ using cycle_induction_on with
  | base_one => simp
  | base_cycles σ hσ => rw [hσ.cycleType, hσ.conj.cycleType, card_support_conj]
  | induction_disjoint σ π hd _ hσ hπ =>
    rw [← conj_mul, hd.cycleType_mul, (hd.conj _).cycleType_mul, hσ, hπ]

Premises used: conj_mul, Equiv.Perm.card_support_conj
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
⊢ (cycleType.{u_1} (α := α) 1).sum = Finset.card.{u_1} (α := α) (support 1)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
base_cycles : Multiset.sum {#σ.support} = #σ.support
base_cycles₁ base_cycles₂ : #σ.support = #σ.support
⊢ σ.cycleType.sum = #σ.support

Tactic:
rw [hσ.cycleType, Multiset.sum_singleton]

Premises used: Equiv.Perm.IsCycle.cycleType, Multiset.sum_singleton
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : σ.cycleType.sum = #σ.support
hτ : τ.cycleType.sum = #τ.support
induction_disjoint : (σ.cycleType + τ.cycleType).sum = #(σ * τ).support
induction_disjoint₁ : σ.cycleType.sum + τ.cycleType.sum = #(σ * τ).support
induction_disjoint₂ : #σ.support + τ.cycleType.sum = #(σ * τ).support
induction_disjoint₃ : #σ.support + #τ.support = #(σ * τ).support
induction_disjoint₄ induction_disjoint₅ : #σ.support + #τ.support = #σ.support + #τ.support
⊢ (σ * τ).cycleType.sum = #(σ * τ).support

Tactic:
rw [hd.cycleType_mul, sum_add, hσ, hτ, hd.card_support_mul]

Premises used: Multiset.sum_add, Equiv.Perm.Disjoint.card_support_mul, Equiv.Perm.Disjoint.cycleType_mul
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
base_one : (cycleType.{u_1} (α := α) 1).sum = Finset.card.{u_1} (α := α) (support 1)
base_cycles : ∀ (σ : Perm α) (hσ : σ.IsCycle), σ.cycleType.sum = #σ.support
induction_disjoint :
  ∀ (σ τ : Perm α) (hd : σ.Disjoint τ),
    σ.IsCycle →
      ∀ (hσ : σ.cycleType.sum = #σ.support) (hτ : τ.cycleType.sum = #τ.support),
        (σ * τ).cycleType.sum = #(σ * τ).support
⊢ σ.cycleType.sum = #σ.support

Tactic:
induction σ using cycle_induction_on with
  | base_one => simp
  | base_cycles σ hσ => rw [hσ.cycleType, Multiset.sum_singleton]
  | induction_disjoint σ τ hd _ hσ hτ => rw [hd.cycleType_mul, sum_add, hσ, hτ, hd.card_support_mul]

Premises used: Multiset.sum_add, Multiset.sum_singleton
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
⊢ σ.cycleType.sum ≤ Fintype.card α

Tactic:
σ.sum_cycleType ▸ Finset.card_le_univ σ.support

Premises used: Equiv.Perm.support, Eq.rec, Finset.card_le_univ, Equiv.Perm.sum_cycleType, Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
rw : #(Finset.filter (Membership.mem (γ := Set α) (Function.fixedPoints (⇑σ : (a : α) → α))) Finset.univ) = #σ.supportᶜ
⊢ Fintype.card.{u_1} (↑(Function.fixedPoints (⇑σ : (a : α) → α)) : Type u_1) = Fintype.card α - σ.cycleType.sum

Tactic:
rw [Equiv.Perm.sum_cycleType, ← Finset.card_compl, Fintype.card_ofFinset]

Premises used: Fintype.card_ofFinset, Finset.card_compl, Equiv.Perm.sum_cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
e_s : Finset.filter (Membership.mem (γ := Set α) (Function.fixedPoints (⇑σ : (a : α) → α))) Finset.univ = σ.supportᶜ
⊢ #(Finset.filter (Membership.mem (γ := Set α) (Function.fixedPoints (⇑σ : (a : α) → α))) Finset.univ) = #σ.supportᶜ

Tactic:
congr
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
⊢ Finset.filter (Membership.mem (γ := Set α) (Function.fixedPoints (⇑σ : (a : α) → α))) Finset.univ = σ.supportᶜ

Tactic:
aesop
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) 1)
    (Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) (cycleType.{u_1} (α := α) 1)))

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ)
    (Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) σ.cycleType) : ℤˣ)

Tactic:
simp [hσ.cycleType, hσ.sign]

Premises used: Equiv.Perm.IsCycle.cycleType, Equiv.Perm.IsCycle.sign
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ :
  Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ)
    (Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) σ.cycleType) : ℤˣ)
hτ :
  Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) τ : ℤˣ)
    (Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) τ.cycleType) : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (σ * τ) : ℤˣ)
    (Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) (σ * τ).cycleType) : ℤˣ)

Tactic:
simp [hσ, hτ, hd.cycleType_mul]

Premises used: Equiv.Perm.Disjoint.cycleType_mul
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
base_one :
  Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) 1)
    (Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) (cycleType.{u_1} (α := α) 1)))
base_cycles :
  ∀ (σ : Perm α) (hσ : σ.IsCycle),
    Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ)
      (Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) σ.cycleType) : ℤˣ)
induction_disjoint :
  ∀ (σ τ : Perm α) (hd : σ.Disjoint τ),
    σ.IsCycle →
      ∀
        (hσ :
          Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ)
            (Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) σ.cycleType) : ℤˣ))
        (hτ :
          Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) τ : ℤˣ)
            (Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) τ.cycleType) : ℤˣ)),
        Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (σ * τ) : ℤˣ)
          (Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) (σ * τ).cycleType) : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ)
    (Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) σ.cycleType) : ℤˣ)

Tactic:
induction σ using cycle_induction_on with
  | base_one => simp
  | base_cycles σ hσ => simp [hσ.cycleType, hσ.sign]
  | induction_disjoint σ τ hd _ hσ hτ => simp [hσ, hτ, hd.cycleType_mul]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
rw :
  Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) f.cycleType) =
    HPow.hPow (α := ℤˣ) (-1) (f.cycleType.sum + f.cycleType.card)
⊢ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f = HPow.hPow (α := ℤˣ) (-1) (f.cycleType.sum + f.cycleType.card)

Tactic:
rw [sign_of_cycleType']

Premises used: Equiv.Perm.sign_of_cycleType'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
⊢ Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) 0) =
    HPow.hPow (α := ℤˣ) (-1) (Multiset.sum 0 + card (α := ℕ) 0)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs :
  Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) s) = HPow.hPow (α := ℤˣ) (-1) (s.sum + s.card)
cons :
  -HPow.hPow (α := ℤˣ) (-1) a * HPow.hPow (α := ℤˣ) (-1) (s.sum + s.card) =
    HPow.hPow (α := ℤˣ) (-1) (a + s.sum + (s.card + 1))
⊢ Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) (a ::ₘ s)) =
    HPow.hPow (α := ℤˣ) (-1) ((a ::ₘ s).sum + (a ::ₘ s).card)

Tactic:
rw [Multiset.map_cons, Multiset.prod_cons, Multiset.sum_cons, Multiset.card_cons, ihs]

Premises used: Multiset.map_cons, Multiset.prod_cons, Multiset.card_cons, Multiset.sum_cons
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs :
  Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) s) = HPow.hPow (α := ℤˣ) (-1) (s.sum + s.card)
⊢ -HPow.hPow (α := ℤˣ) (-1) a * HPow.hPow (α := ℤˣ) (-1) (s.sum + s.card) =
    HPow.hPow (α := ℤˣ) (-1) (a + s.sum + (s.card + 1))

Tactic:
simp only [pow_add, pow_one, neg_mul, mul_neg, mul_assoc, mul_one]

Premises used: mul_assoc, pow_add, pow_one, neg_mul, mul_one, mul_neg
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
induction :
  ∀ (x : Multiset ℕ),
    Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) x) =
      HPow.hPow (α := ℤˣ) (-1) (x.sum + x.card)
⊢ Multiset.prod (Multiset.map (fun (n : ℕ) ↦ -HPow.hPow (α := ℤˣ) (-1) n) f.cycleType) =
    HPow.hPow (α := ℤˣ) (-1) (f.cycleType.sum + f.cycleType.card)

Tactic:
induction f.cycleType using Multiset.induction_on with
  | empty => rfl
  | cons a s ihs =>
    rw [Multiset.map_cons, Multiset.prod_cons, Multiset.sum_cons, Multiset.card_cons, ihs]
    simp only [pow_add, pow_one, neg_mul, mul_neg, mul_assoc, mul_one]

Premises used: Equiv.Perm.cycleType, Multiset.map_cons, Multiset.prod_cons, mul_assoc, pow_add, Multiset.card_cons, pow_one, Multiset.sum_cons, neg_mul, mul_one, mul_neg
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
⊢ (cycleType.{u_1} (α := α) 1).lcm = orderOf.{u_1} (G := Perm α) 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
⊢ σ.cycleType.lcm = orderOf σ

Tactic:
simp [hσ.cycleType, hσ.orderOf]

Premises used: Equiv.Perm.IsCycle.cycleType, Equiv.Perm.IsCycle.orderOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : σ.cycleType.lcm = orderOf σ
hτ : τ.cycleType.lcm = orderOf τ
⊢ (σ * τ).cycleType.lcm = orderOf (σ * τ)

Tactic:
simp [hd.cycleType_mul, hd.orderOf, lcm_eq_nat_lcm, hσ, hτ]

Premises used: lcm_eq_nat_lcm, Equiv.Perm.Disjoint.cycleType_mul, Equiv.Perm.Disjoint.orderOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
base_one : (cycleType.{u_1} (α := α) 1).lcm = orderOf.{u_1} (G := Perm α) 1
base_cycles : ∀ (σ : Perm α) (hσ : σ.IsCycle), σ.cycleType.lcm = orderOf σ
induction_disjoint :
  ∀ (σ τ : Perm α) (hd : σ.Disjoint τ),
    σ.IsCycle →
      ∀ (hσ : σ.cycleType.lcm = orderOf σ) (hτ : τ.cycleType.lcm = orderOf τ), (σ * τ).cycleType.lcm = orderOf (σ * τ)
⊢ σ.cycleType.lcm = orderOf σ

Tactic:
induction σ using cycle_induction_on with
  | base_one => simp
  | base_cycles σ hσ => simp [hσ.cycleType, hσ.orderOf]
  | induction_disjoint σ τ hd _ hσ hτ => simp [hd.cycleType_mul, hd.orderOf, lcm_eq_nat_lcm, hσ, hτ]

Premises used: lcm_eq_nat_lcm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ σ.cycleType
rw : n ∣ σ.cycleType.lcm
⊢ n ∣ orderOf σ

Tactic:
rw [← lcm_cycleType]

Premises used: Equiv.Perm.lcm_cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ σ.cycleType
⊢ n ∣ σ.cycleType.lcm

Tactic:
dvd_lcm h

Premises used: Multiset.dvd_lcm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ σ.cycleType
⊢ n ∣ σ.cycleType.lcm

Tactic:
exact dvd_lcm h

Premises used: Multiset.dvd_lcm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
pos : ∀ (hx : (f : (a : α) → α) x = x), orderOf (f.cycleOf x) ∣ orderOf f
neg : ∀ (hx : ¬(f : (a : α) → α) x = x), orderOf (f.cycleOf x) ∣ orderOf f
⊢ orderOf (f.cycleOf x) ∣ orderOf f

Tactic:
by_cases hx : f x = x

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : (f : (a : α) → α) x = x
⊢ f.cycleOf x = 1

Tactic:
rw [← cycleOf_eq_one_iff] at hx

Premises used: Equiv.Perm.cycleOf_eq_one_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : f.cycleOf x = 1
⊢ orderOf (f.cycleOf x) ∣ orderOf f

Tactic:
simp [hx]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
⊢ orderOf (f.cycleOf x) ∣ orderOf f

Tactic:
dvd_of_mem_cycleType ?_

Premises used: Equiv.Perm.dvd_of_mem_cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
neg : orderOf (f.cycleOf x) ∈ f.cycleType
⊢ orderOf (f.cycleOf x) ∣ orderOf f

Tactic:
refine dvd_of_mem_cycleType ?_

Premises used: Equiv.Perm.dvd_of_mem_cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
neg : ∃ a ∈ f.cycleFactorsFinset.val, (Finset.card ∘ support) a = orderOf (f.cycleOf x)
⊢ orderOf (f.cycleOf x) ∈ f.cycleType

Tactic:
rw [cycleType, Multiset.mem_map]

Premises used: Equiv.Perm.cycleType, Multiset.mem_map
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
⊢ ∃ a ∈ f.cycleFactorsFinset.val, (Finset.card ∘ support) a = orderOf (f.cycleOf x)

Tactic:
⟨f.cycleOf x, ?_, ?_⟩

Premises used: And.intro, Exists.intro, Equiv.Perm.cycleOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
neg : f.cycleOf x ∈ f.cycleFactorsFinset.val
neg₁ : (Finset.card ∘ support) (f.cycleOf x) = orderOf (f.cycleOf x)
⊢ ∃ a ∈ f.cycleFactorsFinset.val, (Finset.card ∘ support) a = orderOf (f.cycleOf x)

Tactic:
refine ⟨f.cycleOf x, ?_, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
neg : f.cycleOf x ∈ f.cycleFactorsFinset
neg₁ : x ∈ f.support
neg₂ neg₃ neg₄ neg₅ : (f : (a : α) → α) x ≠ x
⊢ f.cycleOf x ∈ f.cycleFactorsFinset.val

Tactic:
rwa [← Finset.mem_def, cycleOf_mem_cycleFactorsFinset_iff, mem_support]

Premises used: Equiv.Perm.mem_support, Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff, Finset.mem_def
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
⊢ (Finset.card ∘ support) (f.cycleOf x) = orderOf (f.cycleOf x)

Tactic:
simp [(isCycle_cycleOf _ hx).orderOf]

Premises used: Equiv.Perm.isCycle_cycleOf, Equiv.Perm.IsCycle.orderOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : HPow.hPow (β := ℕ) σ 2 = 1
n : ℕ
hn : n ∈ σ.cycleType
rw rw₁ : Dvd.dvd (α := ℕ) 2 2
⊢ 2 ∣ n

Tactic:
rw [_root_.le_antisymm
          (Nat.le_of_dvd zero_lt_two <|
            (dvd_of_mem_cycleType hn).trans <| orderOf_dvd_of_pow_eq_one hσ)
          (two_le_of_mem_cycleType hn)]

Premises used: orderOf_dvd_of_pow_eq_one, le_antisymm, Equiv.Perm.two_le_of_mem_cycleType, Equiv.Perm.dvd_of_mem_cycleType, zero_lt_two, Nat.le_of_dvd, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ ∃ (n : ℕ), σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)

Tactic:
⟨Multiset.card σ.cycleType - 1, eq_replicate.2 ⟨?_, fun n hn ↦ ?_⟩⟩

Premises used: Iff.mpr, Equiv.Perm.cycleType, HSub.hSub, Multiset.eq_replicate, And.intro, Exists.intro, Multiset.card, OfNat.ofNat