case intro.intro
ι : Type ?u.1651424
α : Type u_1
β : Type ?u.1651430
f g : Perm α
s t : Set α
a b✝ x y : α
hf : IsCycleOn f s
hs : Set.Nontrivial s
ha : a ∈ s
b : α
hb : b ∈ s
hba : b ≠ a
⊢ ↑f a ≠ a
ι : Type ?u.1651424
α : Type u_1
β : Type ?u.1651430
f g : Perm α
s t : Set α
a b x y : α
hf : IsCycleOn f s
hs : Set.Nontrivial s
ha : a ∈ s
⊢ ↑f a ≠ a
obtain ⟨b, hb, hba⟩ := hs.exists_ne a
case intro.intro.intro
ι : Type ?u.1651424
α : Type u_1
β : Type ?u.1651430
f g : Perm α
s t : Set α
a b x y : α
hf : IsCycleOn f s
hs : Set.Nontrivial s
ha : a ∈ s
n : ℤ
hb : ↑(f ^ n) a ∈ s
hba : ↑(f ^ n) a ≠ a
⊢ ↑f a ≠ a
case intro.intro
ι : Type ?u.1651424
α : Type u_1
β : Type ?u.1651430
f g : Perm α
s t : Set α
a b✝ x y : α
hf : IsCycleOn f s
hs : Set.Nontrivial s
ha : a ∈ s
b : α
hb : b ∈ s
hba : b ≠ a
⊢ ↑f a ≠ a
obtain ⟨n, rfl⟩ := hf.2 ha hb
no goals
case intro.intro.intro
ι : Type ?u.1651424
α : Type u_1
β : Type ?u.1651430
f g : Perm α
s t : Set α
a b x y : α
hf : IsCycleOn f s
hs : Set.Nontrivial s
ha : a ∈ s
n : ℤ
hb : ↑(f ^ n) a ∈ s
hba : ↑(f ^ n) a ≠ a
⊢ ↑f a ≠ a
exact fun h => hba (IsFixedPt.perm_zpow h n)