Theorem: IMOSL.IMO2017A3.exists_lt_iterate_eq (IMOSLLean4/IMO2017/A3/A3.lean)

State before:
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
⊢ ∃ a b, a < b ∧ f^[a] = f^[b]
Tactic:
obtain ⟨a, b, h, h0⟩ : ∃ a b : ℕ, a ≠ b ∧ f^[a] = f^[b] :=
  Finite.exists_ne_map_eq_of_infinite _
State after:
case intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a b : ℕ
h : a ≠ b
h0 : f^[a] = f^[b]
⊢ ∃ a b, a < b ∧ f^[a] = f^[b]

State before:
case intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a b : ℕ
h : a ≠ b
h0 : f^[a] = f^[b]
⊢ ∃ a b, a < b ∧ f^[a] = f^[b]
Tactic:
exact h.lt_or_lt.elim (λ h ↦ ⟨a, b, h, h0⟩) (λ h ↦ ⟨b, a, h, h0.symm⟩)
State after:
no goals