ι : Type ?u.3035426
α : Type u_1
β : Type ?u.3035432
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
hσ : IsCycle σ
hτ : IsCycle τ
h : IsConj σ τ
⊢ card (support σ) = card (support τ)
ι : Type ?u.3035426
α : Type u_1
β : Type ?u.3035432
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
hσ : IsCycle σ
hτ : IsCycle τ
⊢ IsConj σ τ → card (support σ) = card (support τ)
intro h
case intro
ι : Type ?u.3035426
α : Type u_1
β : Type ?u.3035432
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : IsCycle σ
π : Perm α
hτ : IsCycle (π * σ * π⁻¹)
h : IsConj σ (π * σ * π⁻¹)
⊢ card (support σ) = card (support (π * σ * π⁻¹))
ι : Type ?u.3035426
α : Type u_1
β : Type ?u.3035432
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
hσ : IsCycle σ
hτ : IsCycle τ
h : IsConj σ τ
⊢ card (support σ) = card (support τ)
obtain ⟨π, rfl⟩ := (_root_.isConj_iff).1 h
case intro.refine'_1
ι : Type ?u.3035426
α : Type u_1
β : Type ?u.3035432
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : IsCycle σ
π : Perm α
hτ : IsCycle (π * σ * π⁻¹)
h : IsConj σ (π * σ * π⁻¹)
x✝ : α
ha : x✝ ∈ support σ
⊢ (fun a x => ↑π a) x✝ ha ∈ support (π * σ * π⁻¹)

case intro.refine'_2
ι : Type ?u.3035426
α : Type u_1
β : Type ?u.3035432
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : IsCycle σ
π : Perm α
hτ : IsCycle (π * σ * π⁻¹)
h : IsConj σ (π * σ * π⁻¹)
b : α
hb : b ∈ support (π * σ * π⁻¹)
⊢ ∃ a ha, (fun a x => ↑π a) a ha = b
case intro
ι : Type ?u.3035426
α : Type u_1
β : Type ?u.3035432
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : IsCycle σ
π : Perm α
hτ : IsCycle (π * σ * π⁻¹)
h : IsConj σ (π * σ * π⁻¹)
⊢ card (support σ) = card (support (π * σ * π⁻¹))
refine' Finset.card_congr (fun a _ => π a) (fun _ ha => _) (fun _ _ _ _ ab => π.injective ab)
    fun b hb => _
no goals
case intro.refine'_1
ι : Type ?u.3035426
α : Type u_1
β : Type ?u.3035432
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : IsCycle σ
π : Perm α
hτ : IsCycle (π * σ * π⁻¹)
h : IsConj σ (π * σ * π⁻¹)
x✝ : α
ha : x✝ ∈ support σ
⊢ (fun a x => ↑π a) x✝ ha ∈ support (π * σ * π⁻¹)
simp [mem_support.1 ha]
case intro.refine'_2
ι : Type ?u.3035426
α : Type u_1
β : Type ?u.3035432
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : IsCycle σ
π : Perm α
hτ : IsCycle (π * σ * π⁻¹)
h : IsConj σ (π * σ * π⁻¹)
b : α
hb : b ∈ support (π * σ * π⁻¹)
⊢ ↑π⁻¹ b ∈ support σ
case intro.refine'_2
ι : Type ?u.3035426
α : Type u_1
β : Type ?u.3035432
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : IsCycle σ
π : Perm α
hτ : IsCycle (π * σ * π⁻¹)
h : IsConj σ (π * σ * π⁻¹)
b : α
hb : b ∈ support (π * σ * π⁻¹)
⊢ ∃ a ha, (fun a x => ↑π a) a ha = b
refine' ⟨π⁻¹ b, ⟨_, π.apply_inv_self b⟩⟩
case intro.refine'_2
ι : Type ?u.3035426
α : Type u_1
β : Type ?u.3035432
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : IsCycle σ
π : Perm α
hτ : IsCycle (π * σ * π⁻¹)
h : IsConj σ (π * σ * π⁻¹)
b : α
hb : ¬↑π⁻¹ b ∈ support σ
⊢ ¬b ∈ support (π * σ * π⁻¹)
case intro.refine'_2
ι : Type ?u.3035426
α : Type u_1
β : Type ?u.3035432
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : IsCycle σ
π : Perm α
hτ : IsCycle (π * σ * π⁻¹)
h : IsConj σ (π * σ * π⁻¹)
b : α
hb : b ∈ support (π * σ * π⁻¹)
⊢ ↑π⁻¹ b ∈ support σ
contrapose! hb
case intro.refine'_2
ι : Type ?u.3035426
α : Type u_1
β : Type ?u.3035432
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : IsCycle σ
π : Perm α
hτ : IsCycle (π * σ * π⁻¹)
h : IsConj σ (π * σ * π⁻¹)
b : α
hb : ↑σ (↑π⁻¹ b) = ↑π⁻¹ b
⊢ ¬b ∈ support (π * σ * π⁻¹)
case intro.refine'_2
ι : Type ?u.3035426
α : Type u_1
β : Type ?u.3035432
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : IsCycle σ
π : Perm α
hτ : IsCycle (π * σ * π⁻¹)
h : IsConj σ (π * σ * π⁻¹)
b : α
hb : ¬↑π⁻¹ b ∈ support σ
⊢ ¬b ∈ support (π * σ * π⁻¹)
rw [mem_support, Classical.not_not] at hb
no goals
case intro.refine'_2
ι : Type ?u.3035426
α : Type u_1
β : Type ?u.3035432
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : IsCycle σ
π : Perm α
hτ : IsCycle (π * σ * π⁻¹)
h : IsConj σ (π * σ * π⁻¹)
b : α
hb : ↑σ (↑π⁻¹ b) = ↑π⁻¹ b
⊢ ¬b ∈ support (π * σ * π⁻¹)
rw [mem_support, Classical.not_not, Perm.mul_apply, Perm.mul_apply, hb, Perm.apply_inv_self]