-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem Countable.exists_cycleOn (hs : s.Countable) :
    ∃ f : Perm α, f.IsCycleOn s ∧ { x | f x ≠ x } ⊆ s

Proof state:
case inl
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Finite
⊢ ∃ f, f.IsCycleOn s ∧ {x | f x ≠ x} ⊆ s

Tactic:
refine ⟨hs'.toFinset.toList.formPerm, ?_, fun x hx => by
  simpa using List.mem_of_formPerm_apply_ne hx⟩

Result:
case inl
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Finite
⊢ hs'.toFinset.toList.formPerm.IsCycleOn s

Proof state:
case h.e'_3
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Finite
⊢ s = {a | a ∈ hs'.toFinset.toList}

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3.h
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this✝ : Countable ↑s
this : Infinite ↑s
f : ℤ ≃ ↑s
x✝ : α
⊢ x✝ ∈ s ↔ x✝ ∈ Subtype.val '' (⇑f.symm ⁻¹' {x | (Equiv.addRight 1) x ≠ x})

Tactic:
simp

Result:
no goals

Proof state:
case inr.intro
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this✝ : Countable ↑s
this : Infinite ↑s
f : ℤ ≃ ↑s
⊢ ((Equiv.addRight 1).extendDomain f).IsCycleOn s

Tactic:
convert Int.addRight_one_isCycle.isCycleOn.extendDomain f

Result:
case h.e'_3
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this✝ : Countable ↑s
this : Infinite ↑s
f : ℤ ≃ ↑s
⊢ s = Subtype.val ∘ ⇑f '' {x | (Equiv.addRight 1) x ≠ x}

Proof state:
case inr
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this : Countable ↑s
⊢ ∃ f, f.IsCycleOn s ∧ {x | f x ≠ x} ⊆ s

Tactic:
haveI := hs'.to_subtype

Result:
case inr
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this✝ : Countable ↑s
this : Infinite ↑s
⊢ ∃ f, f.IsCycleOn s ∧ {x | f x ≠ x} ⊆ s

Proof state:
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Finite
x : α
hx : x ∈ {x | hs'.toFinset.toList.formPerm x ≠ x}
⊢ x ∈ s

Tactic:
simpa using List.mem_of_formPerm_apply_ne hx

Result:
no goals

Proof state:
case inr
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
⊢ ∃ f, f.IsCycleOn s ∧ {x | f x ≠ x} ⊆ s

Tactic:
haveI := hs.to_subtype

Result:
case inr
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this : Countable ↑s
⊢ ∃ f, f.IsCycleOn s ∧ {x | f x ≠ x} ⊆ s

Proof state:
α : Type u_2
s : Set α
hs : s.Countable
⊢ ∃ f, f.IsCycleOn s ∧ {x | f x ≠ x} ⊆ s

Tactic:
obtain hs' | hs' := s.finite_or_infinite

Result:
case inl
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Finite
⊢ ∃ f, f.IsCycleOn s ∧ {x | f x ≠ x} ⊆ s

case inr
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
⊢ ∃ f, f.IsCycleOn s ∧ {x | f x ≠ x} ⊆ s

Proof state:
case h.e'_3
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this✝ : Countable ↑s
this : Infinite ↑s
f : ℤ ≃ ↑s
⊢ s = Subtype.val ∘ ⇑f '' {x | (Equiv.addRight 1) x ≠ x}

Tactic:
rw [Set.image_comp, Equiv.image_eq_preimage]

Result:
case h.e'_3
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this✝ : Countable ↑s
this : Infinite ↑s
f : ℤ ≃ ↑s
⊢ s = Subtype.val '' (⇑f.symm ⁻¹' {x | (Equiv.addRight 1) x ≠ x})

Proof state:
case inl
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Finite
⊢ hs'.toFinset.toList.formPerm.IsCycleOn s

Tactic:
convert hs'.toFinset.nodup_toList.isCycleOn_formPerm

Result:
case h.e'_3
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Finite
⊢ s = {a | a ∈ hs'.toFinset.toList}

Proof state:
case h.e'_3
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this✝ : Countable ↑s
this : Infinite ↑s
f : ℤ ≃ ↑s
⊢ s = Subtype.val '' (⇑f.symm ⁻¹' {x | (Equiv.addRight 1) x ≠ x})

Tactic:
ext

Result:
case h.e'_3.h
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this✝ : Countable ↑s
this : Infinite ↑s
f : ℤ ≃ ↑s
x✝ : α
⊢ x✝ ∈ s ↔ x✝ ∈ Subtype.val '' (⇑f.symm ⁻¹' {x | (Equiv.addRight 1) x ≠ x})

Proof state:
case inr.intro
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this✝ : Countable ↑s
this : Infinite ↑s
f : ℤ ≃ ↑s
⊢ ∃ f, f.IsCycleOn s ∧ {x | f x ≠ x} ⊆ s

Tactic:
refine ⟨(Equiv.addRight 1).extendDomain f, ?_, fun x hx =>
  of_not_not fun h => hx <| Perm.extendDomain_apply_not_subtype _ _ h⟩

Result:
case inr.intro
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this✝ : Countable ↑s
this : Infinite ↑s
f : ℤ ≃ ↑s
⊢ ((Equiv.addRight 1).extendDomain f).IsCycleOn s

Proof state:
case inr
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this✝ : Countable ↑s
this : Infinite ↑s
⊢ ∃ f, f.IsCycleOn s ∧ {x | f x ≠ x} ⊆ s

Tactic:
obtain ⟨f⟩ : Nonempty (ℤ ≃ s) := inferInstance

Result:
case inr.intro
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this✝ : Countable ↑s
this : Infinite ↑s
f : ℤ ≃ ↑s
⊢ ∃ f, f.IsCycleOn s ∧ {x | f x ≠ x} ⊆ s