-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem IsCycle.existsUnique_cycle_nontrivial_subtype {f : Perm α} (hf : IsCycle f) :
    ∃! s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }, (s : Cycle α).formPerm s.prop.left = f

Proof state:
case intro.mk.intro.refine_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hn : s.Nodup
hf : ((↑⟨s, hn⟩).formPerm ⋯).IsCycle
hs' : ∀ (y : { s // s.Nodup }), (fun s_1 => (↑s_1).formPerm ⋯ = (↑⟨s, hn⟩).formPerm ⋯) y → y = ⟨s, hn⟩
H : s.Subsingleton
⊢ (↑⟨s, hn⟩).formPerm ⋯ = 1

Tactic:
simpa using Cycle.formPerm_subsingleton _ H

Result:
no goals

Proof state:
case intro.mk.intro.refine_3.mk.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑⟨s, hn⟩).formPerm ⋯ = f
hs' : ∀ (y : { s // s.Nodup }), (fun s => (↑s).formPerm ⋯ = f) y → y = ⟨s, hn⟩
t : Cycle α
ht : t.Nodup
ht' : t.Nontrivial
ht'' : (↑⟨t, ⋯⟩).formPerm ⋯ = f
⊢ ⟨t, ⋯⟩ = ⟨s, ⋯⟩

Tactic:
simpa using hs' ⟨t, ht⟩ ht''

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
⊢ ∃! s, (↑s).formPerm ⋯ = f

Tactic:
obtain ⟨⟨s, hn⟩, hs, hs'⟩ := hf.existsUnique_cycle_subtype

Result:
case intro.mk.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑⟨s, hn⟩).formPerm ⋯ = f
hs' : ∀ (y : { s // s.Nodup }), (fun s => (↑s).formPerm ⋯ = f) y → y = ⟨s, hn⟩
⊢ ∃! s, (↑s).formPerm ⋯ = f

Proof state:
case intro.mk.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑⟨s, hn⟩).formPerm ⋯ = f
hs' : ∀ (y : { s // s.Nodup }), (fun s => (↑s).formPerm ⋯ = f) y → y = ⟨s, hn⟩
⊢ ∃! s, (↑s).formPerm ⋯ = f

Tactic:
refine ⟨⟨s, hn, ?_⟩, ?_, ?_⟩

Result:
case intro.mk.intro.refine_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑⟨s, hn⟩).formPerm ⋯ = f
hs' : ∀ (y : { s // s.Nodup }), (fun s => (↑s).formPerm ⋯ = f) y → y = ⟨s, hn⟩
⊢ s.Nontrivial

case intro.mk.intro.refine_2
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑⟨s, hn⟩).formPerm ⋯ = f
hs' : ∀ (y : { s // s.Nodup }), (fun s => (↑s).formPerm ⋯ = f) y → y = ⟨s, hn⟩
⊢ (fun s => (↑s).formPerm ⋯ = f) ⟨s, ⋯⟩

case intro.mk.intro.refine_3
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑⟨s, hn⟩).formPerm ⋯ = f
hs' : ∀ (y : { s // s.Nodup }), (fun s => (↑s).formPerm ⋯ = f) y → y = ⟨s, hn⟩
⊢ ∀ (y : { s // s.Nodup ∧ s.Nontrivial }), (fun s => (↑s).formPerm ⋯ = f) y → y = ⟨s, ⋯⟩

Proof state:
case intro.mk.intro.refine_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hn : s.Nodup
hf : ((↑⟨s, hn⟩).formPerm ⋯).IsCycle
hs' : ∀ (y : { s // s.Nodup }), (fun s_1 => (↑s_1).formPerm ⋯ = (↑⟨s, hn⟩).formPerm ⋯) y → y = ⟨s, hn⟩
H : s.Subsingleton
⊢ False

Tactic:
refine hf.ne_one ?_

Result:
case intro.mk.intro.refine_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hn : s.Nodup
hf : ((↑⟨s, hn⟩).formPerm ⋯).IsCycle
hs' : ∀ (y : { s // s.Nodup }), (fun s_1 => (↑s_1).formPerm ⋯ = (↑⟨s, hn⟩).formPerm ⋯) y → y = ⟨s, hn⟩
H : s.Subsingleton
⊢ (↑⟨s, hn⟩).formPerm ⋯ = 1

Proof state:
case intro.mk.intro.refine_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hn : s.Nodup
hf : ((↑⟨s, hn⟩).formPerm ⋯).IsCycle
hs' : ∀ (y : { s // s.Nodup }), (fun s_1 => (↑s_1).formPerm ⋯ = (↑⟨s, hn⟩).formPerm ⋯) y → y = ⟨s, hn⟩
⊢ ¬s.Subsingleton

Tactic:
intro H

Result:
case intro.mk.intro.refine_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hn : s.Nodup
hf : ((↑⟨s, hn⟩).formPerm ⋯).IsCycle
hs' : ∀ (y : { s // s.Nodup }), (fun s_1 => (↑s_1).formPerm ⋯ = (↑⟨s, hn⟩).formPerm ⋯) y → y = ⟨s, hn⟩
H : s.Subsingleton
⊢ False

Proof state:
case intro.mk.intro.refine_3
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑⟨s, hn⟩).formPerm ⋯ = f
hs' : ∀ (y : { s // s.Nodup }), (fun s => (↑s).formPerm ⋯ = f) y → y = ⟨s, hn⟩
⊢ ∀ (y : { s // s.Nodup ∧ s.Nontrivial }), (fun s => (↑s).formPerm ⋯ = f) y → y = ⟨s, ⋯⟩

Tactic:
rintro ⟨t, ht, ht'⟩ ht''

Result:
case intro.mk.intro.refine_3.mk.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑⟨s, hn⟩).formPerm ⋯ = f
hs' : ∀ (y : { s // s.Nodup }), (fun s => (↑s).formPerm ⋯ = f) y → y = ⟨s, hn⟩
t : Cycle α
ht : t.Nodup
ht' : t.Nontrivial
ht'' : (↑⟨t, ⋯⟩).formPerm ⋯ = f
⊢ ⟨t, ⋯⟩ = ⟨s, ⋯⟩

Proof state:
case intro.mk.intro.refine_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑⟨s, hn⟩).formPerm ⋯ = f
hs' : ∀ (y : { s // s.Nodup }), (fun s => (↑s).formPerm ⋯ = f) y → y = ⟨s, hn⟩
⊢ ¬s.Subsingleton

Tactic:
subst f

Result:
case intro.mk.intro.refine_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hn : s.Nodup
hf : ((↑⟨s, hn⟩).formPerm ⋯).IsCycle
hs' : ∀ (y : { s // s.Nodup }), (fun s_1 => (↑s_1).formPerm ⋯ = (↑⟨s, hn⟩).formPerm ⋯) y → y = ⟨s, hn⟩
⊢ ¬s.Subsingleton

Proof state:
case intro.mk.intro.refine_2
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑⟨s, hn⟩).formPerm ⋯ = f
hs' : ∀ (y : { s // s.Nodup }), (fun s => (↑s).formPerm ⋯ = f) y → y = ⟨s, hn⟩
⊢ (fun s => (↑s).formPerm ⋯ = f) ⟨s, ⋯⟩

Tactic:
simpa using hs

Result:
no goals

Proof state:
case intro.mk.intro.refine_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑⟨s, hn⟩).formPerm ⋯ = f
hs' : ∀ (y : { s // s.Nodup }), (fun s => (↑s).formPerm ⋯ = f) y → y = ⟨s, hn⟩
⊢ s.Nontrivial

Tactic:
rw [hn.nontrivial_iff]

Result:
case intro.mk.intro.refine_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑⟨s, hn⟩).formPerm ⋯ = f
hs' : ∀ (y : { s // s.Nodup }), (fun s => (↑s).formPerm ⋯ = f) y → y = ⟨s, hn⟩
⊢ ¬s.Subsingleton