no goals
ι : Type ?u.1885361
α : Type u_1
β : Type ?u.1885367
f g : Perm α
s✝ t : Set α
a b x y : α
s : Finset α
hf : IsCycleOn f ↑s
ha : a ∈ s
hb : b ∈ s
⊢ ∃ n, n < card s ∧ ↑(f ^ n) a = b
classical
  obtain ⟨n, rfl⟩ := hf.2 ha hb
  obtain ⟨k, hk⟩ := (Int.mod_modEq n s.card).symm.dvd
  refine' ⟨n.natMod s.card, Int.natMod_lt (Nonempty.card_pos ⟨a, ha⟩).ne', _⟩
  rw [← zpow_ofNat, 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_coe_nat, coe_mul, comp_apply, EmbeddingLike.apply_eq_iff_eq]
  exact IsFixedPt.perm_zpow (hf.pow_card_apply ha) _
case intro
ι : Type ?u.1885361
α : Type u_1
β : Type ?u.1885367
f g : Perm α
s✝ t : Set α
a x y : α
s : Finset α
hf : IsCycleOn f ↑s
ha : a ∈ s
n : ℤ
hb : ↑(f ^ n) a ∈ s
⊢ ∃ n_1, n_1 < card s ∧ ↑(f ^ n_1) a = ↑(f ^ n) a
ι : Type ?u.1885361
α : Type u_1
β : Type ?u.1885367
f g : Perm α
s✝ t : Set α
a b x y : α
s : Finset α
hf : IsCycleOn f ↑s
ha : a ∈ s
hb : b ∈ s
⊢ ∃ n, n < card s ∧ ↑(f ^ n) a = b
obtain ⟨n, rfl⟩ := hf.2 ha hb
case intro.intro
ι : Type ?u.1885361
α : Type u_1
β : Type ?u.1885367
f g : Perm α
s✝ t : Set α
a x y : α
s : Finset α
hf : IsCycleOn f ↑s
ha : a ∈ s
n : ℤ
hb : ↑(f ^ n) a ∈ s
k : ℤ
hk : n % ↑(card s) - n = ↑(card s) * k
⊢ ∃ n_1, n_1 < card s ∧ ↑(f ^ n_1) a = ↑(f ^ n) a
case intro
ι : Type ?u.1885361
α : Type u_1
β : Type ?u.1885367
f g : Perm α
s✝ t : Set α
a x y : α
s : Finset α
hf : IsCycleOn f ↑s
ha : a ∈ s
n : ℤ
hb : ↑(f ^ n) a ∈ s
⊢ ∃ n_1, n_1 < card s ∧ ↑(f ^ n_1) a = ↑(f ^ n) a
obtain ⟨k, hk⟩ := (Int.mod_modEq n s.card).symm.dvd
case intro.intro
ι : Type ?u.1885361
α : Type u_1
β : Type ?u.1885367
f g : Perm α
s✝ t : Set α
a x y : α
s : Finset α
hf : IsCycleOn f ↑s
ha : a ∈ s
n : ℤ
hb : ↑(f ^ n) a ∈ s
k : ℤ
hk : n % ↑(card s) - n = ↑(card s) * k
⊢ ↑(f ^ Int.natMod n ↑(card s)) a = ↑(f ^ n) a
case intro.intro
ι : Type ?u.1885361
α : Type u_1
β : Type ?u.1885367
f g : Perm α
s✝ t : Set α
a x y : α
s : Finset α
hf : IsCycleOn f ↑s
ha : a ∈ s
n : ℤ
hb : ↑(f ^ n) a ∈ s
k : ℤ
hk : n % ↑(card s) - n = ↑(card s) * k
⊢ ∃ n_1, n_1 < card s ∧ ↑(f ^ n_1) a = ↑(f ^ n) a
refine' ⟨n.natMod s.card, Int.natMod_lt (Nonempty.card_pos ⟨a, ha⟩).ne', _⟩
case intro.intro
ι : Type ?u.1885361
α : Type u_1
β : Type ?u.1885367
f g : Perm α
s✝ t : Set α
a x y : α
s : Finset α
hf : IsCycleOn f ↑s
ha : a ∈ s
n : ℤ
hb : ↑(f ^ n) a ∈ s
k : ℤ
hk : n % ↑(card s) - n = ↑(card s) * k
⊢ ↑(f ^ n * (f ^ ↑(card s)) ^ k) a = ↑(f ^ n) a
case intro.intro
ι : Type ?u.1885361
α : Type u_1
β : Type ?u.1885367
f g : Perm α
s✝ t : Set α
a x y : α
s : Finset α
hf : IsCycleOn f ↑s
ha : a ∈ s
n : ℤ
hb : ↑(f ^ n) a ∈ s
k : ℤ
hk : n % ↑(card s) - n = ↑(card s) * k
⊢ ↑(f ^ Int.natMod n ↑(card s)) a = ↑(f ^ n) a
rw [← zpow_ofNat, 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]
case intro.intro
ι : Type ?u.1885361
α : Type u_1
β : Type ?u.1885367
f g : Perm α
s✝ t : Set α
a x y : α
s : Finset α
hf : IsCycleOn f ↑s
ha : a ∈ s
n : ℤ
hb : ↑(f ^ n) a ∈ s
k : ℤ
hk : n % ↑(card s) - n = ↑(card s) * k
⊢ ↑((f ^ card s) ^ k) a = a
case intro.intro
ι : Type ?u.1885361
α : Type u_1
β : Type ?u.1885367
f g : Perm α
s✝ t : Set α
a x y : α
s : Finset α
hf : IsCycleOn f ↑s
ha : a ∈ s
n : ℤ
hb : ↑(f ^ n) a ∈ s
k : ℤ
hk : n % ↑(card s) - n = ↑(card s) * k
⊢ ↑(f ^ n * (f ^ ↑(card s)) ^ k) a = ↑(f ^ n) a
simp only [zpow_coe_nat, coe_mul, comp_apply, EmbeddingLike.apply_eq_iff_eq]
no goals
case intro.intro
ι : Type ?u.1885361
α : Type u_1
β : Type ?u.1885367
f g : Perm α
s✝ t : Set α
a x y : α
s : Finset α
hf : IsCycleOn f ↑s
ha : a ∈ s
n : ℤ
hb : ↑(f ^ n) a ∈ s
k : ℤ
hk : n % ↑(card s) - n = ↑(card s) * k
⊢ ↑((f ^ card s) ^ k) a = a
exact IsFixedPt.perm_zpow (hf.pow_card_apply ha) _