ι : Type ?u.2777278
α : Type u_1
β : Type ?u.2777284
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f c : Perm α
a : α
ha : a ∈ support c
hc : c ∈ cycleFactorsFinset f
⊢ cycleOf f a = cycleOf c a
ι : Type ?u.2777278
α : Type u_1
β : Type ?u.2777284
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f c : Perm α
a : α
ha : a ∈ support c
hc : c ∈ cycleFactorsFinset f
⊢ c = cycleOf f a
suffices f.cycleOf a = c.cycleOf a by
  rw [this]
  apply symm
  exact
    Equiv.Perm.IsCycle.cycleOf_eq (Equiv.Perm.mem_cycleFactorsFinset_iff.mp hc).left
      (Equiv.Perm.mem_support.mp ha)
ι : Type ?u.2777278
α : Type u_1
β : Type ?u.2777284
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f c : Perm α
a : α
ha : a ∈ support c
hc : c ∈ cycleFactorsFinset f
hfc : Disjoint c (f * c⁻¹) := Disjoint.symm (disjoint_mul_inv_of_mem_cycleFactorsFinset hc)
⊢ cycleOf f a = cycleOf c a
ι : Type ?u.2777278
α : Type u_1
β : Type ?u.2777284
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f c : Perm α
a : α
ha : a ∈ support c
hc : c ∈ cycleFactorsFinset f
⊢ cycleOf f a = cycleOf c a
let hfc := (Equiv.Perm.disjoint_mul_inv_of_mem_cycleFactorsFinset hc).symm
ι : Type ?u.2777278
α : Type u_1
β : Type ?u.2777284
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f c : Perm α
a : α
ha : a ∈ support c
hc : c ∈ cycleFactorsFinset f
hfc : Disjoint c (f * c⁻¹) := Disjoint.symm (disjoint_mul_inv_of_mem_cycleFactorsFinset hc)
hfc2 : _root_.Commute c (f * c⁻¹) := Disjoint.commute hfc
⊢ cycleOf f a = cycleOf c a
ι : Type ?u.2777278
α : Type u_1
β : Type ?u.2777284
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f c : Perm α
a : α
ha : a ∈ support c
hc : c ∈ cycleFactorsFinset f
hfc : Disjoint c (f * c⁻¹) := Disjoint.symm (disjoint_mul_inv_of_mem_cycleFactorsFinset hc)
⊢ cycleOf f a = cycleOf c a
let hfc2 := Perm.Disjoint.commute hfc
ι : Type ?u.2777278
α : Type u_1
β : Type ?u.2777284
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f c : Perm α
a : α
ha : a ∈ support c
hc : c ∈ cycleFactorsFinset f
hfc : Disjoint c (f * c⁻¹) := Disjoint.symm (disjoint_mul_inv_of_mem_cycleFactorsFinset hc)
hfc2 : _root_.Commute c (f * c⁻¹) := Disjoint.commute hfc
⊢ cycleOf f a = cycleOf (c * (f * c⁻¹)) a

case hx
ι : Type ?u.2777278
α : Type u_1
β : Type ?u.2777284
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f c : Perm α
a : α
ha : a ∈ support c
hc : c ∈ cycleFactorsFinset f
hfc : Disjoint c (f * c⁻¹) := Disjoint.symm (disjoint_mul_inv_of_mem_cycleFactorsFinset hc)
hfc2 : _root_.Commute c (f * c⁻¹) := Disjoint.commute hfc
⊢ ↑(f * c⁻¹) a = a
ι : Type ?u.2777278
α : Type u_1
β : Type ?u.2777284
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f c : Perm α
a : α
ha : a ∈ support c
hc : c ∈ cycleFactorsFinset f
hfc : Disjoint c (f * c⁻¹) := Disjoint.symm (disjoint_mul_inv_of_mem_cycleFactorsFinset hc)
hfc2 : _root_.Commute c (f * c⁻¹) := Disjoint.commute hfc
⊢ cycleOf f a = cycleOf c a
rw [← Equiv.Perm.cycleOf_mul_of_apply_right_eq_self hfc2]
case hx
ι : Type ?u.2777278
α : Type u_1
β : Type ?u.2777284
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f c : Perm α
a : α
ha : a ∈ support c
hc : c ∈ cycleFactorsFinset f
hfc : Disjoint c (f * c⁻¹) := Disjoint.symm (disjoint_mul_inv_of_mem_cycleFactorsFinset hc)
hfc2 : _root_.Commute c (f * c⁻¹) := Disjoint.commute hfc
⊢ ↑(f * c⁻¹) a = a
ι : Type ?u.2777278
α : Type u_1
β : Type ?u.2777284
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f c : Perm α
a : α
ha : a ∈ support c
hc : c ∈ cycleFactorsFinset f
hfc : Disjoint c (f * c⁻¹) := Disjoint.symm (disjoint_mul_inv_of_mem_cycleFactorsFinset hc)
hfc2 : _root_.Commute c (f * c⁻¹) := Disjoint.commute hfc
⊢ cycleOf f a = cycleOf (c * (f * c⁻¹)) a

case hx
ι : Type ?u.2777278
α : Type u_1
β : Type ?u.2777284
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f c : Perm α
a : α
ha : a ∈ support c
hc : c ∈ cycleFactorsFinset f
hfc : Disjoint c (f * c⁻¹) := Disjoint.symm (disjoint_mul_inv_of_mem_cycleFactorsFinset hc)
hfc2 : _root_.Commute c (f * c⁻¹) := Disjoint.commute hfc
⊢ ↑(f * c⁻¹) a = a
simp only [hfc2.eq, inv_mul_cancel_right]
no goals
case hx
ι : Type ?u.2777278
α : Type u_1
β : Type ?u.2777284
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f c : Perm α
a : α
ha : a ∈ support c
hc : c ∈ cycleFactorsFinset f
hfc : Disjoint c (f * c⁻¹) := Disjoint.symm (disjoint_mul_inv_of_mem_cycleFactorsFinset hc)
hfc2 : _root_.Commute c (f * c⁻¹) := Disjoint.commute hfc
⊢ ↑(f * c⁻¹) a = a
exact
  Equiv.Perm.not_mem_support.mp
    (Finset.disjoint_left.mp (Equiv.Perm.Disjoint.disjoint_support hfc) ha)
ι : Type ?u.2777278
α : Type u_1
β : Type ?u.2777284
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f c : Perm α
a : α
ha : a ∈ support c
hc : c ∈ cycleFactorsFinset f
this : cycleOf f a = cycleOf c a
⊢ c = cycleOf c a
ι : Type ?u.2777278
α : Type u_1
β : Type ?u.2777284
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f c : Perm α
a : α
ha : a ∈ support c
hc : c ∈ cycleFactorsFinset f
this : cycleOf f a = cycleOf c a
⊢ c = cycleOf f a
rw [this]
case a
ι : Type ?u.2777278
α : Type u_1
β : Type ?u.2777284
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f c : Perm α
a : α
ha : a ∈ support c
hc : c ∈ cycleFactorsFinset f
this : cycleOf f a = cycleOf c a
⊢ cycleOf c a = c
ι : Type ?u.2777278
α : Type u_1
β : Type ?u.2777284
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f c : Perm α
a : α
ha : a ∈ support c
hc : c ∈ cycleFactorsFinset f
this : cycleOf f a = cycleOf c a
⊢ c = cycleOf c a
apply symm
no goals
case a
ι : Type ?u.2777278
α : Type u_1
β : Type ?u.2777284
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f c : Perm α
a : α
ha : a ∈ support c
hc : c ∈ cycleFactorsFinset f
this : cycleOf f a = cycleOf c a
⊢ cycleOf c a = c
exact
  Equiv.Perm.IsCycle.cycleOf_eq (Equiv.Perm.mem_cycleFactorsFinset_iff.mp hc).left
    (Equiv.Perm.mem_support.mp ha)