case intro
ι : Type ?u.1655743
α : Type u_1
β : Type ?u.1655749
f g : Perm α
s t : Set α
a✝ b x y : α
hf : IsCycleOn f s
hs : Set.Nontrivial s
a : α
ha : a ∈ s
⊢ IsCycle (subtypePerm f (_ : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s))
ι : Type ?u.1655743
α : Type u_1
β : Type ?u.1655749
f g : Perm α
s t : Set α
a b x y : α
hf : IsCycleOn f s
hs : Set.Nontrivial s
⊢ IsCycle (subtypePerm f (_ : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s))
obtain ⟨a, ha⟩ := hs.nonempty
no goals
case intro
ι : Type ?u.1655743
α : Type u_1
β : Type ?u.1655749
f g : Perm α
s t : Set α
a✝ b x y : α
hf : IsCycleOn f s
hs : Set.Nontrivial s
a : α
ha : a ∈ s
⊢ IsCycle (subtypePerm f (_ : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s))
exact
  ⟨⟨a, ha⟩, ne_of_apply_ne ((↑) : s → α) (hf.apply_ne hs ha), fun b _ =>
    (hf.2 (⟨a, ha⟩ : s).2 b.2).subtypePerm⟩