case inl
ι : Type ?u.1656340
α : Type u_1
β : Type ?u.1656346
f g : Perm α
s t : Set α
a b x y : α
hf : IsCycleOn f s
hs : Set.Subsingleton s
⊢ IsCycleOn (subtypePerm f (_ : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s)) _root_.Set.univ

case inr
ι : Type ?u.1656340
α : Type u_1
β : Type ?u.1656346
f g : Perm α
s t : Set α
a b x y : α
hf : IsCycleOn f s
hs : Set.Nontrivial s
⊢ IsCycleOn (subtypePerm f (_ : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s)) _root_.Set.univ
ι : Type ?u.1656340
α : Type u_1
β : Type ?u.1656346
f g : Perm α
s t : Set α
a b x y : α
hf : IsCycleOn f s
⊢ IsCycleOn (subtypePerm f (_ : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s)) _root_.Set.univ
obtain hs | hs := s.subsingleton_or_nontrivial
case h.e'_3
ι : Type ?u.1656340
α : Type u_1
β : Type ?u.1656346
f g : Perm α
s t : Set α
a b x y : α
hf : IsCycleOn f s
hs : Set.Nontrivial s
⊢ _root_.Set.univ = {x | ↑(subtypePerm f (_ : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s)) x ≠ x}
case inr
ι : Type ?u.1656340
α : Type u_1
β : Type ?u.1656346
f g : Perm α
s t : Set α
a b x y : α
hf : IsCycleOn f s
hs : Set.Nontrivial s
⊢ IsCycleOn (subtypePerm f (_ : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s)) _root_.Set.univ
convert (hf.isCycle_subtypePerm hs).isCycleOn
case h.e'_3
ι : Type ?u.1656340
α : Type u_1
β : Type ?u.1656346
f g : Perm α
s t : Set α
a b x y : α
hf : IsCycleOn f s
hs : Set.Nontrivial s
⊢ ∀ (x : { x // x ∈ s }), x ∈ {x | ↑(subtypePerm f (_ : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s)) x ≠ x}
case h.e'_3
ι : Type ?u.1656340
α : Type u_1
β : Type ?u.1656346
f g : Perm α
s t : Set α
a b x y : α
hf : IsCycleOn f s
hs : Set.Nontrivial s
⊢ _root_.Set.univ = {x | ↑(subtypePerm f (_ : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s)) x ≠ x}
rw [eq_comm, Set.eq_univ_iff_forall]
no goals
case h.e'_3
ι : Type ?u.1656340
α : Type u_1
β : Type ?u.1656346
f g : Perm α
s t : Set α
a b x y : α
hf : IsCycleOn f s
hs : Set.Nontrivial s
⊢ ∀ (x : { x // x ∈ s }), x ∈ {x | ↑(subtypePerm f (_ : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s)) x ≠ x}
exact fun x => ne_of_apply_ne ((↑) : s → α) (hf.apply_ne hs x.2)
case inl
ι : Type ?u.1656340
α : Type u_1
β : Type ?u.1656346
f g : Perm α
s t : Set α
a b x y : α
hf : IsCycleOn f s
hs : Set.Subsingleton s
this : Subsingleton ↑s
⊢ IsCycleOn (subtypePerm f (_ : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s)) _root_.Set.univ
case inl
ι : Type ?u.1656340
α : Type u_1
β : Type ?u.1656346
f g : Perm α
s t : Set α
a b x y : α
hf : IsCycleOn f s
hs : Set.Subsingleton s
⊢ IsCycleOn (subtypePerm f (_ : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s)) _root_.Set.univ
haveI := hs.coe_sort
no goals
case inl
ι : Type ?u.1656340
α : Type u_1
β : Type ?u.1656346
f g : Perm α
s t : Set α
a b x y : α
hf : IsCycleOn f s
hs : Set.Subsingleton s
this : Subsingleton ↑s
⊢ IsCycleOn (subtypePerm f (_ : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s)) _root_.Set.univ
exact isCycleOn_of_subsingleton _ _