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

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
h' : σ.support.card ∈ τ.cycleType
⊢ IsConj (σ * π) τ

Tactic:
obtain ⟨σ', hσ'l, hσ'⟩ := Multiset.mem_map.mp h'

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
⊢ IsConj (σ * π) τ

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
⊢ IsConj (σ * π) τ

Tactic:
rw [hd.cycleType] at h

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
⊢ IsConj (σ * π) τ

Proof state:
case induction_disjoint.intro.intro.refine_1
α : 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
⊢ σ' ∈ τ.cycleFactorsFinset

Tactic:
rwa [Finset.mem_def]

Result:
no goals

Proof state:
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : Perm α
h : τ = 1
⊢ IsConj 1 τ

Tactic:
rw [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 (σ' * τ * σ'⁻¹) τ
⊢ ↑[(Finset.card ∘ support) σ'] = ↑[σ'.support.card]

Tactic:
rfl

Result:
no goals

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 (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
⊢ IsConj (σ * π) (σ' * (τ * σ'⁻¹))

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

Result:
case induction_disjoint.intro.intro.refine_1
α : 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
⊢ π.cycleType = (τ * σ'⁻¹).cycleType

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 (τ * σ'⁻¹)

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 : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = σ.support.card
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ σ.cycleType = σ'.cycleType

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

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 (σ' * τ * σ'⁻¹) τ
⊢ σ.cycleType = σ'.cycleType

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

Tactic:
rw [hσ.cycleType, hτ.cycleType, coe_eq_coe, List.singleton_perm] at h

Result:
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

Proof state:
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
τ : Perm α
h : σ.cycleType = τ.cycleType
⊢ IsConj σ τ

Tactic:
have hτ := card_cycleType_eq_one.2 hσ

Result:
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
τ : Perm α
h : σ.cycleType = τ.cycleType
hτ : σ.cycleType.card = 1
⊢ IsConj σ τ

Proof state:
case induction_disjoint.intro.intro.refine_1
α : 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
⊢ π.cycleType = (τ * σ'⁻¹).cycleType

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

Result:
case induction_disjoint.intro.intro.refine_1
α : 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
⊢ σ' ∈ τ.cycleFactorsFinset