awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
m : ℕ
hm : r = (↑m : ℤ)
div_euc : (↑m : ℤ) + (↑(orderOf g) : ℤ) * q = n ∧ m < orderOf g
this : (g ^ m : (a : α) → α) x = x ↔ g ^ m = 1
hm0 : ¬m = 0
neg : ¬g ^ m = 1
⊢ g ^ m = 1 ↔ m = 0

Tactic:
simp only [hm0, iff_false]

Premises used: iff_false
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
m : ℕ
hm : r = (↑m : ℤ)
div_euc : (↑m : ℤ) + (↑(orderOf g) : ℤ) * q = n ∧ m < orderOf g
this : (g ^ m : (a : α) → α) x = x ↔ g ^ m = 1
hm0 : ¬m = 0
⊢ ¬g ^ m = 1

Tactic:
pow_ne_one_of_lt_orderOf hm0 div_euc.2

Premises used: And.right, pow_ne_one_of_lt_orderOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
m : ℕ
hm : r = (↑m : ℤ)
div_euc : (↑m : ℤ) + (↑(orderOf g) : ℤ) * q = n ∧ m < orderOf g
this : (g ^ m : (a : α) → α) x = x ↔ g ^ m = 1
hm0 : ¬m = 0
⊢ ¬g ^ m = 1

Tactic:
exact pow_ne_one_of_lt_orderOf hm0 div_euc.2

Premises used: And.right, pow_ne_one_of_lt_orderOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
mp :
  (∀ (x : α), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x) → ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
mpr :
  (∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False) → ∀ (x : α), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
⊢ (∀ (x : α), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x) ↔ ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ (x : α), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
x : α
hx : x ∈ l
hx' : x ∈ l'
⊢ (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x

Tactic:
specialize h x
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
x : α
hx : x ∈ l
hx' : x ∈ l'
h : (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
⊢ l.length ≤ 1 ∨ l'.length ≤ 1

Tactic:
rw [formPerm_apply_mem_eq_self_iff _ hl _ hx, formPerm_apply_mem_eq_self_iff _ hl' _ hx'] at h

Premises used: List.formPerm_apply_mem_eq_self_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
x : α
hx : x ∈ l
hx' : x ∈ l'
h : l.length ≤ 1 ∨ l'.length ≤ 1
⊢ False

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
pos : ∀ (hx : x ∈ l), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
neg : ∀ (hx : x ∉ l), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
⊢ (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x

Tactic:
by_cases hx : x ∈ l
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
pos : ∀ (hx' : x ∈ l'), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
neg : ∀ (hx' : x ∉ l'), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
⊢ (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x

Tactic:
by_cases hx' : x ∈ l'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
pos : ∀ (hx' : x ∈ l'), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
neg : ∀ (hx' : x ∉ l'), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
⊢ (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x

Tactic:
on_goal 1 => by_cases hx' : x ∈ l'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
hx' : x ∈ l'
⊢ (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x

Tactic:
(h hx hx').elim

Premises used: False.elim
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
hx' : x ∈ l'
⊢ (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x

Tactic:
exact (h hx hx').elim

Premises used: False.elim
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
hx' : x ∉ l'
⊢ (l'.formPerm : (a : α) → α) x = x

Tactic:
have := List.formPerm_apply_of_notMem ‹_›
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
hx' : x ∉ l'
this : (l'.formPerm : (a : α) → α) x = x
neg : ¬(l.formPerm : (a : α) → α) x = x → (l'.formPerm : (a : α) → α) x = x
⊢ (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∉ l
⊢ (l.formPerm : (a : α) → α) x = x

Tactic:
have := List.formPerm_apply_of_notMem ‹_›
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∉ l
this : (l.formPerm : (a : α) → α) x = x
neg neg₁ : ¬(l.formPerm : (a : α) → α) x = x → (l'.formPerm : (a : α) → α) x = x
⊢ (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
hn : 2 ≤ l.length
nil : ∀ (hl : Nodup.{u_1} (α := α) []) (hn : 2 ≤ length.{u_1} (α := α) []), IsCycle.{u_1} (α := α) (formPerm [])
cons : ∀ (x : α) (l : List α) (hl : (x :: l).Nodup) (hn : 2 ≤ (x :: l).length), (x :: l).formPerm.IsCycle
⊢ l.formPerm.IsCycle

Tactic:
rcases l with - | ⟨x, l⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
hl : Nodup.{u_1} (α := α) []
hn : 2 ≤ length.{u_1} (α := α) []
⊢ IsCycle.{u_1} (α := α) (formPerm [])

Tactic:
norm_num at hn
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
x : α
hl : [x].Nodup
hn : 2 ≤ [x].length
⊢ [x].formPerm.IsCycle

Tactic:
norm_num at hn
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
y : α
l : List α
tail_ih : ∀ (x : α) (hl : (x :: l).Nodup) (hn : 2 ≤ (x :: l).length), (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
h :
  ((x :: y :: l).formPerm : (a : α) → α) x ≠ x ∧
    ∀ ⦃y_1 : α⦄, ((x :: y :: l).formPerm : (a : α) → α) y_1 ≠ y_1 → (x :: y :: l).formPerm.SameCycle x y_1
⊢ (x :: y :: l).formPerm.IsCycle

Tactic:
use x
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
y : α
l : List α
tail_ih : ∀ (x : α) (hl : (x :: l).Nodup) (hn : 2 ≤ (x :: l).length), (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
h : ((x :: y :: l).formPerm : (a : α) → α) x ≠ x
h₁ : ∀ ⦃y_1 : α⦄, ((x :: y :: l).formPerm : (a : α) → α) y_1 ≠ y_1 → (x :: y :: l).formPerm.SameCycle x y_1
⊢ ((x :: y :: l).formPerm : (a : α) → α) x ≠ x ∧
    ∀ ⦃y_1 : α⦄, ((x :: y :: l).formPerm : (a : α) → α) y_1 ≠ y_1 → (x :: y :: l).formPerm.SameCycle x y_1

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
y : α
l : List α
tail_ih : ∀ (x : α) (hl : (x :: l).Nodup) (hn : 2 ≤ (x :: l).length), (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn h h₁ h₂ h₃ : 2 ≤ (x :: y :: l).length
⊢ ((x :: y :: l).formPerm : (a : α) → α) x ≠ x

Tactic:
rwa [formPerm_apply_mem_ne_self_iff _ hl _ mem_cons_self]

Premises used: List.formPerm_apply_mem_ne_self_iff, List.mem_cons_self
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
y : α
l : List α
tail_ih : ∀ (x : α) (hl : (x :: l).Nodup) (hn : 2 ≤ (x :: l).length), (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
w : α
hw : ((x :: y :: l).formPerm : (a : α) → α) w ≠ w
⊢ w ∈ x :: y :: l

Tactic:
have : w ∈ x::y::l := mem_of_formPerm_apply_ne hw
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
y : α
l : List α
tail_ih : ∀ (x : α) (hl : (x :: l).Nodup) (hn : 2 ≤ (x :: l).length), (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
w : α
hw : ((x :: y :: l).formPerm : (a : α) → α) w ≠ w
this : w ∈ x :: y :: l
h :
  ∀ (k : ℕ) (hk : k < (x :: y :: l).length)
    (hw :
      ((x :: y :: l).formPerm : (a : α) → α)
          (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) k hk) ≠
        getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) k hk)
    (this : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) k hk ∈ x :: y :: l),
    (x :: y :: l).formPerm.SameCycle x (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) k hk)
⊢ (x :: y :: l).formPerm.SameCycle x w

Tactic:
obtain ⟨k, hk, rfl⟩ := getElem_of_mem this

Premises used: List.getElem_of_mem, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
y : α
l : List α
tail_ih : ∀ (x : α) (hl : (x :: l).Nodup) (hn : 2 ≤ (x :: l).length), (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
k : ℕ
hk : k < (x :: y :: l).length
hw :
  ((x :: y :: l).formPerm : (a : α) → α)
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) k hk) ≠
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) k hk
this : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) k hk ∈ x :: y :: l
h :
  (HPow.hPow (β := ℤ) (x :: y :: l).formPerm (↑k : ℤ) : (a : α) → α) x =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) k hk
⊢ (x :: y :: l).formPerm.SameCycle x (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) k hk)

Tactic:
use k
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
y : α
l : List α
tail_ih : ∀ (x : α) (hl : (x :: l).Nodup) (hn : 2 ≤ (x :: l).length), (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
k : ℕ
hk : k < (x :: y :: l).length
hw :
  ((x :: y :: l).formPerm : (a : α) → α)
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) k hk) ≠
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) k hk
this : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) k hk ∈ x :: y :: l
⊢ (HPow.hPow (β := ℤ) (x :: y :: l).formPerm (↑k : ℤ) : (a : α) → α) x =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) k hk

Tactic:
simp only [zpow_natCast, formPerm_pow_apply_head _ _ hl k, Nat.mod_eq_of_lt hk]

Premises used: zpow_natCast, List.formPerm_pow_apply_head, Nat.mod_eq_of_lt
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
x : α
l : List α
hl : (x :: l).Nodup
hn : 2 ≤ (x :: l).length
cons : ∀ (x : α) (hl : [x].Nodup) (hn : 2 ≤ [x].length), [x].formPerm.IsCycle
cons₁ :
  ∀ (y : α) (l : List α),
    (∀ (x : α) (hl : (x :: l).Nodup) (hn : 2 ≤ (x :: l).length), (x :: l).formPerm.IsCycle) →
      ∀ (x : α) (hl : (x :: y :: l).Nodup) (hn : 2 ≤ (x :: y :: l).length), (x :: y :: l).formPerm.IsCycle
⊢ (x :: l).formPerm.IsCycle

Tactic:
induction l generalizing x with
  | nil => norm_num at hn
  | cons y l =>
    use x
    constructor
    · rwa [formPerm_apply_mem_ne_self_iff _ hl _ mem_cons_self]
    · intro w hw
      have : w ∈ x::y::l := mem_of_formPerm_apply_ne hw
      obtain ⟨k, hk, rfl⟩ := getElem_of_mem this
      use k
      simp only [zpow_natCast, formPerm_pow_apply_head _ _ hl k, Nat.mod_eq_of_lt hk]

Premises used: zpow_natCast, List.cons, List.formPerm_apply_mem_ne_self_iff, List.mem_cons_self, rfl, List.nil
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
hn : 2 ≤ l.length
⊢ Pairwise l.formPerm.SameCycle l

Tactic:
Pairwise.imp_mem.mpr
    (pairwise_of_forall fun _ _ hx hy =>
      (isCycle_formPerm hl hn).sameCycle ((formPerm_apply_mem_ne_self_iff _ hl _ hx).mpr hn)
        ((formPerm_apply_mem_ne_self_iff _ hl _ hy).mpr hn))

Premises used: Iff.mpr, Equiv.Perm.IsCycle.sameCycle, List.Pairwise.imp_mem, List.pairwise_of_forall, List.formPerm_apply_mem_ne_self_iff, List.isCycle_formPerm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
hn : 2 ≤ l.length
x : { x : α // x ∈ l }
rwa rwa₁ rwa₂ rwa₃ : ∀ (hn : 2 ≤ l.attach.length) (x : { x : α // x ∈ l }), 2 ≤ l.attach.length
⊢ 2 ≤ l.attach.length

Tactic:
rwa [← length_attach] at hn

Premises used: List.length_attach
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
hn_1 : 2 ≤ l.length
x : { x : α // x ∈ l }
hn : 2 ≤ l.attach.length
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hl : l.attach.Nodup) (hn : 2 ≤ l.length) (x : { x : α // x ∈ l }) (hn : 2 ≤ l.attach.length), l.attach.Nodup
⊢ l.attach.Nodup

Tactic:
rwa [← nodup_attach] at hl

Premises used: List.nodup_attach
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
hn : 2 ≤ l.length
⊢ 2 ≤ l.attach.length

Tactic:
rw [← length_attach] at hn

Premises used: List.length_attach
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
hn : 2 ≤ l.attach.length
⊢ l.attach.Nodup

Tactic:
rw [← nodup_attach] at hl

Premises used: List.nodup_attach
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
hn : 2 ≤ l.attach.length
hl₁ : l.attach.Nodup
⊢ 2 ≤ l.attach.length

Tactic:
rw [← nodup_attach] at hl

Premises used: List.nodup_attach
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
rw : (↑(map (Finset.card ∘ support) [l.attach.formPerm]) : Multiset ℕ) = {l.length}
h0 : [l.attach.formPerm].prod = l.attach.formPerm
h1 : ∀ σ ∈ [l.attach.formPerm], σ.IsCycle
h2 : Pairwise Perm.Disjoint [l.attach.formPerm]
⊢ l.attach.formPerm.cycleType = {l.length}

Tactic:
rw [cycleType_eq [l.attach.formPerm]]

Premises used: Equiv.Perm.cycleType_eq, List.cons, List.formPerm, List.attach, List.nil
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
simp : (↑[l.attach.formPerm.support.card] : Multiset ℕ) = {l.length}
⊢ (↑(map (Finset.card ∘ support) [l.attach.formPerm]) : Multiset ℕ) = {l.length}

Tactic:
simp only [map, Function.comp_apply]

Premises used: List.map, Function.comp_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
rw : (↑[l.attach.length] : Multiset ℕ) = {l.length}
rw₁ : ∀ (x : { x : α // x ∈ l }), l.attach ≠ [x]
⊢ (↑[l.attach.formPerm.support.card] : Multiset ℕ) = {l.length}

Tactic:
rw [support_formPerm_of_nodup _ hl, card_toFinset, dedup_eq_self.mpr hl]

Premises used: Iff.mpr, List.dedup_eq_self, List.card_toFinset, List.support_formPerm_of_nodup
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ (↑[l.attach.length] : Multiset ℕ) = {l.length}

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
x : { x : α // x ∈ l }
h : l.attach = [x]
⊢ False

Tactic:
simp [h] at hn
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ [l.attach.formPerm].prod = l.attach.formPerm

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ ∀ σ ∈ [l.attach.formPerm], σ.IsCycle

Tactic:
simpa using isCycle_formPerm hl hn

Premises used: List.isCycle_formPerm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ Pairwise Perm.Disjoint [l.attach.formPerm]

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
obtain :
  ∀ (k : ℕ) (hk : k < l.length) (hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l),
    (l.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) =
      l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) hx
⊢ (l.formPerm : (a : α) → α) x = l.next x hx

Tactic:
obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx

Premises used: List.getElem_of_mem, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
rw :
  (l.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((k + 1) % l.length) ⋯
rw₁ rw₂ :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((k + 1) % l.length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((k + 1) % l.length) ⋯
⊢ (l.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) =
    l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) hx

Tactic:
rw [next_getElem _ hl, formPerm_apply_getElem _ hl]

Premises used: List.formPerm_apply_getElem, List.next_getElem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
s_1 s : Cycle α
l₁ l₂ : List α
h : l₁ ~r l₂
hα : Nodup ⟦l₁⟧ = Nodup ⟦l₂⟧
h₁ : ∀ (a : Nodup ⟦l₁⟧) (a' : Nodup ⟦l₂⟧), a ≍ a' → l₁.formPerm ≍ l₂.formPerm
⊢ HEq.{u_1 + 1} (α := Nodup ⟦l₁⟧ → Equiv.Perm α) fun (x : Nodup ⟦l₁⟧) ↦ l₁.formPerm (β := Nodup ⟦l₂⟧ → Equiv.Perm α)
    fun (x : Nodup ⟦l₂⟧) ↦ l₂.formPerm

Tactic:
apply Function.hfunext

Premises used: Function.hfunext
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
s_1 s : Cycle α
l₁ l₂ : List α
h : l₁ ~r l₂
hα : Nodup ⟦l₁⟧ ↔ Nodup ⟦l₂⟧
⊢ Nodup ⟦l₁⟧ = Nodup ⟦l₂⟧

Tactic:
ext
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
s_1 s : Cycle α
l₁ l₂ : List α
h : l₁ ~r l₂
⊢ Nodup ⟦l₁⟧ ↔ Nodup ⟦l₂⟧

Tactic:
h.nodup_iff

Premises used: List.IsRotated.nodup_iff, Cycle.Nodup
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
s_1 s : Cycle α
l₁ l₂ : List α
h : l₁ ~r l₂
⊢ Nodup ⟦l₁⟧ ↔ Nodup ⟦l₂⟧

Tactic:
exact h.nodup_iff

Premises used: List.IsRotated.nodup_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
s_1 s : Cycle α
l₁ l₂ : List α
h : l₁ ~r l₂
h₁ : Nodup ⟦l₁⟧
h₂ : Nodup ⟦l₂⟧
h₃ : h₁ ≍ h₂ → l₁.formPerm ≍ l₂.formPerm
⊢ h₁ ≍ h₂ → l₁.formPerm ≍ l₂.formPerm

Tactic:
_
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
s_1 s : Cycle α
l₁ l₂ : List α
h : l₁ ~r l₂
h₁ : Nodup ⟦l₁⟧
h₂ : Nodup ⟦l₂⟧
h_1 : h₁ ≍ h₂
⊢ l₁.formPerm ≍ l₂.formPerm

Tactic:
heq_of_eq (formPerm_eq_of_isRotated h₁ h)

Premises used: heq_of_eq, List.formPerm_eq_of_isRotated
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
s_1 s : Cycle α
l₁ l₂ : List α
h : l₁ ~r l₂
h₁ : Nodup ⟦l₁⟧
h₂ : Nodup ⟦l₂⟧
h_1 : h₁ ≍ h₂
⊢ l₁.formPerm ≍ l₂.formPerm

Tactic:
exact heq_of_eq (formPerm_eq_of_isRotated h₁ h)

Premises used: heq_of_eq, List.formPerm_eq_of_isRotated
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
⊢ (↑l : Cycle α).formPerm hl = l.formPerm

Tactic:
rfl

Premises used: List.formPerm, Cycle.ofList, Cycle.formPerm, rfl, List.prod
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
h : s.Subsingleton
mk :
  ∀ (s : List α) (h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)),
    formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) ⋯ = 1
⊢ s.formPerm ⋯ = 1

Tactic:
obtain ⟨s⟩ := s
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
s_1 : Cycle α
s : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
mk : s.formPerm = 1
⊢ formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) ⋯ = 1

Tactic:
simp only [formPerm_coe, mk_eq_coe]

Premises used: Cycle.mk_eq_coe, Cycle.formPerm_coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
s_1 : Cycle α
s : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
⊢ s.length ≤ 1

Tactic:
simp only [length_subsingleton_iff, length_coe, mk_eq_coe] at h

Premises used: Cycle.mk_eq_coe, Cycle.length_subsingleton_iff, Cycle.length_coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
s_1 : Cycle α
s : List α
h : s.length ≤ 1
mk : ∀ (h : List.length.{u_1} (α := α) [] ≤ 1), Eq.{u_1 + 1} (α := Equiv.Perm α) (List.formPerm []) 1
mk₁ : ∀ (hd : α) (tl : List α) (h : (hd :: tl).length ≤ 1), (hd :: tl).formPerm = 1
⊢ s.formPerm = 1

Tactic:
obtain - | ⟨hd, tl⟩ := s
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
h : List.length.{u_1} (α := α) [] ≤ 1
⊢ Eq.{u_1 + 1} (α := Equiv.Perm α) (List.formPerm []) 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
hd : α
tl : List α
h : (hd :: tl).length ≤ 1
⊢ tl = []

Tactic:
simp only [length_eq_zero_iff, add_le_iff_nonpos_left, List.length, nonpos_iff_eq_zero] at h

Premises used: add_le_iff_nonpos_left, List.length, List.length_eq_zero_iff, nonpos_iff_eq_zero
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
hd : α
tl : List α
h : tl = []
⊢ (hd :: tl).formPerm = 1

Tactic:
simp [h]