case inl
ι : Type ?u.2072778
α : Type u_1
β : Type ?u.2072784
f g : Perm α
t : Set α
a b x y : α
hs : IsCycleOn f ∅
⊢ Set.Countable ∅

case inr.intro
ι : Type ?u.2072778
α : Type u_1
β : Type ?u.2072784
f g : Perm α
s t : Set α
a✝ b x y : α
hs : IsCycleOn f s
a : α
ha : a ∈ s
⊢ Set.Countable s
ι : Type ?u.2072778
α : Type u_1
β : Type ?u.2072784
f g : Perm α
s t : Set α
a b x y : α
hs : IsCycleOn f s
⊢ Set.Countable s
obtain rfl | ⟨a, ha⟩ := s.eq_empty_or_nonempty
no goals
case inl
ι : Type ?u.2072778
α : Type u_1
β : Type ?u.2072784
f g : Perm α
t : Set α
a b x y : α
hs : IsCycleOn f ∅
⊢ Set.Countable ∅
exact Set.countable_empty
no goals
case inr.intro
ι : Type ?u.2072778
α : Type u_1
β : Type ?u.2072784
f g : Perm α
s t : Set α
a✝ b x y : α
hs : IsCycleOn f s
a : α
ha : a ∈ s
⊢ Set.Countable s
exact (Set.countable_range fun n : ℤ => (⇑(f ^ n) : α → α) a).mono (hs.2 ha)