case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : Perm α
h : τ = 1
⊢ IsConj 1 τ
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : Perm α
h : cycleType 1 = cycleType τ
⊢ IsConj 1 τ
rw [cycleType_one, eq_comm, cycleType_eq_zero] at h
no goals
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : Perm α
h : τ = 1
⊢ IsConj 1 τ
rw [h]
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
τ : Perm α
h : cycleType σ = cycleType τ
hτ : ↑card (cycleType σ) = 1
⊢ IsConj σ τ
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
τ : Perm α
h : cycleType σ = cycleType τ
⊢ IsConj σ τ
have hτ := card_cycleType_eq_one.2 hσ
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
τ : Perm α
h : cycleType σ = cycleType τ
hτ : IsCycle τ
⊢ IsConj σ τ
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
τ : Perm α
h : cycleType σ = cycleType τ
hτ : ↑card (cycleType σ) = 1
⊢ IsConj σ τ
rw [h, card_cycleType_eq_one] at hτ
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
τ : Perm α
h : cycleType σ = cycleType τ
hτ : IsCycle τ
⊢ Finset.card (support σ) = Finset.card (support τ)
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
τ : Perm α
h : cycleType σ = cycleType τ
hτ : IsCycle τ
⊢ IsConj σ τ
apply hσ.isConj hτ
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
τ : Perm α
h : [Finset.card (support σ)] = [Finset.card (support τ)]
hτ : IsCycle τ
⊢ Finset.card (support σ) = Finset.card (support τ)
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
τ : Perm α
h : cycleType σ = cycleType τ
hτ : IsCycle τ
⊢ Finset.card (support σ) = Finset.card (support τ)
rw [hσ.cycleType, hτ.cycleType, coe_eq_coe, List.singleton_perm] at h
no goals
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
τ : Perm α
h : [Finset.card (support σ)] = [Finset.card (support τ)]
hτ : IsCycle τ
⊢ Finset.card (support σ) = Finset.card (support τ)
exact List.singleton_injective h
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 (σ * π) τ
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 (σ * π) τ
rw [hd.cycleType] at h
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' : Finset.card (support σ) ∈ cycleType τ
⊢ IsConj (σ * π) τ
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 (σ * π) τ
have h' : σ.support.card ∈ τ.cycleType := by
  simp [← h, hc.cycleType]
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' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
⊢ IsConj (σ * π) τ
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' : Finset.card (support σ) ∈ cycleType τ
⊢ IsConj (σ * π) τ
obtain ⟨σ', hσ'l, hσ'⟩ := Multiset.mem_map.mp h'
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' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ IsConj (σ * π) τ
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' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
⊢ IsConj (σ * π) τ
have key : IsConj (σ' * τ * σ'⁻¹) τ := (isConj_iff.2 ⟨σ', rfl⟩).symm
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' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ IsConj (σ * π) (σ' * τ * σ'⁻¹)
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' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ IsConj (σ * π) τ
refine' IsConj.trans _ key
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' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ IsConj (σ * π) (σ' * (τ * σ'⁻¹))
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' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ IsConj (σ * π) (σ' * τ * σ'⁻¹)
rw [mul_assoc]
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' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : cycleType σ = cycleType σ'
⊢ IsConj (σ * π) (σ' * (τ * σ'⁻¹))
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' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ IsConj (σ * π) (σ' * (τ * σ'⁻¹))
have hs : σ.cycleType = σ'.cycleType := by
  rw [← Finset.mem_def, mem_cycleFactorsFinset_iff] at hσ'l
  rw [hc.cycleType, ← hσ', hσ'l.left.cycleType]; rfl
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' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
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' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : cycleType σ = cycleType σ'
⊢ Disjoint σ' (τ * σ'⁻¹)
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' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : cycleType σ = cycleType σ'
⊢ IsConj (σ * π) (σ' * (τ * σ'⁻¹))
refine' hd.isConj_mul (hσ hs) (hπ _) _
no goals
α : 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 τ
⊢ Finset.card (support σ) ∈ cycleType τ
simp [← h, hc.cycleType]
α : 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' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : IsCycle σ' ∧ ∀ (a : α), a ∈ support σ' → ↑σ' a = ↑τ a
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ cycleType σ = cycleType σ'
α : 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' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ cycleType σ = cycleType σ'
rw [← Finset.mem_def, mem_cycleFactorsFinset_iff] at hσ'l
α : 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' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : IsCycle σ' ∧ ∀ (a : α), a ∈ support σ' → ↑σ' a = ↑τ a
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ ↑[(Finset.card ∘ support) σ'] = ↑[Finset.card (support σ')]
α : 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' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : IsCycle σ' ∧ ∀ (a : α), a ∈ support σ' → ↑σ' a = ↑τ a
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ cycleType σ = cycleType σ'
rw [hc.cycleType, ← hσ', hσ'l.left.cycleType]
no goals
α : 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' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : IsCycle σ' ∧ ∀ (a : α), a ∈ support σ' → ↑σ' a = ↑τ a
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ ↑[(Finset.card ∘ support) σ'] = ↑[Finset.card (support σ')]
rfl
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' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : cycleType σ = cycleType σ'
⊢ σ' ∈ cycleFactorsFinset τ
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' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : cycleType σ = cycleType σ'
⊢ cycleType π = cycleType (τ * σ'⁻¹)
rw [cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub, ← h, add_comm, hs,
  add_tsub_cancel_right]
no goals
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' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : cycleType σ = cycleType σ'
⊢ σ' ∈ cycleFactorsFinset τ
rwa [Finset.mem_def]
no goals
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' : Finset.card (support σ) ∈ cycleType τ
σ' : Perm α
hσ'l : σ' ∈ (cycleFactorsFinset τ).val
hσ' : (Finset.card ∘ support) σ' = Finset.card (support σ)
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : cycleType σ = cycleType σ'
⊢ Disjoint σ' (τ * σ'⁻¹)
exact (disjoint_mul_inv_of_mem_cycleFactorsFinset hσ'l).symm