ι : Type ?u.3031573
α : Type u_1
β : Type ?u.3031579
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
hσ : IsCycle σ
hτ : IsCycle τ
h : card (support σ) = card (support τ)
⊢ ∀ (x : α) (hx : x ∈ ↑(support σ)),
    ↑(↑((zpowersEquivSupport hσ).symm.trans
              ((zpowersEquivZpowers (_ : orderOf σ = orderOf τ)).trans (zpowersEquivSupport hτ)))
          { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }) =
      ↑τ
        ↑(↑((zpowersEquivSupport hσ).symm.trans
                ((zpowersEquivZpowers (_ : orderOf σ = orderOf τ)).trans (zpowersEquivSupport hτ)))
            { val := x, property := hx })
ι : Type ?u.3031573
α : Type u_1
β : Type ?u.3031579
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
hσ : IsCycle σ
hτ : IsCycle τ
h : card (support σ) = card (support τ)
⊢ IsConj σ τ
refine'
  isConj_of_support_equiv
    (hσ.zpowersEquivSupport.symm.trans <|
      (zpowersEquivZpowers <| by rw [hσ.orderOf, h, hτ.orderOf]).trans hτ.zpowersEquivSupport)
    _
ι : Type ?u.3031573
α : Type u_1
β : Type ?u.3031579
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
hσ : IsCycle σ
hτ : IsCycle τ
h : card (support σ) = card (support τ)
x : α
hx : x ∈ ↑(support σ)
⊢ ↑(↑((zpowersEquivSupport hσ).symm.trans
            ((zpowersEquivZpowers (_ : orderOf σ = orderOf τ)).trans (zpowersEquivSupport hτ)))
        { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }) =
    ↑τ
      ↑(↑((zpowersEquivSupport hσ).symm.trans
              ((zpowersEquivZpowers (_ : orderOf σ = orderOf τ)).trans (zpowersEquivSupport hτ)))
          { val := x, property := hx })
ι : Type ?u.3031573
α : Type u_1
β : Type ?u.3031579
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
hσ : IsCycle σ
hτ : IsCycle τ
h : card (support σ) = card (support τ)
⊢ ∀ (x : α) (hx : x ∈ ↑(support σ)),
    ↑(↑((zpowersEquivSupport hσ).symm.trans
              ((zpowersEquivZpowers (_ : orderOf σ = orderOf τ)).trans (zpowersEquivSupport hτ)))
          { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }) =
      ↑τ
        ↑(↑((zpowersEquivSupport hσ).symm.trans
                ((zpowersEquivZpowers (_ : orderOf σ = orderOf τ)).trans (zpowersEquivSupport hτ)))
            { val := x, property := hx })
intro x hx
ι : Type ?u.3031573
α : Type u_1
β : Type ?u.3031579
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
hσ : IsCycle σ
hτ : IsCycle τ
h : card (support σ) = card (support τ)
x : α
hx : x ∈ ↑(support σ)
⊢ ↑(↑(zpowersEquivSupport hτ)
        (↑(zpowersEquivZpowers (_ : orderOf σ = orderOf τ))
          (↑(zpowersEquivSupport hσ).symm { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }))) =
    ↑τ
      ↑(↑(zpowersEquivSupport hτ)
          (↑(zpowersEquivZpowers (_ : orderOf σ = orderOf τ))
            (↑(zpowersEquivSupport hσ).symm { val := x, property := hx })))
ι : Type ?u.3031573
α : Type u_1
β : Type ?u.3031579
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
hσ : IsCycle σ
hτ : IsCycle τ
h : card (support σ) = card (support τ)
x : α
hx : x ∈ ↑(support σ)
⊢ ↑(↑((zpowersEquivSupport hσ).symm.trans
            ((zpowersEquivZpowers (_ : orderOf σ = orderOf τ)).trans (zpowersEquivSupport hτ)))
        { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }) =
    ↑τ
      ↑(↑((zpowersEquivSupport hσ).symm.trans
              ((zpowersEquivZpowers (_ : orderOf σ = orderOf τ)).trans (zpowersEquivSupport hτ)))
          { val := x, property := hx })
simp only [Perm.mul_apply, Equiv.trans_apply, Equiv.sumCongr_apply]
case intro
ι : Type ?u.3031573
α : Type u_1
β : Type ?u.3031579
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
hσ : IsCycle σ
hτ : IsCycle τ
h : card (support σ) = card (support τ)
n : ℕ
hx : ↑(σ ^ n) (Classical.choose hσ) ∈ ↑(support σ)
⊢ ↑(↑(zpowersEquivSupport hτ)
        (↑(zpowersEquivZpowers (_ : orderOf σ = orderOf τ))
          (↑(zpowersEquivSupport hσ).symm
            { val := ↑σ (↑(σ ^ n) (Classical.choose hσ)),
              property := (_ : ↑σ (↑(σ ^ n) (Classical.choose hσ)) ∈ support σ) }))) =
    ↑τ
      ↑(↑(zpowersEquivSupport hτ)
          (↑(zpowersEquivZpowers (_ : orderOf σ = orderOf τ))
            (↑(zpowersEquivSupport hσ).symm { val := ↑(σ ^ n) (Classical.choose hσ), property := hx })))
ι : Type ?u.3031573
α : Type u_1
β : Type ?u.3031579
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
hσ : IsCycle σ
hτ : IsCycle τ
h : card (support σ) = card (support τ)
x : α
hx : x ∈ ↑(support σ)
⊢ ↑(↑(zpowersEquivSupport hτ)
        (↑(zpowersEquivZpowers (_ : orderOf σ = orderOf τ))
          (↑(zpowersEquivSupport hσ).symm { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }))) =
    ↑τ
      ↑(↑(zpowersEquivSupport hτ)
          (↑(zpowersEquivZpowers (_ : orderOf σ = orderOf τ))
            (↑(zpowersEquivSupport hσ).symm { val := x, property := hx })))
obtain ⟨n, rfl⟩ := hσ.exists_pow_eq (Classical.choose_spec hσ).1 (mem_support.1 hx)
ι : Type ?u.3031573
α : Type u_1
β : Type ?u.3031579
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
hσ : IsCycle σ
hτ : IsCycle τ
h : card (support σ) = card (support τ)
n : ℕ
hx : ↑(σ ^ n) (Classical.choose hσ) ∈ ↑(support σ)
⊢ ↑(↑(zpowersEquivSupport hτ)
        (↑(zpowersEquivZpowers (_ : orderOf σ = orderOf τ))
          (↑(zpowersEquivSupport hσ).symm
            { val := ↑σ (↑(σ ^ n) (Classical.choose hσ)),
              property := (_ : ↑σ (↑(σ ^ n) (Classical.choose hσ)) ∈ support σ) }))) =
    ↑τ
      ↑(↑(zpowersEquivSupport hτ)
          (↑(zpowersEquivZpowers (_ : orderOf σ = orderOf τ))
            { val := σ ^ n, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) σ y = σ ^ n) }))
case intro
ι : Type ?u.3031573
α : Type u_1
β : Type ?u.3031579
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
hσ : IsCycle σ
hτ : IsCycle τ
h : card (support σ) = card (support τ)
n : ℕ
hx : ↑(σ ^ n) (Classical.choose hσ) ∈ ↑(support σ)
⊢ ↑(↑(zpowersEquivSupport hτ)
        (↑(zpowersEquivZpowers (_ : orderOf σ = orderOf τ))
          (↑(zpowersEquivSupport hσ).symm
            { val := ↑σ (↑(σ ^ n) (Classical.choose hσ)),
              property := (_ : ↑σ (↑(σ ^ n) (Classical.choose hσ)) ∈ support σ) }))) =
    ↑τ
      ↑(↑(zpowersEquivSupport hτ)
          (↑(zpowersEquivZpowers (_ : orderOf σ = orderOf τ))
            (↑(zpowersEquivSupport hσ).symm { val := ↑(σ ^ n) (Classical.choose hσ), property := hx })))
apply
  Eq.trans _
    (congr rfl (congr rfl (congr rfl (congr rfl (hσ.zpowersEquivSupport_symm_apply n).symm))))
ι : Type ?u.3031573
α : Type u_1
β : Type ?u.3031579
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
hσ : IsCycle σ
hτ : IsCycle τ
h : card (support σ) = card (support τ)
n : ℕ
hx : ↑(σ ^ n) (Classical.choose hσ) ∈ ↑(support σ)
⊢ ↑(↑(zpowersEquivSupport hτ)
        (↑(zpowersEquivZpowers (_ : orderOf σ = orderOf τ))
          { val := σ ^ (n + 1), property := (_ : ∃ y, (fun x x_1 => x ^ x_1) σ y = σ ^ (n + 1)) })) =
    ↑τ
      ↑(↑(zpowersEquivSupport hτ)
          (↑(zpowersEquivZpowers (_ : orderOf σ = orderOf τ))
            { val := σ ^ n, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) σ y = σ ^ n) }))
ι : Type ?u.3031573
α : Type u_1
β : Type ?u.3031579
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
hσ : IsCycle σ
hτ : IsCycle τ
h : card (support σ) = card (support τ)
n : ℕ
hx : ↑(σ ^ n) (Classical.choose hσ) ∈ ↑(support σ)
⊢ ↑(↑(zpowersEquivSupport hτ)
        (↑(zpowersEquivZpowers (_ : orderOf σ = orderOf τ))
          (↑(zpowersEquivSupport hσ).symm
            { val := ↑σ (↑(σ ^ n) (Classical.choose hσ)),
              property := (_ : ↑σ (↑(σ ^ n) (Classical.choose hσ)) ∈ support σ) }))) =
    ↑τ
      ↑(↑(zpowersEquivSupport hτ)
          (↑(zpowersEquivZpowers (_ : orderOf σ = orderOf τ))
            { val := σ ^ n, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) σ y = σ ^ n) }))
apply (congr rfl (congr rfl (congr rfl (hσ.zpowersEquivSupport_symm_apply (n + 1))))).trans _
ι : Type ?u.3031573
α : Type u_1
β : Type ?u.3031579
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
hσ : IsCycle σ
hτ : IsCycle τ
h : card (support σ) = card (support τ)
n : ℕ
hx : ↑(σ ^ n) (Classical.choose hσ) ∈ ↑(support σ)
⊢ ↑(↑(zpowersEquivSupport hτ) { val := τ ^ (n + 1), property := (_ : ∃ y, (fun x x_1 => x ^ x_1) τ y = τ ^ (n + 1)) }) =
    ↑τ ↑(↑(zpowersEquivSupport hτ) { val := τ ^ n, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) τ y = τ ^ n) })
ι : Type ?u.3031573
α : Type u_1
β : Type ?u.3031579
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
hσ : IsCycle σ
hτ : IsCycle τ
h : card (support σ) = card (support τ)
n : ℕ
hx : ↑(σ ^ n) (Classical.choose hσ) ∈ ↑(support σ)
⊢ ↑(↑(zpowersEquivSupport hτ)
        (↑(zpowersEquivZpowers (_ : orderOf σ = orderOf τ))
          { val := σ ^ (n + 1), property := (_ : ∃ y, (fun x x_1 => x ^ x_1) σ y = σ ^ (n + 1)) })) =
    ↑τ
      ↑(↑(zpowersEquivSupport hτ)
          (↑(zpowersEquivZpowers (_ : orderOf σ = orderOf τ))
            { val := σ ^ n, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) σ y = σ ^ n) }))
simp only [Ne.def, IsCycle.zpowersEquivSupport_apply, Subtype.coe_mk,
  zpowersEquivZpowers_apply]
ι : Type ?u.3031573
α : Type u_1
β : Type ?u.3031579
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
hσ : IsCycle σ
hτ : IsCycle τ
h : card (support σ) = card (support τ)
n : ℕ
hx : ↑(σ ^ n) (Classical.choose hσ) ∈ ↑(support σ)
⊢ ↑(τ ^ (n + 1)) (Classical.choose hτ) = ↑τ (↑(τ ^ n) (Classical.choose hτ))
ι : Type ?u.3031573
α : Type u_1
β : Type ?u.3031579
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
hσ : IsCycle σ
hτ : IsCycle τ
h : card (support σ) = card (support τ)
n : ℕ
hx : ↑(σ ^ n) (Classical.choose hσ) ∈ ↑(support σ)
⊢ ↑(↑(zpowersEquivSupport hτ) { val := τ ^ (n + 1), property := (_ : ∃ y, (fun x x_1 => x ^ x_1) τ y = τ ^ (n + 1)) }) =
    ↑τ ↑(↑(zpowersEquivSupport hτ) { val := τ ^ n, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) τ y = τ ^ n) })
dsimp
no goals
ι : Type ?u.3031573
α : Type u_1
β : Type ?u.3031579
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
hσ : IsCycle σ
hτ : IsCycle τ
h : card (support σ) = card (support τ)
n : ℕ
hx : ↑(σ ^ n) (Classical.choose hσ) ∈ ↑(support σ)
⊢ ↑(τ ^ (n + 1)) (Classical.choose hτ) = ↑τ (↑(τ ^ n) (Classical.choose hτ))
rw [pow_succ, Perm.mul_apply]
no goals
ι : Type ?u.3031573
α : Type u_1
β : Type ?u.3031579
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
hσ : IsCycle σ
hτ : IsCycle τ
h : card (support σ) = card (support τ)
⊢ orderOf σ = orderOf τ
rw [hσ.orderOf, h, hτ.orderOf]