case intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
val✝ : Fintype α
⊢ ∃! s, ∃ h, Cycle.formPerm s h = f
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
⊢ ∃! s, ∃ h, Cycle.formPerm s h = f
cases nonempty_fintype α
case intro.intro.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
val✝ : Fintype α
x : α
hx : ↑f x ≠ x
hy : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
⊢ ∃! s, ∃ h, Cycle.formPerm s h = f
case intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
val✝ : Fintype α
⊢ ∃! s, ∃ h, Cycle.formPerm s h = f
obtain ⟨x, hx, hy⟩ := id hf
case intro.intro.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
val✝ : Fintype α
x : α
hx : ↑f x ≠ x
hy : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
⊢ Cycle.formPerm ↑(toList f x) (_ : Nodup (toList f x)) = f

case intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
val✝ : Fintype α
x : α
hx : ↑f x ≠ x
hy : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
⊢ ∀ (y : Cycle α), (fun s => ∃ h, Cycle.formPerm s h = f) y → y = ↑(toList f x)
case intro.intro.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
val✝ : Fintype α
x : α
hx : ↑f x ≠ x
hy : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
⊢ ∃! s, ∃ h, Cycle.formPerm s h = f
refine' ⟨f.toList x, ⟨nodup_toList f x, _⟩, _⟩
no goals
case intro.intro.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
val✝ : Fintype α
x : α
hx : ↑f x ≠ x
hy : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
⊢ Cycle.formPerm ↑(toList f x) (_ : Nodup (toList f x)) = f
simp [formPerm_toList, hf.cycleOf_eq hx]
case intro.intro.intro.refine'_2.mk.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hx : ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x ≠ x
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
⊢ Quot.mk Setoid.r l = ↑(toList (Cycle.formPerm (Quot.mk Setoid.r l) hn) x)
case intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
val✝ : Fintype α
x : α
hx : ↑f x ≠ x
hy : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
⊢ ∀ (y : Cycle α), (fun s => ∃ h, Cycle.formPerm s h = f) y → y = ↑(toList f x)
rintro ⟨l⟩ ⟨hn, rfl⟩
case intro.intro.intro.refine'_2.mk.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hx : ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x ≠ x
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
⊢ l ~r toList (formPerm l) x
case intro.intro.intro.refine'_2.mk.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hx : ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x ≠ x
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
⊢ Quot.mk Setoid.r l = ↑(toList (Cycle.formPerm (Quot.mk Setoid.r l) hn) x)
simp only [Cycle.mk_eq_coe, Cycle.coe_eq_coe, Subtype.coe_mk, Cycle.formPerm_coe]
case intro.intro.intro.refine'_2.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hx : ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x ≠ x
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
⊢ 2 ≤ length l

case intro.intro.intro.refine'_2.mk.intro.refine'_2
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hx : ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x ≠ x
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
⊢ x ∈ l
case intro.intro.intro.refine'_2.mk.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hx : ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x ≠ x
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
⊢ l ~r toList (formPerm l) x
refine' (toList_formPerm_isRotated_self _ _ hn _ _).symm
case intro.intro.intro.refine'_2.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
hx : length l < 2
⊢ ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x = x
case intro.intro.intro.refine'_2.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hx : ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x ≠ x
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
⊢ 2 ≤ length l
contrapose! hx
case intro.intro.intro.refine'_2.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
hx : length l < 2
⊢ formPerm l = 1
case intro.intro.intro.refine'_2.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
hx : length l < 2
⊢ ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x = x
suffices formPerm l = 1 by simp [this]
case intro.intro.intro.refine'_2.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
hx : length l < 2
⊢ length l ≤ 1
case intro.intro.intro.refine'_2.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
hx : length l < 2
⊢ formPerm l = 1
rw [formPerm_eq_one_iff _ hn]
no goals
case intro.intro.intro.refine'_2.mk.intro.refine'_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
hx : length l < 2
⊢ length l ≤ 1
exact Nat.le_of_lt_succ hx
no goals
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
hx : length l < 2
this : formPerm l = 1
⊢ ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x = x
simp [this]
case intro.intro.intro.refine'_2.mk.intro.refine'_2
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hx : ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x ≠ x
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
⊢ x ∈ toFinset l
case intro.intro.intro.refine'_2.mk.intro.refine'_2
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hx : ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x ≠ x
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
⊢ x ∈ l
rw [← mem_toFinset]
case intro.intro.intro.refine'_2.mk.intro.refine'_2
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hx : ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x ≠ x
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
⊢ x ∈ support (formPerm l)
case intro.intro.intro.refine'_2.mk.intro.refine'_2
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hx : ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x ≠ x
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
⊢ x ∈ toFinset l
refine' support_formPerm_le l _
no goals
case intro.intro.intro.refine'_2.mk.intro.refine'_2
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk Setoid.r l)
hf : IsCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn)
hx : ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) x ≠ x
hy : ∀ ⦃y : α⦄, ↑(Cycle.formPerm (Quot.mk Setoid.r l) hn) y ≠ y → SameCycle (Cycle.formPerm (Quot.mk Setoid.r l) hn) x y
⊢ x ∈ support (formPerm l)
simpa using hx