case intro
ι : Type ?u.1917955
α : Type u_1
β : Type ?u.1917961
f g : Perm α
t : Set α
a b x y : α
s : Finset α
hs : Set.Finite ↑s
hf : IsCycleOn f ↑s
ha : a ∈ ↑s
hb : b ∈ ↑s
⊢ ∃ n, ↑(f ^ n) a = b
ι : Type ?u.1917955
α : Type u_1
β : Type ?u.1917961
f g : Perm α
s t : Set α
a b x y : α
hs : Set.Finite s
hf : IsCycleOn f s
ha : a ∈ s
hb : b ∈ s
⊢ ∃ n, ↑(f ^ n) a = b
lift s to Finset α using id hs
case intro.intro.intro
ι : Type ?u.1917955
α : Type u_1
β : Type ?u.1917961
f g : Perm α
t : Set α
a b x y : α
s : Finset α
hs : Set.Finite ↑s
hf : IsCycleOn f ↑s
ha : a ∈ ↑s
hb : b ∈ ↑s
n : ℕ
hn : ↑(f ^ n) a = b
⊢ ∃ n, ↑(f ^ n) a = b
case intro
ι : Type ?u.1917955
α : Type u_1
β : Type ?u.1917961
f g : Perm α
t : Set α
a b x y : α
s : Finset α
hs : Set.Finite ↑s
hf : IsCycleOn f ↑s
ha : a ∈ ↑s
hb : b ∈ ↑s
⊢ ∃ n, ↑(f ^ n) a = b
obtain ⟨n, -, hn⟩ := hf.exists_pow_eq ha hb
no goals
case intro.intro.intro
ι : Type ?u.1917955
α : Type u_1
β : Type ?u.1917961
f g : Perm α
t : Set α
a b x y : α
s : Finset α
hs : Set.Finite ↑s
hf : IsCycleOn f ↑s
ha : a ∈ ↑s
hb : b ∈ ↑s
n : ℕ
hn : ↑(f ^ n) a = b
⊢ ∃ n, ↑(f ^ n) a = b
exact ⟨n, hn⟩