awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
val : Fintype α
x : α
y : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).IsCycle
hx : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) x ≠ x
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).SameCycle x y
intro : l ~r l.formPerm.toList x
⊢ Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l =
    (↑((Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).toList x) : Cycle α)

Tactic:
simp only [Cycle.mk_eq_coe, Cycle.coe_eq_coe, Cycle.formPerm_coe]

Premises used: Cycle.mk_eq_coe, Cycle.formPerm_coe, Cycle.coe_eq_coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
val : Fintype α
x : α
y : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).IsCycle
hx : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) x ≠ x
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).SameCycle x y
⊢ l ~r l.formPerm.toList x

Tactic:
(toList_formPerm_isRotated_self _ ?_ hn _ ?_).symm

Premises used: Equiv.Perm.toList_formPerm_isRotated_self, List.IsRotated.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
val : Fintype α
x : α
y : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).IsCycle
hx : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) x ≠ x
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).SameCycle x y
intro : 2 ≤ l.length
intro₁ : x ∈ l
⊢ l ~r l.formPerm.toList x

Tactic:
refine (toList_formPerm_isRotated_self _ ?_ hn _ ?_).symm

Premises used: Equiv.Perm.toList_formPerm_isRotated_self, List.IsRotated.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
val : Fintype α
x : α
y : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).IsCycle
hx : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) x ≠ x
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).SameCycle x y
intro :
  ∀ (hx : l.length < 2),
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) x = x
⊢ 2 ≤ l.length

Tactic:
contrapose! hx
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
val : Fintype α
x : α
y : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).IsCycle
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).SameCycle x y
hx : l.length < 2
this : l.formPerm = 1
⊢ (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) x = x

Tactic:
simp [this]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
val : Fintype α
x : α
y : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).IsCycle
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).SameCycle x y
hx : l.length < 2
intro : l.formPerm = 1
⊢ (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) x = x

Tactic:
suffices formPerm l = 1 by simp [this]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
val : Fintype α
x : α
y : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).IsCycle
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).SameCycle x y
hx : l.length < 2
intro : l.length ≤ 1
⊢ l.formPerm = 1

Tactic:
rw [formPerm_eq_one_iff _ hn]

Premises used: List.formPerm_eq_one_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
val : Fintype α
x : α
y : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).IsCycle
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).SameCycle x y
hx : l.length < 2
⊢ l.length ≤ 1

Tactic:
Nat.le_of_lt_succ hx

Premises used: Nat.le_of_lt_succ
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
val : Fintype α
x : α
y : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).IsCycle
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).SameCycle x y
hx : l.length < 2
⊢ l.length ≤ 1

Tactic:
exact Nat.le_of_lt_succ hx

Premises used: Nat.le_of_lt_succ
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
val : Fintype α
x : α
y : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).IsCycle
hx : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) x ≠ x
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).SameCycle x y
intro : x ∈ l.toFinset
⊢ x ∈ l

Tactic:
rw [← mem_toFinset]

Premises used: List.mem_toFinset
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
val : Fintype α
x : α
y : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).IsCycle
hx : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) x ≠ x
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).SameCycle x y
⊢ x ∈ l.toFinset

Tactic:
support_formPerm_le l ?_

Premises used: List.support_formPerm_le
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
val : Fintype α
x : α
y : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).IsCycle
hx : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) x ≠ x
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).SameCycle x y
intro : x ∈ l.formPerm.support
⊢ x ∈ l.toFinset

Tactic:
refine support_formPerm_le l ?_

Premises used: List.support_formPerm_le
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
val : Fintype α
x : α
y : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).IsCycle
hx : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) x ≠ x
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).SameCycle x y
⊢ x ∈ l.formPerm.support

Tactic:
simpa using hx
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
obtain :
  ∀ (s : Cycle α) (hs : s.Nodup) (hf : (s.formPerm hs).IsCycle)
    (hs' : ∀ (y : Cycle α), (fun (s_1 : Cycle α) ↦ ∃ (h : s_1.Nodup), s_1.formPerm h = s.formPerm hs) y → y = s),
    ∃! s_1 : { s : Cycle α // s.Nodup }, (↑s_1 : Cycle α).formPerm ⋯ = s.formPerm hs
⊢ ∃! s : { s : Cycle α // s.Nodup }, (↑s : Cycle α).formPerm ⋯ = f

Tactic:
obtain ⟨s, ⟨hs, rfl⟩, hs'⟩ := hf.existsUnique_cycle

Premises used: Equiv.Perm.IsCycle.existsUnique_cycle, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
s : Cycle α
hs : s.Nodup
hf : (s.formPerm hs).IsCycle
hs' : ∀ (y : Cycle α), (fun (s_1 : Cycle α) ↦ ∃ (h : s_1.Nodup), s_1.formPerm h = s.formPerm hs) y → y = s
⊢ ∃! s_1 : { s : Cycle α // s.Nodup }, (↑s_1 : Cycle α).formPerm ⋯ = s.formPerm hs

Tactic:
⟨⟨s, hs⟩, rfl, ?_⟩

Premises used: Subtype.mk, ExistsUnique, And.intro, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
s : Cycle α
hs : s.Nodup
hf : (s.formPerm hs).IsCycle
hs' : ∀ (y : Cycle α), (fun (s_1 : Cycle α) ↦ ∃ (h : s_1.Nodup), s_1.formPerm h = s.formPerm hs) y → y = s
refine :
  ∀ (y : { s : Cycle α // s.Nodup }),
    (fun (s_1 : { s : Cycle α // s.Nodup }) ↦ (↑s_1 : Cycle α).formPerm ⋯ = s.formPerm hs) y →
      y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hs
⊢ ∃! s_1 : { s : Cycle α // s.Nodup }, (↑s_1 : Cycle α).formPerm ⋯ = s.formPerm hs

Tactic:
refine ⟨⟨s, hs⟩, rfl, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
s : Cycle α
hs : s.Nodup
hf : (s.formPerm hs).IsCycle
hs' : ∀ (y : Cycle α), (fun (s_1 : Cycle α) ↦ ∃ (h : s_1.Nodup), s_1.formPerm h = s.formPerm hs) y → y = s
t : Cycle α
ht : t.Nodup
ht' : (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) t ht) : Cycle α).formPerm ⋯ = s.formPerm hs
⊢ Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) t ht = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hs

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

Premises used: Exists.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
obtain :
  ∀ (s : Cycle α) (hn : s.Nodup) (hs : (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯ = f)
    (hs' :
      ∀ (y : { s : Cycle α // s.Nodup }),
        (fun (s : { s : Cycle α // s.Nodup }) ↦ (↑s : Cycle α).formPerm ⋯ = f) y →
          y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn),
    ∃! s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }, (↑s : Cycle α).formPerm ⋯ = f
⊢ ∃! s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }, (↑s : Cycle α).formPerm ⋯ = f

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

Premises used: Equiv.Perm.IsCycle.existsUnique_cycle_subtype
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯ = f
hs' :
  ∀ (y : { s : Cycle α // s.Nodup }),
    (fun (s : { s : Cycle α // s.Nodup }) ↦ (↑s : Cycle α).formPerm ⋯ = f) y →
      y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn
⊢ ∃! s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }, (↑s : Cycle α).formPerm ⋯ = f

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

Premises used: Subtype.mk, ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯ = f
hs' :
  ∀ (y : { s : Cycle α // s.Nodup }),
    (fun (s : { s : Cycle α // s.Nodup }) ↦ (↑s : Cycle α).formPerm ⋯ = f) y →
      y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn
refine_1 : s.Nontrivial
refine_2 :
  (fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦ (↑s : Cycle α).formPerm ⋯ = f)
    (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) s ⋯)
refine_3 :
  ∀ (y : { s : Cycle α // s.Nodup ∧ s.Nontrivial }),
    (fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦ (↑s : Cycle α).formPerm ⋯ = f) y →
      y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) s ⋯
⊢ ∃! s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }, (↑s : Cycle α).formPerm ⋯ = f

Tactic:
refine ⟨⟨s, hn, ?_⟩, ?_, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯ = f
hs' :
  ∀ (y : { s : Cycle α // s.Nodup }),
    (fun (s : { s : Cycle α // s.Nodup }) ↦ (↑s : Cycle α).formPerm ⋯ = f) y →
      y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn
refine_1 : ¬s.Subsingleton
⊢ s.Nontrivial

Tactic:
rw [hn.nontrivial_iff]

Premises used: Cycle.Nodup.nontrivial_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯ = f
hs' :
  ∀ (y : { s : Cycle α // s.Nodup }),
    (fun (s : { s : Cycle α // s.Nodup }) ↦ (↑s : Cycle α).formPerm ⋯ = f) y →
      y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn
⊢ ((↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯).IsCycle

Tactic:
subst f
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯ = f
hs' :
  ∀ (y : { s : Cycle α // s.Nodup }),
    (fun (s : { s : Cycle α // s.Nodup }) ↦ (↑s : Cycle α).formPerm ⋯ = f) y →
      y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn
hf₁ : ((↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯).IsCycle
⊢ ∀ (y : { s : Cycle α // s.Nodup }),
    (fun (s_1 : { s : Cycle α // s.Nodup }) ↦
          (↑s_1 : Cycle α).formPerm ⋯ = (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯)
        y →
      y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn

Tactic:
subst f
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
s : Cycle α
hn : s.Nodup
hf : ((↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯).IsCycle
hs' :
  ∀ (y : { s : Cycle α // s.Nodup }),
    (fun (s_1 : { s : Cycle α // s.Nodup }) ↦
          (↑s_1 : Cycle α).formPerm ⋯ = (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯)
        y →
      y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn
H : s.Subsingleton
⊢ False

Tactic:
hf.ne_one ?_

Premises used: Equiv.Perm.IsCycle.ne_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
s : Cycle α
hn : s.Nodup
hf : ((↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯).IsCycle
hs' :
  ∀ (y : { s : Cycle α // s.Nodup }),
    (fun (s_1 : { s : Cycle α // s.Nodup }) ↦
          (↑s_1 : Cycle α).formPerm ⋯ = (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯)
        y →
      y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn
H : s.Subsingleton
refine_1 : (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯ = 1
⊢ False

Tactic:
refine hf.ne_one ?_

Premises used: Equiv.Perm.IsCycle.ne_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
s : Cycle α
hn : s.Nodup
hf : ((↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯).IsCycle
hs' :
  ∀ (y : { s : Cycle α // s.Nodup }),
    (fun (s_1 : { s : Cycle α // s.Nodup }) ↦
          (↑s_1 : Cycle α).formPerm ⋯ = (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯)
        y →
      y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn
H : s.Subsingleton
⊢ (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯ = 1

Tactic:
simpa using Cycle.formPerm_subsingleton _ H

Premises used: Cycle.formPerm_subsingleton
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯ = f
hs' :
  ∀ (y : { s : Cycle α // s.Nodup }),
    (fun (s : { s : Cycle α // s.Nodup }) ↦ (↑s : Cycle α).formPerm ⋯ = f) y →
      y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn
⊢ (fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦ (↑s : Cycle α).formPerm ⋯ = f)
    (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) s ⋯)

Tactic:
simpa using hs
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn) : Cycle α).formPerm ⋯ = f
hs' :
  ∀ (y : { s : Cycle α // s.Nodup }),
    (fun (s : { s : Cycle α // s.Nodup }) ↦ (↑s : Cycle α).formPerm ⋯ = f) y →
      y = Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hn
t : Cycle α
ht : t.Nodup
ht' : t.Nontrivial
ht'' : (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) t ⋯) : Cycle α).formPerm ⋯ = f
⊢ Eq (α := { s : Cycle α // s.Nodup ∧ s.Nontrivial }) (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) t ⋯)
    (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) s ⋯)

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

Premises used: Subtype.mk
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : { s : Cycle α // s.Nodup ∧ s.Nontrivial } → { f : Perm α // f.IsCycle } :=
  fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦
    Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) ((↑s : Cycle α).formPerm ⋯) ⋯
rw : ∀ (b : { f : Perm α // f.IsCycle }), ∃! a : { s : Cycle α // s.Nodup ∧ s.Nontrivial }, f a = b
⊢ Function.Bijective f

Tactic:
rw [Function.bijective_iff_existsUnique]

Premises used: Function.bijective_iff_existsUnique
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f_1 : { s : Cycle α // s.Nodup ∧ s.Nontrivial } → { f : Perm α // f.IsCycle } :=
  fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦
    Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) ((↑s : Cycle α).formPerm ⋯) ⋯
f : Perm α
hf : f.IsCycle
simp : ∃! a : { s : Cycle α // s.Nodup ∧ s.Nontrivial }, (↑(f_1 a) : Perm α) = f
⊢ ∃! a : { s : Cycle α // s.Nodup ∧ s.Nontrivial }, f_1 a = Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) f hf

Tactic:
simp only [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f_1 : { s : Cycle α // s.Nodup ∧ s.Nontrivial } → { f : Perm α // f.IsCycle } :=
  fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦
    Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) ((↑s : Cycle α).formPerm ⋯) ⋯
f : Perm α
hf : f.IsCycle
⊢ ∃! a : { s : Cycle α // s.Nodup ∧ s.Nontrivial }, (↑(f_1 a) : Perm α) = f

Tactic:
hf.existsUnique_cycle_nontrivial_subtype

Premises used: Equiv.Perm.IsCycle.existsUnique_cycle_nontrivial_subtype, Cycle.formPerm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f_1 : { s : Cycle α // s.Nodup ∧ s.Nontrivial } → { f : Perm α // f.IsCycle } :=
  fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦
    Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) ((↑s : Cycle α).formPerm ⋯) ⋯
f : Perm α
hf : f.IsCycle
⊢ ∃! a : { s : Cycle α // s.Nodup ∧ s.Nontrivial }, (↑(f_1 a) : Perm α) = f

Tactic:
exact hf.existsUnique_cycle_nontrivial_subtype

Premises used: Equiv.Perm.IsCycle.existsUnique_cycle_nontrivial_subtype
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x y : α
dsimp :
  Eq (α := α)
    ((((ofSubtype (p := fun (x_1 : α) ↦ f.SameCycle x x_1) : (a : Perm { x_1 : α // f.SameCycle x x_1 }) → Perm α)
              (f.subtypePerm (p := f.SameCycle x) ⋯) :
            Perm α) :
          (a : α) → α)
        y :
      α)
    (if f.SameCycle x y then (f : (a : α) → α) y else y : α)
⊢ Eq (α := α) ((f.cycleOf x : (a : α) → α) y : α) (if f.SameCycle x y then (f : (a : α) → α) y else y : α)

Tactic:
dsimp only [cycleOf]

Premises used: Equiv.Perm.cycleOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x y : α
pos :
  ∀ (h : f.SameCycle x y),
    Eq (α := α)
      ((((ofSubtype (p := fun (x_1 : α) ↦ f.SameCycle x x_1) : (a : Perm { x_1 : α // f.SameCycle x x_1 }) → Perm α)
                (f.subtypePerm (p := f.SameCycle x) ⋯) :
              Perm α) :
            (a : α) → α)
          y :
        α)
      ((f : (a : α) → α) y : α)
neg :
  ∀ (h : ¬f.SameCycle x y),
    (((ofSubtype (p := fun (x_1 : α) ↦ f.SameCycle x x_1) : (a : Perm { x_1 : α // f.SameCycle x x_1 }) → Perm α)
              (f.subtypePerm (p := f.SameCycle x) ⋯) :
            Perm α) :
          (a : α) → α)
        y =
      y
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x_1 : α) ↦ f.SameCycle x x_1) : (a : Perm { x_1 : α // f.SameCycle x x_1 }) → Perm α)
              (f.subtypePerm (p := f.SameCycle x) ⋯) :
            Perm α) :
          (a : α) → α)
        y :
      α)
    (if f.SameCycle x y then (f : (a : α) → α) y else y : α)

Tactic:
split_ifs with h
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x y : α
h pos : f.SameCycle x y
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x_1 : α) ↦ f.SameCycle x x_1) : (a : Perm { x_1 : α // f.SameCycle x x_1 }) → Perm α)
              (f.subtypePerm (p := f.SameCycle x) ⋯) :
            Perm α) :
          (a : α) → α)
        y :
      α)
    ((f : (a : α) → α) y : α)

Tactic:
apply ofSubtype_apply_of_mem

Premises used: Equiv.Perm.ofSubtype_apply_of_mem