f^[n] x = x

Stream: Is there code for X?

[Patrick Johnson]

Any easy way to prove this lemma? It looks trivial, but I can't find a short proof.
Is there some similar lemma in mathlib that can be applied here?

example {α : Type*} [nonempty α] [fintype α]
  {f : α → α} :
  ∃ (x : α) (n : ℕ), 0 < n ∧ (f^[n]) x = x :=
begin
  sorry
end

My attempt

example {α : Type*} [nonempty α] [fintype α]
  {f : α → α} :
  ∃ (x : α) (n : ℕ), 0 < n ∧ (f^[n]) x = x :=
begin
  tactic.unfreeze_local_instances,
  obtain ⟨s, hs⟩ := id _inst_2,
  generalize n_def : s.card = n,
  induction n with n hn generalizing α,
  { obtain ⟨x₀⟩ := id _inst_1,
    rw finset.card_eq_zero at n_def,
    subst n_def,
    exact (finset.not_mem_empty _).elim (hs x₀) },
  { obtain ⟨x₀⟩ := id _inst_1,
    by_cases hx : ∀ (x : α), x = x₀,
    { refine ⟨x₀, 1, nat.zero_lt_one, hx _⟩, },
    push_neg at hx, cases hx with x₁ hx₁,
    by_cases hf : f x₁ = x₁,
    { refine ⟨x₁, 1, nat.zero_lt_one, hf⟩ },
    have h₁ : nonempty {x : α // x ≠ x₁},
    { use x₀, symmetry, apply hx₁ },
    have h₂ : fintype {x : α // x ≠ x₁},
    { apply fintype_of_finset_card_le s.card,
      rintro s₁,
      fapply finset.card_le_card_of_inj_on,
      { rintro ⟨x₂, hx₂⟩, exact x₂ },
      { rintro ⟨x₂, hx₁⟩ hx₂, dsimp, apply hs },
      { rintro ⟨x₃, hx₁⟩ hx₂ ⟨x₄, hx₃⟩ hx₄ hx₅,
        dsimp at hx₅, congr, exact hx₅ }},
    generalize f₁_def : (by {
      rintro ⟨x, hx⟩, by_cases f x = x₁,
      { use f (f x), rw h, exact hf },
      { use f x }} : {x : α // x ≠ x₁} → {x : α // x ≠ x₁}) = f₁,
    obtain ⟨s₁, hs₁⟩ := id h₂,
    have h₄ : s₁.card = n,
    sorry, -- `s₁` is effectively `s` without `x₁`, so `s₁.card = s.card - 1`
    replace hn := @hn {x : α // x ≠ x₁} h₁ h₂ f₁ s₁ hs₁ h₄,
    rcases hn with ⟨⟨x₂, hx₂⟩, n₂, h₅, h₆⟩,
    use x₂,
    sorry, -- if `f₁` goes through `x₁`, then `n₂ - 1`, else `n₂`,
           -- then use induction on `n₂`
  },
end

[Kevin Buzzard]

My instinct would be to get an element a of alpha, define a map from the natural numbers into alpha sending n to f^n(a), use a result from the library saying this isn't injective and put things together from there

[Alex J. Best]

A rough proof, its basically what kevin said

import data.fintype.basic
import logic.function.iterate

example {α : Type*} [nonempty α] [fintype α]
  {f : α → α} :
  ∃ (x : α) (n : ℕ), 0 < n ∧ (f^[n]) x = x :=
begin
  by_contra',
  apply nonempty.elim ‹_›, -- I'm not sure what the cleanest way to do this is
  intro y,
  have := not_injective_infinite_fintype (λ n, f^[n] y),
  rw function.injective at this,
  push_neg at this,
  rcases this with ⟨a, b, h, hh⟩,
  cases lt_or_gt_of_ne hh with hlt hlt;
  rw [← tsub_add_cancel_of_le (le_of_lt hlt), function.iterate_add_apply] at h,
  exact this (f^[a] y) (b - a) (tsub_pos_of_lt hlt) h.symm,
  exact this (f^[b] y) (a - b) (tsub_pos_of_lt hlt) h,
end

[Alex J. Best]

(deleted)