awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ
hπ : ∀ {τ : Perm α} (h : π.cycleType = τ.cycleType), IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
induction_disjoint : IsConj (σ * π) (σ' * (τ * σ'⁻¹))
⊢ IsConj (σ * π) (σ' * τ * σ'⁻¹)

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ
hπ : ∀ {τ : Perm α} (h : π.cycleType = τ.cycleType), IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ σ'.IsCycle ∧ ∀ a ∈ σ'.support, Eq (α := α) ((σ' : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)

Tactic:
rw [← Finset.mem_def, mem_cycleFactorsFinset_iff] at hσ'l

Premises used: Equiv.Perm.mem_cycleFactorsFinset_iff, Finset.mem_def
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ
hπ : ∀ {τ : Perm α} (h : π.cycleType = τ.cycleType), IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
hσ'l₁ : σ'.IsCycle ∧ ∀ a ∈ σ'.support, Eq (α := α) ((σ' : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
⊢ (Finset.card ∘ support) σ' = #σ.support

Tactic:
rw [← Finset.mem_def, mem_cycleFactorsFinset_iff] at hσ'l

Premises used: Equiv.Perm.mem_cycleFactorsFinset_iff, Finset.mem_def
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ
hπ : ∀ {τ : Perm α} (h : π.cycleType = τ.cycleType), IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
hσ'l₁ : σ'.IsCycle ∧ ∀ a ∈ σ'.support, Eq (α := α) ((σ' : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
hσ'₁ : (Finset.card ∘ support) σ' = #σ.support
⊢ IsConj (σ' * τ * σ'⁻¹) τ

Tactic:
rw [← Finset.mem_def, mem_cycleFactorsFinset_iff] at hσ'l

Premises used: Equiv.Perm.mem_cycleFactorsFinset_iff, Finset.mem_def
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ
hπ : ∀ {τ : Perm α} (h : π.cycleType = τ.cycleType), IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ'.IsCycle ∧ ∀ a ∈ σ'.support, Eq (α := α) ((σ' : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
rw : Eq (α := Multiset ℕ) {(Finset.card ∘ support) σ'} {#σ'.support}
⊢ σ.cycleType = σ'.cycleType

Tactic:
rw [hc.cycleType, ← hσ', hσ'l.left.cycleType]

Premises used: Equiv.Perm.IsCycle.cycleType, And.left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ
hπ : ∀ {τ : Perm α} (h : π.cycleType = τ.cycleType), IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ'.IsCycle ∧ ∀ a ∈ σ'.support, Eq (α := α) ((σ' : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ Eq (α := Multiset ℕ) {(Finset.card ∘ support) σ'} {#σ'.support}

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ
hπ : ∀ {τ : Perm α} (h : π.cycleType = τ.cycleType), IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ σ.cycleType = σ'.cycleType

Tactic:
have hs : σ.cycleType = σ'.cycleType := by
      rw [← Finset.mem_def, mem_cycleFactorsFinset_iff] at hσ'l
      rw [hc.cycleType, ← hσ', hσ'l.left.cycleType]; rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ
hπ : ∀ {τ : Perm α} (h : π.cycleType = τ.cycleType), IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
⊢ IsConj (σ * π) (σ' * (τ * σ'⁻¹))

Tactic:
hd.isConj_mul (hσ hs) (hπ ?_) ?_

Premises used: Equiv.Perm.Disjoint.isConj_mul
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ
hπ : ∀ {τ : Perm α} (h : π.cycleType = τ.cycleType), IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
induction_disjoint : π.cycleType = (τ * σ'⁻¹).cycleType
induction_disjoint₁ : σ'.Disjoint (τ * σ'⁻¹)
⊢ IsConj (σ * π) (σ' * (τ * σ'⁻¹))

Tactic:
refine hd.isConj_mul (hσ hs) (hπ ?_) ?_

Premises used: Equiv.Perm.Disjoint.isConj_mul
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ
hπ : ∀ {τ : Perm α} (h : π.cycleType = τ.cycleType), IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
induction_disjoint : σ' ∈ τ.cycleFactorsFinset
⊢ π.cycleType = (τ * σ'⁻¹).cycleType

Tactic:
rw [cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub, ← h, add_comm, hs,
        add_tsub_cancel_right]

Premises used: Equiv.Perm.cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub, add_comm, add_tsub_cancel_right
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ
hπ : ∀ {τ : Perm α} (h : π.cycleType = τ.cycleType), IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
induction_disjoint induction_disjoint₁ induction_disjoint₂ induction_disjoint₃ : σ' ∈ τ.cycleFactorsFinset.val
⊢ σ' ∈ τ.cycleFactorsFinset

Tactic:
rwa [Finset.mem_def]

Premises used: Finset.mem_def
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ
hπ : ∀ {τ : Perm α} (h : π.cycleType = τ.cycleType), IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
⊢ σ'.Disjoint (τ * σ'⁻¹)

Tactic:
(disjoint_mul_inv_of_mem_cycleFactorsFinset hσ'l).symm

Premises used: Equiv.Perm.Disjoint.symm, Equiv.Perm.disjoint_mul_inv_of_mem_cycleFactorsFinset
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α} (h : σ.cycleType = τ.cycleType), IsConj σ τ
hπ : ∀ {τ : Perm α} (h : π.cycleType = τ.cycleType), IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
⊢ σ'.Disjoint (τ * σ'⁻¹)

Tactic:
exact (disjoint_mul_inv_of_mem_cycleFactorsFinset hσ'l).symm

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

Tactic:
induction σ using cycle_induction_on generalizing τ with
  | base_one =>
    rw [cycleType_one, eq_comm, cycleType_eq_zero] at h
    rw [h]
  | base_cycles σ hσ =>
    have hτ := card_cycleType_eq_one.2 hσ
    rw [h, card_cycleType_eq_one] at hτ
    apply hσ.isConj hτ
    rwa [hσ.cycleType, hτ.cycleType, Multiset.singleton_inj] at h
  | induction_disjoint σ π hd hc hσ hπ =>
    rw [hd.cycleType_mul] at h
    have h' : #σ.support ∈ τ.cycleType := by
      simp [← h, hc.cycleType]
    obtain ⟨σ', hσ'l, hσ'⟩ := Multiset.mem_map.mp h'
    have key : IsConj (σ' * τ * σ'⁻¹) τ := (isConj_iff.2 ⟨σ', rfl⟩).symm
    refine IsConj.trans ?_ key
    rw [mul_assoc]
    have hs : σ.cycleType = σ'.cycleType := by
      rw [← Finset.mem_def, mem_cycleFactorsFinset_iff] at hσ'l
      rw [hc.cycleType, ← hσ', hσ'l.left.cycleType]; rfl
    refine hd.isConj_mul (hσ hs) (hπ ?_) ?_
    · rw [cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub, ← h, add_comm, hs,
        add_tsub_cancel_right]
      rwa [Finset.mem_def]
    · exact (disjoint_mul_inv_of_mem_cycleFactorsFinset hσ'l).symm

Premises used: Equiv.Perm.cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub, Multiset.singleton_inj, mul_assoc, Equiv.Perm.card_cycleType_eq_one, eq_comm, add_comm, Equiv.Perm.cycleType_eq_zero, Equiv.Perm.cycleType_one, add_tsub_cancel_right, Finset.mem_def
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
h : IsConj σ τ
obtain : ∀ (π : Perm α) (h : IsConj σ (π * σ * π⁻¹)), σ.cycleType = (π * σ * π⁻¹).cycleType
⊢ σ.cycleType = τ.cycleType

Tactic:
obtain ⟨π, rfl⟩ := isConj_iff.1 h

Premises used: isConj_iff, Iff.mp, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ π : Perm α
h : IsConj σ (π * σ * π⁻¹)
rw rw₁ : σ.cycleType = σ.cycleType
⊢ σ.cycleType = (π * σ * π⁻¹).cycleType

Tactic:
rw [cycleType_conj]

Premises used: Equiv.Perm.cycleType_conj
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
β : Type u_2
inst_2 : Fintype β
inst_3 : DecidableEq β
p : β → Prop
inst_4 : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
base_one : cycleType.{u_2} (α := β) 1 = cycleType.{u_1} (α := α) 1
base_one₁ : 0 = cycleType.{u_1} (α := α) 1
base_one₂ base_one₃ : Eq (α := Multiset ℕ) 0 0
⊢ (extendDomain 1 (p := p) f).cycleType = cycleType.{u_1} (α := α) 1

Tactic:
rw [extendDomain_one, cycleType_one, cycleType_one]

Premises used: Equiv.Perm.cycleType_one, Equiv.Perm.extendDomain_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
β : Type u_2
inst_2 : Fintype β
inst_3 : DecidableEq β
p : β → Prop
inst_4 : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
σ : Perm α
hσ : σ.IsCycle
base_cycles : {#(σ.extendDomain (p := p) f).support} = σ.cycleType
base_cycles₁ : Eq (α := Multiset ℕ) {#(σ.extendDomain (p := p) f).support} {#σ.support}
base_cycles₂ base_cycles₃ : Eq (α := Multiset ℕ) {#σ.support} {#σ.support}
⊢ (σ.extendDomain (p := p) f).cycleType = σ.cycleType

Tactic:
rw [(hσ.extendDomain f).cycleType, hσ.cycleType, card_support_extend_domain]

Premises used: Equiv.Perm.IsCycle.extendDomain, Equiv.Perm.IsCycle.cycleType, Equiv.Perm.card_support_extend_domain
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
β : Type u_2
inst_2 : Fintype β
inst_3 : DecidableEq β
p : β → Prop
inst_4 : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : (σ.extendDomain (p := p) f).cycleType = σ.cycleType
hτ : (τ.extendDomain (p := p) f).cycleType = τ.cycleType
induction_disjoint : ((σ * τ).extendDomain (p := p) f).cycleType = σ.cycleType + τ.cycleType
induction_disjoint₁ : (σ.extendDomain (p := p) f * τ.extendDomain (p := p) f).cycleType = σ.cycleType + τ.cycleType
induction_disjoint₂ :
  (σ.extendDomain (p := p) f).cycleType + (τ.extendDomain (p := p) f).cycleType = σ.cycleType + τ.cycleType
induction_disjoint₃ : σ.cycleType + (τ.extendDomain (p := p) f).cycleType = σ.cycleType + τ.cycleType
induction_disjoint₄ induction_disjoint₅ : σ.cycleType + τ.cycleType = σ.cycleType + τ.cycleType
⊢ ((σ * τ).extendDomain (p := p) f).cycleType = (σ * τ).cycleType

Tactic:
rw [hd.cycleType_mul, ← extendDomain_mul, (hd.extendDomain f).cycleType_mul, hσ, hτ]

Premises used: Equiv.Perm.extendDomain_mul, Equiv.Perm.Disjoint.cycleType_mul, Equiv.Perm.Disjoint.extendDomain
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
β : Type u_2
inst_2 : Fintype β
inst_3 : DecidableEq β
p : β → Prop
inst_4 : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g : Perm α
base_one : (extendDomain 1 (p := p) f).cycleType = cycleType.{u_1} (α := α) 1
base_cycles : ∀ (σ : Perm α) (hσ : σ.IsCycle), (σ.extendDomain (p := p) f).cycleType = σ.cycleType
induction_disjoint :
  ∀ (σ τ : Perm α) (hd : σ.Disjoint τ),
    σ.IsCycle →
      ∀ (hσ : (σ.extendDomain (p := p) f).cycleType = σ.cycleType)
        (hτ : (τ.extendDomain (p := p) f).cycleType = τ.cycleType),
        ((σ * τ).extendDomain (p := p) f).cycleType = (σ * τ).cycleType
⊢ (g.extendDomain (p := p) f).cycleType = g.cycleType

Tactic:
induction g using cycle_induction_on with
  | base_one => rw [extendDomain_one, cycleType_one, cycleType_one]
  | base_cycles σ hσ =>
    rw [(hσ.extendDomain f).cycleType, hσ.cycleType, card_support_extend_domain]
  | induction_disjoint σ τ hd _ hσ hτ =>
    rw [hd.cycleType_mul, ← extendDomain_mul, (hd.extendDomain f).cycleType_mul, hσ, hτ]

Premises used: Equiv.Perm.extendDomain_mul, Equiv.Perm.card_support_extend_domain, Equiv.Perm.cycleType_one, Equiv.Perm.extendDomain_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : α → Prop
inst_2 : DecidablePred p
inst_3 : Fintype (Subtype p)
g : Perm (Subtype p)
⊢ cycleType.{u_1} (α := α) ((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) g) = g.cycleType

Tactic:
cycleType_extendDomain (Equiv.refl (Subtype p))

Premises used: Equiv.Perm.extendDomain, Subtype, Equiv.Perm.cycleType_extendDomain, Equiv.Perm.subtypeCongr, Equiv.refl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
σ : Perm α
mp : n ∈ σ.cycleType → ∃ (c : Perm α) (τ : Perm α), σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n
mpr : (∃ (c : Perm α) (τ : Perm α), σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n) → n ∈ σ.cycleType
⊢ n ∈ σ.cycleType ↔ ∃ (c : Perm α) (τ : Perm α), σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
σ : Perm α
h : n ∈ σ.cycleType
mp :
  ∀ (l : List (Perm α)) (h : n ∈ l.prod.cycleType)
    (x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 })
    (hlc : ∀ g ∈ l, g.IsCycle) (hld : List.Pairwise Disjoint l),
    ∃ (c : Perm α) (τ : Perm α), l.prod = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n
⊢ ∃ (c : Perm α) (τ : Perm α), σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n

Tactic:
obtain ⟨l, rfl, hlc, hld⟩ := truncCycleFactors σ

Premises used: Equiv.Perm.truncCycleFactors, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
l : List (Perm α)
h : n ∈ l.prod.cycleType
x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
hld : List.Pairwise Disjoint l
mp :
  ∀ (h : ∃ a ∈ l, (Finset.card ∘ support) a = n)
    (x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 })
    (hlc : ∀ g ∈ l, g.IsCycle) (hld : List.Pairwise Disjoint l),
    ∃ (c : Perm α) (τ : Perm α), l.prod = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n
⊢ ∃ (c : Perm α) (τ : Perm α), l.prod = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n

Tactic:
rw [cycleType_eq _ rfl hlc hld, Multiset.mem_coe, List.mem_map] at h

Premises used: Equiv.Perm.cycleType_eq, Multiset.mem_coe, List.mem_map, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
l : List (Perm α)
h : ∃ a ∈ l, (Finset.card ∘ support) a = n
x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
hld : List.Pairwise Disjoint l
mp :
  ∀ (c : Perm α) (cl : c ∈ l),
    ∃ (c_1 : Perm α) (τ : Perm α),
      l.prod = c_1 * τ ∧ c_1.Disjoint τ ∧ c_1.IsCycle ∧ #c_1.support = (Finset.card ∘ support) c
⊢ ∃ (c : Perm α) (τ : Perm α), l.prod = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n

Tactic:
obtain ⟨c, cl, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List (Perm α)
x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
hld : List.Pairwise Disjoint l
c : Perm α
cl : c ∈ l
⊢ List.Pairwise Disjoint (c :: l.erase c)

Tactic:
rw [(List.perm_cons_erase cl).pairwise_iff @(Disjoint.symmetric)] at hld

Premises used: List.Perm.pairwise_iff, List.perm_cons_erase, Equiv.Perm.Disjoint.symmetric
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List (Perm α)
x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
hld : List.Pairwise Disjoint l
c : Perm α
cl : c ∈ l
hld₁ : List.Pairwise Disjoint (c :: l.erase c)
⊢ c ∈ l

Tactic:
rw [(List.perm_cons_erase cl).pairwise_iff @(Disjoint.symmetric)] at hld

Premises used: List.Perm.pairwise_iff, List.perm_cons_erase, Equiv.Perm.Disjoint.symmetric
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List (Perm α)
x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
c : Perm α
hld : List.Pairwise Disjoint (c :: l.erase c)
cl : c ∈ l
⊢ ∃ (c_1 : Perm α) (τ : Perm α),
    l.prod = c_1 * τ ∧ c_1.Disjoint τ ∧ c_1.IsCycle ∧ #c_1.support = (Finset.card ∘ support) c

Tactic:
⟨c, (l.erase c).prod, ?_, ?_, hlc _ cl, rfl⟩

Premises used: List.erase, And.intro, Exists.intro, rfl, List.prod
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List (Perm α)
x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
c : Perm α
hld : List.Pairwise Disjoint (c :: l.erase c)
cl : c ∈ l
mp : l.prod = c * (l.erase c).prod
mp₁ : c.Disjoint (l.erase c).prod
⊢ ∃ (c_1 : Perm α) (τ : Perm α),
    l.prod = c_1 * τ ∧ c_1.Disjoint τ ∧ c_1.IsCycle ∧ #c_1.support = (Finset.card ∘ support) c

Tactic:
refine ⟨c, (l.erase c).prod, ?_, ?_, hlc _ cl, rfl⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List (Perm α)
x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
c : Perm α
hld : List.Pairwise Disjoint (c :: l.erase c)
cl : c ∈ l
mp : l.prod = (c :: l.erase c).prod
mp₁ mp₂ : l.prod = l.prod
⊢ l.prod = c * (l.erase c).prod

Tactic:
rw [← List.prod_cons, (List.perm_cons_erase cl).symm.prod_eq' (hld.imp Disjoint.commute)]

Premises used: Equiv.Perm.Disjoint.commute, List.perm_cons_erase, List.Perm.symm, List.Pairwise.imp, List.prod_cons, List.Perm.prod_eq'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List (Perm α)
x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
c : Perm α
hld : List.Pairwise Disjoint (c :: l.erase c)
cl : c ∈ l
⊢ c.Disjoint (l.erase c).prod

Tactic:
disjoint_prod_right _ fun g => List.rel_of_pairwise_cons hld

Premises used: List.rel_of_pairwise_cons, Equiv.Perm.disjoint_prod_right
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List (Perm α)
x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
c : Perm α
hld : List.Pairwise Disjoint (c :: l.erase c)
cl : c ∈ l
⊢ c.Disjoint (l.erase c).prod

Tactic:
exact disjoint_prod_right _ fun g => List.rel_of_pairwise_cons hld

Premises used: List.rel_of_pairwise_cons, Equiv.Perm.disjoint_prod_right
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
c t : Perm α
hd : c.Disjoint t
hc : c.IsCycle
⊢ #c.support ∈ (c * t).cycleType

Tactic:
simp [hd.cycleType_mul, hc.cycleType]

Premises used: Equiv.Perm.IsCycle.cycleType, Equiv.Perm.Disjoint.cycleType_mul
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
σ : Perm α
h : n ∈ σ.cycleType
⊢ n ≤ #σ.support

Tactic:
(le_sum_of_mem h).trans (le_of_eq σ.sum_cycleType)

Premises used: LE.le.trans, le_of_eq, Equiv.Perm.sum_cycleType, Multiset.le_sum_of_mem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
g : Perm α
hn2 : Fintype.card α < n + 2
hng : n ∈ g.cycleType
obtain :
  ∀ (c g' : Perm α) (hd : c.Disjoint g') (hc : c.IsCycle) (hn2 : Fintype.card α < #c.support + 2)
    (hng : #c.support ∈ (c * g').cycleType), (c * g').cycleType = {#c.support}
⊢ g.cycleType = {n}

Tactic:
obtain ⟨c, g', rfl, hd, hc, rfl⟩ := mem_cycleType_iff.1 hng

Premises used: Equiv.Perm.mem_cycleType_iff, Iff.mp, rfl