case intro.intro.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hs : Cycle.Nodup s
hf : IsCycle (Cycle.formPerm s hs)
hs' : ∀ (y : Cycle α), (fun s_1 => ∃ h, Cycle.formPerm s_1 h = Cycle.formPerm s hs) y → y = s
⊢ ∃! s_1, Cycle.formPerm ↑s_1 (_ : Cycle.Nodup ↑s_1) = Cycle.formPerm s hs
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
⊢ ∃! s, Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f
obtain ⟨s, ⟨hs, rfl⟩, hs'⟩ := hf.existsUnique_cycle
case intro.intro.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hs : Cycle.Nodup s
hf : IsCycle (Cycle.formPerm s hs)
hs' : ∀ (y : Cycle α), (fun s_1 => ∃ h, Cycle.formPerm s_1 h = Cycle.formPerm s hs) y → y = s
⊢ ∀ (y : { s // Cycle.Nodup s }),
    (fun s_1 => Cycle.formPerm ↑s_1 (_ : Cycle.Nodup ↑s_1) = Cycle.formPerm s hs) y → y = { val := s, property := hs }
case intro.intro.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hs : Cycle.Nodup s
hf : IsCycle (Cycle.formPerm s hs)
hs' : ∀ (y : Cycle α), (fun s_1 => ∃ h, Cycle.formPerm s_1 h = Cycle.formPerm s hs) y → y = s
⊢ ∃! s_1, Cycle.formPerm ↑s_1 (_ : Cycle.Nodup ↑s_1) = Cycle.formPerm s hs
refine' ⟨⟨s, hs⟩, rfl, _⟩
case intro.intro.intro.mk
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hs : Cycle.Nodup s
hf : IsCycle (Cycle.formPerm s hs)
hs' : ∀ (y : Cycle α), (fun s_1 => ∃ h, Cycle.formPerm s_1 h = Cycle.formPerm s hs) y → y = s
t : Cycle α
ht : Cycle.Nodup t
ht' : Cycle.formPerm ↑{ val := t, property := ht } (_ : Cycle.Nodup ↑{ val := t, property := ht }) = Cycle.formPerm s hs
⊢ { val := t, property := ht } = { val := s, property := hs }
case intro.intro.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hs : Cycle.Nodup s
hf : IsCycle (Cycle.formPerm s hs)
hs' : ∀ (y : Cycle α), (fun s_1 => ∃ h, Cycle.formPerm s_1 h = Cycle.formPerm s hs) y → y = s
⊢ ∀ (y : { s // Cycle.Nodup s }),
    (fun s_1 => Cycle.formPerm ↑s_1 (_ : Cycle.Nodup ↑s_1) = Cycle.formPerm s hs) y → y = { val := s, property := hs }
rintro ⟨t, ht⟩ ht'
no goals
case intro.intro.intro.mk
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hs : Cycle.Nodup s
hf : IsCycle (Cycle.formPerm s hs)
hs' : ∀ (y : Cycle α), (fun s_1 => ∃ h, Cycle.formPerm s_1 h = Cycle.formPerm s hs) y → y = s
t : Cycle α
ht : Cycle.Nodup t
ht' : Cycle.formPerm ↑{ val := t, property := ht } (_ : Cycle.Nodup ↑{ val := t, property := ht }) = Cycle.formPerm s hs
⊢ { val := t, property := ht } = { val := s, property := hs }
simpa using hs' _ ⟨ht, ht'⟩