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

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

case intro.mk.intro.refine'_3
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
s : Cycle α
hn : Cycle.Nodup s
hs : Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }) = f
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s => Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f) y → y = { val := s, property := hn }
⊢ ∀ (y : { s // Cycle.Nodup s ∧ Cycle.Nontrivial s }),
    (fun s => Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f) y →
      y = { val := s, property := (_ : Cycle.Nodup s ∧ Cycle.Nontrivial s) }
case intro.mk.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
s : Cycle α
hn : Cycle.Nodup s
hs : Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }) = f
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s => Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f) y → y = { val := s, property := hn }
⊢ ∃! s, Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f
refine' ⟨⟨s, hn, _⟩, _, _⟩
case intro.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
s : Cycle α
hn : Cycle.Nodup s
hs : Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }) = f
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s => Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f) y → y = { val := s, property := hn }
⊢ ¬Cycle.Subsingleton s
case intro.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
s : Cycle α
hn : Cycle.Nodup s
hs : Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }) = f
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s => Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f) y → y = { val := s, property := hn }
⊢ Cycle.Nontrivial s
rw [hn.nontrivial_iff]
case intro.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hn : Cycle.Nodup s
hf : IsCycle (Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }))
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s_1 =>
          Cycle.formPerm ↑s_1 (_ : Cycle.Nodup ↑s_1) =
            Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }))
        y →
      y = { val := s, property := hn }
⊢ ¬Cycle.Subsingleton s
case intro.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
s : Cycle α
hn : Cycle.Nodup s
hs : Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }) = f
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s => Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f) y → y = { val := s, property := hn }
⊢ ¬Cycle.Subsingleton s
subst f
case intro.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hn : Cycle.Nodup s
hf : IsCycle (Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }))
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s_1 =>
          Cycle.formPerm ↑s_1 (_ : Cycle.Nodup ↑s_1) =
            Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }))
        y →
      y = { val := s, property := hn }
H : Cycle.Subsingleton s
⊢ False
case intro.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hn : Cycle.Nodup s
hf : IsCycle (Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }))
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s_1 =>
          Cycle.formPerm ↑s_1 (_ : Cycle.Nodup ↑s_1) =
            Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }))
        y →
      y = { val := s, property := hn }
⊢ ¬Cycle.Subsingleton s
intro H
case intro.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hn : Cycle.Nodup s
hf : IsCycle (Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }))
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s_1 =>
          Cycle.formPerm ↑s_1 (_ : Cycle.Nodup ↑s_1) =
            Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }))
        y →
      y = { val := s, property := hn }
H : Cycle.Subsingleton s
⊢ Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }) = 1
case intro.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hn : Cycle.Nodup s
hf : IsCycle (Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }))
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s_1 =>
          Cycle.formPerm ↑s_1 (_ : Cycle.Nodup ↑s_1) =
            Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }))
        y →
      y = { val := s, property := hn }
H : Cycle.Subsingleton s
⊢ False
refine' hf.ne_one _
no goals
case intro.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hn : Cycle.Nodup s
hf : IsCycle (Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }))
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s_1 =>
          Cycle.formPerm ↑s_1 (_ : Cycle.Nodup ↑s_1) =
            Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }))
        y →
      y = { val := s, property := hn }
H : Cycle.Subsingleton s
⊢ Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }) = 1
simpa using Cycle.formPerm_subsingleton _ H
no goals
case intro.mk.intro.refine'_2
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
s : Cycle α
hn : Cycle.Nodup s
hs : Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }) = f
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s => Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f) y → y = { val := s, property := hn }
⊢ (fun s => Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f)
    { val := s, property := (_ : Cycle.Nodup s ∧ Cycle.Nontrivial s) }
simpa using hs
case intro.mk.intro.refine'_3.mk.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
s : Cycle α
hn : Cycle.Nodup s
hs : Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }) = f
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s => Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f) y → y = { val := s, property := hn }
t : Cycle α
ht : Cycle.Nodup t
ht' : Cycle.Nontrivial t
ht'' :
  Cycle.formPerm ↑{ val := t, property := (_ : Cycle.Nodup t ∧ Cycle.Nontrivial t) }
      (_ : Cycle.Nodup ↑{ val := t, property := (_ : Cycle.Nodup t ∧ Cycle.Nontrivial t) }) =
    f
⊢ { val := t, property := (_ : Cycle.Nodup t ∧ Cycle.Nontrivial t) } =
    { val := s, property := (_ : Cycle.Nodup s ∧ Cycle.Nontrivial s) }
case intro.mk.intro.refine'_3
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
s : Cycle α
hn : Cycle.Nodup s
hs : Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }) = f
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s => Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f) y → y = { val := s, property := hn }
⊢ ∀ (y : { s // Cycle.Nodup s ∧ Cycle.Nontrivial s }),
    (fun s => Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f) y →
      y = { val := s, property := (_ : Cycle.Nodup s ∧ Cycle.Nontrivial s) }
rintro ⟨t, ht, ht'⟩ ht''
no goals
case intro.mk.intro.refine'_3.mk.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
s : Cycle α
hn : Cycle.Nodup s
hs : Cycle.formPerm ↑{ val := s, property := hn } (_ : Cycle.Nodup ↑{ val := s, property := hn }) = f
hs' :
  ∀ (y : { s // Cycle.Nodup s }),
    (fun s => Cycle.formPerm ↑s (_ : Cycle.Nodup ↑s) = f) y → y = { val := s, property := hn }
t : Cycle α
ht : Cycle.Nodup t
ht' : Cycle.Nontrivial t
ht'' :
  Cycle.formPerm ↑{ val := t, property := (_ : Cycle.Nodup t ∧ Cycle.Nontrivial t) }
      (_ : Cycle.Nodup ↑{ val := t, property := (_ : Cycle.Nodup t ∧ Cycle.Nontrivial t) }) =
    f
⊢ { val := t, property := (_ : Cycle.Nodup t ∧ Cycle.Nontrivial t) } =
    { val := s, property := (_ : Cycle.Nodup s ∧ Cycle.Nontrivial s) }
simpa using hs' ⟨t, ht⟩ ht''