-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycleOn.exists_pow_eq {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) (hb : b ∈ s) :
    ∃ n < #s, (f ^ n) a = b

Proof state:
case intro.intro
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℤ
hb : (f ^ n) a ∈ s
k : ℤ
hk : n % ↑(#s) - n = ↑(#s) * k
⊢ (f ^ n.natMod ↑(#s)) a = (f ^ n) a

Tactic:
rw [← zpow_natCast, Int.natMod,
  Int.toNat_of_nonneg (Int.emod_nonneg _ <| Nat.cast_ne_zero.2
    (Nonempty.card_pos ⟨a, ha⟩).ne'), sub_eq_iff_eq_add'.1 hk, zpow_add, zpow_mul]

Result:
case intro.intro
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℤ
hb : (f ^ n) a ∈ s
k : ℤ
hk : n % ↑(#s) - n = ↑(#s) * k
⊢ (f ^ n * (f ^ ↑(#s)) ^ k) a = (f ^ n) a

Proof state:
case intro
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℤ
hb : (f ^ n) a ∈ s
⊢ ∃ n_1 < #s, (f ^ n_1) a = (f ^ n) a

Tactic:
obtain ⟨k, hk⟩ := (Int.mod_modEq n #s).symm.dvd

Result:
case intro.intro
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℤ
hb : (f ^ n) a ∈ s
k : ℤ
hk : n % ↑(#s) - n = ↑(#s) * k
⊢ ∃ n_1 < #s, (f ^ n_1) a = (f ^ n) a

Proof state:
case intro.intro
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℤ
hb : (f ^ n) a ∈ s
k : ℤ
hk : n % ↑(#s) - n = ↑(#s) * k
⊢ ∃ n_1 < #s, (f ^ n_1) a = (f ^ n) a

Tactic:
refine ⟨n.natMod #s, Int.natMod_lt (Nonempty.card_pos ⟨a, ha⟩).ne', ?_⟩

Result:
case intro.intro
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℤ
hb : (f ^ n) a ∈ s
k : ℤ
hk : n % ↑(#s) - n = ↑(#s) * k
⊢ (f ^ n.natMod ↑(#s)) a = (f ^ n) a

Proof state:
α : Type u_2
f : Perm α
a b : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
hb : b ∈ s
⊢ ∃ n < #s, (f ^ n) a = b

Tactic:
classical
  obtain ⟨n, rfl⟩ := hf.2 ha hb
  obtain ⟨k, hk⟩ := (Int.mod_modEq n #s).symm.dvd
  refine ⟨n.natMod #s, Int.natMod_lt (Nonempty.card_pos ⟨a, ha⟩).ne', ?_⟩
  rw [← zpow_natCast, Int.natMod,
    Int.toNat_of_nonneg (Int.emod_nonneg _ <| Nat.cast_ne_zero.2
      (Nonempty.card_pos ⟨a, ha⟩).ne'), sub_eq_iff_eq_add'.1 hk, zpow_add, zpow_mul]
  simp only [zpow_natCast, coe_mul, comp_apply, EmbeddingLike.apply_eq_iff_eq]
  exact IsFixedPt.perm_zpow (hf.pow_card_apply ha) _

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
a b : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
hb : b ∈ s
⊢ ∃ n < #s, (f ^ n) a = b

Tactic:
obtain ⟨n, rfl⟩ := hf.2 ha hb

Result:
case intro
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℤ
hb : (f ^ n) a ∈ s
⊢ ∃ n_1 < #s, (f ^ n_1) a = (f ^ n) a

Proof state:
case intro.intro
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℤ
hb : (f ^ n) a ∈ s
k : ℤ
hk : n % ↑(#s) - n = ↑(#s) * k
⊢ ((f ^ #s) ^ k) a = a

Tactic:
exact IsFixedPt.perm_zpow (hf.pow_card_apply ha) _

Result:
no goals

Proof state:
case intro.intro
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℤ
hb : (f ^ n) a ∈ s
k : ℤ
hk : n % ↑(#s) - n = ↑(#s) * k
⊢ (f ^ n * (f ^ ↑(#s)) ^ k) a = (f ^ n) a

Tactic:
simp only [zpow_natCast, coe_mul, comp_apply, EmbeddingLike.apply_eq_iff_eq]

Result:
case intro.intro
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℤ
hb : (f ^ n) a ∈ s
k : ℤ
hk : n % ↑(#s) - n = ↑(#s) * k
⊢ ((f ^ #s) ^ k) a = a