-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycleOn.pow_apply_eq {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) {n : ℕ} :
    (f ^ n) a = a ↔ #s ∣ n

Proof state:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
⊢ (f ^ n) a = a ↔ #s ∣ n

Tactic:
obtain rfl | hs := Finset.eq_singleton_or_nontrivial ha

Result:
case inl
α : Type u_2
f : Perm α
a : α
n : ℕ
hf : f.IsCycleOn ↑{a}
ha : a ∈ {a}
⊢ (f ^ n) a = a ↔ #{a} ∣ n

case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
⊢ (f ^ n) a = a ↔ #s ∣ n

Proof state:
case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
⊢ (f ^ n) a = a ↔ #s ∣ n

Tactic:
have h (x : s) : ¬f x = x := hf.apply_ne hs x.2

Result:
case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : { x // x ∈ s }), ¬f ↑x = ↑x
⊢ (f ^ n) a = a ↔ #s ∣ n

Proof state:
case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
⊢ (f ^ n) a = a ↔ #s ∣ n

Tactic:
classical
  have h (x : s) : ¬f x = x := hf.apply_ne hs x.2
  have := (hf.isCycle_subtypePerm hs).orderOf
  simp only [coe_sort_coe, support_subtype_perm, ne_eq, h, not_false_eq_true, univ_eq_attach,
    mem_attach, imp_self, implies_true, filter_true_of_mem, card_attach] at this
  rw [← this, orderOf_dvd_iff_pow_eq_one,
    (hf.isCycle_subtypePerm hs).pow_eq_one_iff'
      (ne_of_apply_ne ((↑) : s → α) <| hf.apply_ne hs (⟨a, ha⟩ : s).2)]
  simp
  erw [subtypePerm_apply]
  simp

Result:
no goals

Proof state:
case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : { x // x ∈ s }), ¬f ↑x = ↑x
this : orderOf (f.subtypePerm ⋯) = #s
⊢ (f ^ n) a = a ↔ ⟨(f ^ n) ↑⟨a, ha⟩, ⋯⟩ = ⟨a, ha⟩

Tactic:
simp

Result:
no goals

Proof state:
case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : { x // x ∈ s }), ¬f ↑x = ↑x
this : orderOf (f.subtypePerm ⋯) = #s
⊢ (f ^ n) a = a ↔ ((f ^ n).subtypePerm ⋯) ⟨a, ha⟩ = ⟨a, ha⟩

Tactic:
erw [subtypePerm_apply]

Result:
case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : { x // x ∈ s }), ¬f ↑x = ↑x
this : orderOf (f.subtypePerm ⋯) = #s
⊢ (f ^ n) a = a ↔ ⟨(f ^ n) ↑⟨a, ha⟩, ⋯⟩ = ⟨a, ha⟩

Proof state:
case inl
α : Type u_2
f : Perm α
a : α
n : ℕ
hf : f a = a
ha : a ∈ {a}
⊢ (f ^ n) a = a ↔ #{a} ∣ n

Tactic:
simpa using IsFixedPt.iterate hf n

Result:
no goals

Proof state:
case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : { x // x ∈ s }), ¬f ↑x = ↑x
this : orderOf (f.subtypePerm ⋯) = #s
⊢ (f ^ n) a = a ↔ (f.subtypePerm ⋯ ^ n) ⟨a, ha⟩ = ⟨a, ha⟩

Tactic:
simp

Result:
case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : { x // x ∈ s }), ¬f ↑x = ↑x
this : orderOf (f.subtypePerm ⋯) = #s
⊢ (f ^ n) a = a ↔ ((f ^ n).subtypePerm ⋯) ⟨a, ha⟩ = ⟨a, ha⟩

Proof state:
case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : { x // x ∈ s }), ¬f ↑x = ↑x
this : orderOf (f.subtypePerm ⋯) = #s
⊢ (f ^ n) a = a ↔ #s ∣ n

Tactic:
rw [← this, orderOf_dvd_iff_pow_eq_one,
  (hf.isCycle_subtypePerm hs).pow_eq_one_iff'
    (ne_of_apply_ne ((↑) : s → α) <| hf.apply_ne hs (⟨a, ha⟩ : s).2)]

Result:
case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : { x // x ∈ s }), ¬f ↑x = ↑x
this : orderOf (f.subtypePerm ⋯) = #s
⊢ (f ^ n) a = a ↔ (f.subtypePerm ⋯ ^ n) ⟨a, ha⟩ = ⟨a, ha⟩

Proof state:
case inl
α : Type u_2
f : Perm α
a : α
n : ℕ
hf : f.IsCycleOn ↑{a}
ha : a ∈ {a}
⊢ (f ^ n) a = a ↔ #{a} ∣ n

Tactic:
rw [coe_singleton, isCycleOn_singleton] at hf

Result:
case inl
α : Type u_2
f : Perm α
a : α
n : ℕ
hf : f a = a
ha : a ∈ {a}
⊢ (f ^ n) a = a ↔ #{a} ∣ n

Proof state:
case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : { x // x ∈ s }), ¬f ↑x = ↑x
⊢ (f ^ n) a = a ↔ #s ∣ n

Tactic:
have := (hf.isCycle_subtypePerm hs).orderOf

Result:
case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : { x // x ∈ s }), ¬f ↑x = ↑x
this : orderOf (f.subtypePerm ⋯) = #(f.subtypePerm ⋯).support
⊢ (f ^ n) a = a ↔ #s ∣ n

Proof state:
case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : { x // x ∈ s }), ¬f ↑x = ↑x
this : orderOf (f.subtypePerm ⋯) = #(f.subtypePerm ⋯).support
⊢ (f ^ n) a = a ↔ #s ∣ n

Tactic:
simp only [coe_sort_coe, support_subtype_perm, ne_eq, h, not_false_eq_true, univ_eq_attach,
  mem_attach, imp_self, implies_true, filter_true_of_mem, card_attach] at this

Result:
case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : { x // x ∈ s }), ¬f ↑x = ↑x
this : orderOf (f.subtypePerm ⋯) = #s
⊢ (f ^ n) a = a ↔ #s ∣ n