-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem isConj_of_cycleType_eq {σ τ : Perm α} (h : cycleType σ = cycleType τ) : IsConj σ τ

Proof state:
case induction_disjoint.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : σ.support.card ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = σ.support.card
⊢ IsConj (σ * π) τ

Tactic:
have key : IsConj (σ' * τ * σ'⁻¹) τ := (isConj_iff.2 ⟨σ', rfl⟩).symm

Result:
case induction_disjoint.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : σ.support.card ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = σ.support.card
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ IsConj (σ * π) τ

Proof state:
case induction_disjoint.intro.intro.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : σ.support.card ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = σ.support.card
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
⊢ σ'.Disjoint (τ * σ'⁻¹)

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

Result:
no goals

Proof state:
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
τ : Perm α
h : [σ.support.card] = [τ.support.card]
hτ : τ.IsCycle
⊢ σ.support.card = τ.support.card

Tactic:
exact List.singleton_injective h

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : σ.support.card ∈ τ.cycleType
σ' : Perm α
hσ'l : σ'.IsCycle ∧ ∀ a ∈ σ'.support, σ' a = τ a
hσ' : (Finset.card ∘ support) σ' = σ.support.card
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ σ.cycleType = σ'.cycleType

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

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : σ.support.card ∈ τ.cycleType
σ' : Perm α
hσ'l : σ'.IsCycle ∧ ∀ a ∈ σ'.support, σ' a = τ a
hσ' : (Finset.card ∘ support) σ' = σ.support.card
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ ↑[(Finset.card ∘ support) σ'] = ↑[σ'.support.card]

Proof state:
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
⊢ IsConj (σ * π) τ

Tactic:
have h' : σ.support.card ∈ τ.cycleType := by
  simp [← h, hc.cycleType]

Result:
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : σ.support.card ∈ τ.cycleType
⊢ IsConj (σ * π) τ

Proof state:
case induction_disjoint.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : σ.support.card ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = σ.support.card
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ IsConj (σ * π) (σ' * τ * σ'⁻¹)

Tactic:
rw [mul_assoc]

Result:
case induction_disjoint.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : σ.support.card ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = σ.support.card
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ IsConj (σ * π) (σ' * (τ * σ'⁻¹))

Proof state:
case induction_disjoint.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : σ.support.card ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = σ.support.card
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ IsConj (σ * π) (σ' * (τ * σ'⁻¹))

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

Result:
case induction_disjoint.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : σ.support.card ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = σ.support.card
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
⊢ IsConj (σ * π) (σ' * (τ * σ'⁻¹))

Proof state:
case induction_disjoint.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : σ.support.card ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = σ.support.card
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ IsConj (σ * π) τ

Tactic:
refine IsConj.trans ?_ key

Result:
case induction_disjoint.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : σ.support.card ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = σ.support.card
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ IsConj (σ * π) (σ' * τ * σ'⁻¹)