awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h :
  ∀ (x_1 : α),
    Eq (α := α) (((x :: y :: l).formPerm : (a : α) → α) x_1 : α) (((x' :: y' :: l').formPerm : (a : α) → α) x_1 : α)
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get (⟨n, hn⟩ : Fin (x :: y :: l).length) = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
k : ℕ
IH :
  ∀ (hk : k < ((x :: y :: l).rotate n).length) (hk' : k < (x' :: y' :: l').length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) ((k + n) % (x :: y :: l).length) ⋯ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') k hk'
hk : k + 1 < ((x :: y :: l).rotate n).length
hk' : k + 1 < (x' :: y' :: l').length
h₁ :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l)
      (((k + 1) % (x' :: y' :: l').length + n) % (x :: y :: l).length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') ((k + 1) % (x' :: y' :: l').length) ⋯
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) ((k + 1 + n) % (x :: y :: l).length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') (k + 1) hk'

Tactic:
conv => congr <;> · arg 2; (rw [← Nat.mod_eq_of_lt hk'])

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h :
  ∀ (x_1 : α),
    Eq (α := α) (((x :: y :: l).formPerm : (a : α) → α) x_1 : α) (((x' :: y' :: l').formPerm : (a : α) → α) x_1 : α)
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get (⟨n, hn⟩ : Fin (x :: y :: l).length) = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
k : ℕ
IH :
  ∀ (hk : k < ((x :: y :: l).rotate n).length) (hk' : k < (x' :: y' :: l').length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) ((k + n) % (x :: y :: l).length) ⋯ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') k hk'
hk : k + 1 < ((x :: y :: l).rotate n).length
hk' : k + 1 < (x' :: y' :: l').length
h₁ :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l)
      (((k + 1) % (x' :: y' :: l').length + n) % (x :: y :: l).length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l)
      (((k + n) % (x :: y :: l).length + 1) % (x :: y :: l).length) ⋯
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l)
      (((k + 1) % (x' :: y' :: l').length + n) % (x :: y :: l).length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') ((k + 1) % (x' :: y' :: l').length) ⋯

Tactic:
rw [← formPerm_apply_getElem _ hd' k (k.lt_succ_self.trans hk'),
        ← IH (k.lt_succ_self.trans hk), ← h, formPerm_apply_getElem _ hd]

Premises used: List.formPerm_apply_getElem, Nat.lt_succ_self, LT.lt.trans
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h :
  ∀ (x_1 : α),
    Eq (α := α) (((x :: y :: l).formPerm : (a : α) → α) x_1 : α) (((x' :: y' :: l').formPerm : (a : α) → α) x_1 : α)
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get (⟨n, hn⟩ : Fin (x :: y :: l).length) = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
k : ℕ
IH :
  ∀ (hk : k < ((x :: y :: l).rotate n).length) (hk' : k < (x' :: y' :: l').length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) ((k + n) % (x :: y :: l).length) ⋯ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') k hk'
hk : k + 1 < ((x :: y :: l).rotate n).length
hk' : k + 1 < (x' :: y' :: l').length
h₁ :
  ((k + 1) % (x' :: y' :: l').length + n) % (x :: y :: l).length =
    ((k + n) % (x :: y :: l).length + 1) % (x :: y :: l).length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l)
      (((k + 1) % (x' :: y' :: l').length + n) % (x :: y :: l).length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l)
      (((k + n) % (x :: y :: l).length + 1) % (x :: y :: l).length) ⋯

Tactic:
congr 1
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h :
  ∀ (x_1 : α),
    Eq (α := α) (((x :: y :: l).formPerm : (a : α) → α) x_1 : α) (((x' :: y' :: l').formPerm : (a : α) → α) x_1 : α)
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get (⟨n, hn⟩ : Fin (x :: y :: l).length) = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
k : ℕ
IH :
  ∀ (hk : k < ((x :: y :: l).rotate n).length) (hk' : k < (x' :: y' :: l').length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) ((k + n) % (x :: y :: l).length) ⋯ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') k hk'
hk : k + 1 < ((x :: y :: l).rotate n).length
hk' : k + 1 < (x' :: y' :: l').length
h₁ : (k + n + 1) % (x' :: y' :: l').length = ((k + n) % (x' :: y' :: l').length + 1) % (x' :: y' :: l').length
⊢ ((k + 1) % (x' :: y' :: l').length + n) % (x :: y :: l).length =
    ((k + n) % (x :: y :: l).length + 1) % (x :: y :: l).length

Tactic:
rw [hl, Nat.mod_eq_of_lt hk', add_right_comm]

Premises used: add_right_comm, Nat.mod_eq_of_lt
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h :
  ∀ (x_1 : α),
    Eq (α := α) (((x :: y :: l).formPerm : (a : α) → α) x_1 : α) (((x' :: y' :: l').formPerm : (a : α) → α) x_1 : α)
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get (⟨n, hn⟩ : Fin (x :: y :: l).length) = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
k : ℕ
IH :
  ∀ (hk : k < ((x :: y :: l).rotate n).length) (hk' : k < (x' :: y' :: l').length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) ((k + n) % (x :: y :: l).length) ⋯ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') k hk'
hk : k + 1 < ((x :: y :: l).rotate n).length
hk' : k + 1 < (x' :: y' :: l').length
⊢ (k + n + 1) % (x' :: y' :: l').length = ((k + n) % (x' :: y' :: l').length + 1) % (x' :: y' :: l').length

Tactic:
apply Nat.add_mod

Premises used: Nat.add_mod
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h :
  ∀ (x_1 : α),
    Eq (α := α) (((x :: y :: l).formPerm : (a : α) → α) x_1 : α) (((x' :: y' :: l').formPerm : (a : α) → α) x_1 : α)
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get (⟨n, hn⟩ : Fin (x :: y :: l).length) = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
k : ℕ
hk : k < ((x :: y :: l).rotate n).length
hk' : k < (x' :: y' :: l').length
h₁ :
  ∀ (hk : 0 < ((x :: y :: l).rotate n).length) (hk' : 0 < (x' :: y' :: l').length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) ((0 + n) % (x :: y :: l).length) ⋯ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') 0 hk'
h₂ :
  ∀ (k : ℕ)
    (IH :
      ∀ (hk : k < ((x :: y :: l).rotate n).length) (hk' : k < (x' :: y' :: l').length),
        getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) ((k + n) % (x :: y :: l).length) ⋯ =
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') k hk')
    (hk : k + 1 < ((x :: y :: l).rotate n).length) (hk' : k + 1 < (x' :: y' :: l').length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) ((k + 1 + n) % (x :: y :: l).length) ⋯ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') (k + 1) hk'
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) ((k + n) % (x :: y :: l).length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') k hk'

Tactic:
induction k with
    | zero =>
      refine Eq.trans ?_ hx'
      congr
      simpa using hn
    | succ k IH =>
      conv => congr <;> · arg 2; (rw [← Nat.mod_eq_of_lt hk'])
      rw [← formPerm_apply_getElem _ hd' k (k.lt_succ_self.trans hk'),
        ← IH (k.lt_succ_self.trans hk), ← h, formPerm_apply_getElem _ hd]
      congr 1
      rw [hl, Nat.mod_eq_of_lt hk', add_right_comm]
      apply Nat.add_mod

Premises used: List.formPerm_apply_getElem, add_right_comm, Nat.mod_eq_of_lt, Nat.add_mod, Eq.trans
-- Module: Mathlib.GroupTheory.Perm.List
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) =
        getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ↔
      l.length ≤ 1
⊢ (l.formPerm : (a : α) → α) x = x ↔ l.length ≤ 1

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

Premises used: List.getElem_of_mem, rfl
-- Module: Mathlib.GroupTheory.Perm.List
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 : (k + 1) % l.length = k ↔ l.length ≤ 1
⊢ (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 hk ↔
    l.length ≤ 1

Tactic:
rw [formPerm_apply_getElem _ hl k hk, hl.getElem_inj_iff]

Premises used: List.Nodup.getElem_inj_iff, List.formPerm_apply_getElem
-- Module: Mathlib.GroupTheory.Perm.List
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
zero : ∀ (hn : l.length = 0), (k + 1) % 0 = k ↔ LE.le (α := ℕ) 0 1
succ : ∀ (n : ℕ) (hn : l.length = n + 1), (k + 1) % (n + 1) = k ↔ n + 1 ≤ 1
⊢ (k + 1) % l.length = k ↔ l.length ≤ 1

Tactic:
cases hn : l.length

Premises used: List.length
-- Module: Mathlib.GroupTheory.Perm.List
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
hn : l.length = 0
⊢ (k + 1) % 0 = k ↔ LE.le (α := ℕ) 0 1

Tactic:
absurd k.zero_le (hk.trans_le hn.le).not_ge

Premises used: Nat.zero_le, Eq.le, absurd, LT.lt.trans_le, LT.lt.not_ge
-- Module: Mathlib.GroupTheory.Perm.List
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
hn : l.length = 0
⊢ (k + 1) % 0 = k ↔ LE.le (α := ℕ) 0 1

Tactic:
exact absurd k.zero_le (hk.trans_le hn.le).not_ge

Premises used: Nat.zero_le, Eq.le, absurd, LT.lt.trans_le, LT.lt.not_ge
-- Module: Mathlib.GroupTheory.Perm.List
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
n : ℕ
hn : l.length = n + 1
⊢ k < n + 1

Tactic:
rw [hn] at hk
-- Module: Mathlib.GroupTheory.Perm.List
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
n : ℕ
hn : l.length = n + 1
hk₁ : k < n + 1
⊢ l.length = n + 1

Tactic:
rw [hn] at hk
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk_1 : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk_1 ∈ l
n : ℕ
hk : k < n + 1
hn : l.length = n + 1
succ : ∀ (hk' : k = n), (k + 1) % (n + 1) = k ↔ n + 1 ≤ 1
succ₁ : ∀ (hk' : k < n), (k + 1) % (n + 1) = k ↔ n + 1 ≤ 1
⊢ (k + 1) % (n + 1) = k ↔ n + 1 ≤ 1

Tactic:
rcases (Nat.le_of_lt_succ hk).eq_or_lt with hk' | hk'

Premises used: LE.le.eq_or_lt, Nat.le_of_lt_succ
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk_1 : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk_1 ∈ l
n : ℕ
hk : k < n + 1
hn : l.length = n + 1
hk' : k = n
⊢ (k + 1) % (n + 1) = k ↔ n + 1 ≤ 1

Tactic:
simp [← hk', eq_comm]

Premises used: eq_comm
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk_1 : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk_1 ∈ l
n : ℕ
hk : k < n + 1
hn : l.length = n + 1
hk' : k < n
⊢ (k + 1) % (n + 1) = k ↔ n + 1 ≤ 1

Tactic:
simpa [Nat.mod_eq_of_lt (Nat.succ_lt_succ hk'), Nat.succ_lt_succ_iff] using
        (k.zero_le.trans_lt hk').ne.symm

Premises used: Nat.succ_lt_succ_iff, Nat.zero_le, Nat.succ_lt_succ, Ne.symm, Nat.mod_eq_of_lt, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
rw : 1 < l.length ↔ 2 ≤ l.length
⊢ (l.formPerm : (a : α) → α) x ≠ x ↔ 2 ≤ l.length

Tactic:
rw [Ne, formPerm_apply_mem_eq_self_iff _ hl x hx, not_le]

Premises used: not_le, Ne, List.formPerm_apply_mem_eq_self_iff
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ 1 < l.length ↔ 2 ≤ l.length

Tactic:
⟨Nat.succ_le_of_lt, Nat.lt_of_succ_le⟩

Premises used: Nat.succ_le_of_lt, Nat.lt_of_succ_le, Iff.intro
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ 1 < l.length ↔ 2 ≤ l.length

Tactic:
exact ⟨Nat.succ_le_of_lt, Nat.lt_of_succ_le⟩
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
nil : ∀ (hl : Nodup.{u_1} (α := α) []), Eq.{u_1 + 1} (α := Equiv.Perm α) (formPerm []) 1 ↔ length.{u_1} (α := α) [] ≤ 1
cons : ∀ (hd : α) (tl : List α) (hl : (hd :: tl).Nodup), (hd :: tl).formPerm = 1 ↔ (hd :: tl).length ≤ 1
⊢ l.formPerm = 1 ↔ l.length ≤ 1

Tactic:
rcases l with - | ⟨hd, tl⟩
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
hl : Nodup.{u_1} (α := α) []
⊢ Eq.{u_1 + 1} (α := Equiv.Perm α) (formPerm []) 1 ↔ length.{u_1} (α := α) [] ≤ 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
cons : (hd :: tl).formPerm = 1 ↔ ((hd :: tl).formPerm : (a : α) → α) hd = hd
⊢ (hd :: tl).formPerm = 1 ↔ (hd :: tl).length ≤ 1

Tactic:
rw [← formPerm_apply_mem_eq_self_iff _ hl hd mem_cons_self]

Premises used: List.formPerm_apply_mem_eq_self_iff, List.mem_cons_self
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
cons : (hd :: tl).formPerm = 1 → ((hd :: tl).formPerm : (a : α) → α) hd = hd
cons₁ : ((hd :: tl).formPerm : (a : α) → α) hd = hd → (hd :: tl).formPerm = 1
⊢ (hd :: tl).formPerm = 1 ↔ ((hd :: tl).formPerm : (a : α) → α) hd = hd

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
⊢ (hd :: tl).formPerm = 1 → ((hd :: tl).formPerm : (a : α) → α) hd = hd

Tactic:
simp +contextual
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
h : ((hd :: tl).formPerm : (a : α) → α) hd = hd
⊢ tl = []

Tactic:
simp only [(hd :: tl).formPerm_apply_mem_eq_self_iff hl hd mem_cons_self,
        add_le_iff_nonpos_left, length, nonpos_iff_eq_zero, length_eq_zero_iff] at h

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

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
nil :
  ∀ (hl : Nodup.{u_1} (α := α) []), formPerm [] = l'.formPerm ↔ [] ~r l' ∨ length.{u_1} (α := α) [] ≤ 1 ∧ l'.length ≤ 1
cons : ∀ (x : α) (hl : [x].Nodup), [x].formPerm = l'.formPerm ↔ [x] ~r l' ∨ [x].length ≤ 1 ∧ l'.length ≤ 1
cons₁ :
  ∀ (x y : α) (l : List α) (hl : (x :: y :: l).Nodup),
    (x :: y :: l).formPerm = l'.formPerm ↔ x :: y :: l ~r l' ∨ (x :: y :: l).length ≤ 1 ∧ l'.length ≤ 1
⊢ l.formPerm = l'.formPerm ↔ l ~r l' ∨ l.length ≤ 1 ∧ l'.length ≤ 1

Tactic:
rcases l with (_ | ⟨x, _ | ⟨y, l⟩⟩)
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : Nodup.{u_1} (α := α) []
this : l'.length ≤ 1 ↔ l' = [] ∨ l'.length ≤ 1
⊢ formPerm [] = l'.formPerm ↔ [] ~r l' ∨ length.{u_1} (α := α) [] ≤ 1 ∧ l'.length ≤ 1

Tactic:
simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero_iff]

Premises used: eq_comm, List.formPerm_eq_one_iff, List.length_eq_zero_iff
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : Nodup.{u_1} (α := α) []
nil : l'.length ≤ 1 ↔ l' = [] ∨ l'.length ≤ 1
⊢ formPerm [] = l'.formPerm ↔ [] ~r l' ∨ length.{u_1} (α := α) [] ≤ 1 ∧ l'.length ≤ 1

Tactic:
suffices l'.length ≤ 1 ↔ l' = nil ∨ l'.length ≤ 1 by
      simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero_iff]
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : Nodup.{u_1} (α := α) []
⊢ l'.length ≤ 1 ↔ l' = [] ∨ l'.length ≤ 1

Tactic:
⟨fun h => Or.inr h, ?_⟩

Premises used: Iff.intro, Or.inr
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : Nodup.{u_1} (α := α) []
nil : l' = [] ∨ l'.length ≤ 1 → l'.length ≤ 1
⊢ l'.length ≤ 1 ↔ l' = [] ∨ l'.length ≤ 1

Tactic:
refine ⟨fun h => Or.inr h, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
hl hl' : Nodup.{u_1} (α := α) []
⊢ length.{u_1} (α := α) [] ≤ 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : Nodup.{u_1} (α := α) []
h : l'.length ≤ 1
⊢ l'.length ≤ 1

Tactic:
h
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : Nodup.{u_1} (α := α) []
h : l'.length ≤ 1
⊢ l'.length ≤ 1

Tactic:
exact h
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
this : l'.length ≤ 1 ↔ [x] ~r l' ∨ l'.length ≤ 1
⊢ [x].formPerm = l'.formPerm ↔ [x] ~r l' ∨ [x].length ≤ 1 ∧ l'.length ≤ 1

Tactic:
simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero_iff, le_rfl]

Premises used: le_rfl, eq_comm, List.formPerm_eq_one_iff, List.length_eq_zero_iff
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
cons : l'.length ≤ 1 ↔ [x] ~r l' ∨ l'.length ≤ 1
⊢ [x].formPerm = l'.formPerm ↔ [x] ~r l' ∨ [x].length ≤ 1 ∧ l'.length ≤ 1

Tactic:
suffices l'.length ≤ 1 ↔ [x] ~r l' ∨ l'.length ≤ 1 by
      simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero_iff, le_rfl]
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
⊢ l'.length ≤ 1 ↔ [x] ~r l' ∨ l'.length ≤ 1

Tactic:
⟨fun h => Or.inr h, ?_⟩

Premises used: Iff.intro, Or.inr
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
cons : [x] ~r l' ∨ l'.length ≤ 1 → l'.length ≤ 1
⊢ l'.length ≤ 1 ↔ [x] ~r l' ∨ l'.length ≤ 1

Tactic:
refine ⟨fun h => Or.inr h, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
h : [x] ~r l'
⊢ l'.length ≤ 1

Tactic:
simp [← h.perm.length_eq]

Premises used: List.Perm.length_eq, List.IsRotated.perm
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
h : l'.length ≤ 1
⊢ l'.length ≤ 1

Tactic:
h
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
h : l'.length ≤ 1
⊢ l'.length ≤ 1

Tactic:
exact h
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l' : List α
hl' : l'.Nodup
x y : α
l : List α
hl : (x :: y :: l).Nodup
cons :
  ∀ (hl' : Nodup.{u_1} (α := α) []),
    (x :: y :: l).formPerm = formPerm [] ↔ x :: y :: l ~r [] ∨ (x :: y :: l).length ≤ 1 ∧ length.{u_1} (α := α) [] ≤ 1
cons₁ :
  ∀ (x' : α) (hl' : [x'].Nodup),
    (x :: y :: l).formPerm = [x'].formPerm ↔ x :: y :: l ~r [x'] ∨ (x :: y :: l).length ≤ 1 ∧ [x'].length ≤ 1
cons₂ :
  ∀ (x' y' : α) (l' : List α) (hl' : (x' :: y' :: l').Nodup),
    (x :: y :: l).formPerm = (x' :: y' :: l').formPerm ↔
      x :: y :: l ~r x' :: y' :: l' ∨ (x :: y :: l).length ≤ 1 ∧ (x' :: y' :: l').length ≤ 1
⊢ (x :: y :: l).formPerm = l'.formPerm ↔ x :: y :: l ~r l' ∨ (x :: y :: l).length ≤ 1 ∧ l'.length ≤ 1

Tactic:
rcases l' with (_ | ⟨x', _ | ⟨y', l'⟩⟩)
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
l : List α
hl : (x :: y :: l).Nodup
hl' : Nodup.{u_1} (α := α) []
⊢ (x :: y :: l).formPerm = formPerm [] ↔ x :: y :: l ~r [] ∨ (x :: y :: l).length ≤ 1 ∧ length.{u_1} (α := α) [] ≤ 1

Tactic:
simp [formPerm_eq_one_iff _ hl, -formPerm_cons_cons]

Premises used: List.formPerm_eq_one_iff, List.formPerm_cons_cons
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
l : List α
hl : (x :: y :: l).Nodup
x' : α
hl' : [x'].Nodup
⊢ (x :: y :: l).formPerm = [x'].formPerm ↔ x :: y :: l ~r [x'] ∨ (x :: y :: l).length ≤ 1 ∧ [x'].length ≤ 1

Tactic:
simp [formPerm_eq_one_iff _ hl, -formPerm_cons_cons]

Premises used: List.formPerm_eq_one_iff, List.formPerm_cons_cons
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
l : List α
hl : (x :: y :: l).Nodup
x' y' : α
l' : List α
hl' : (x' :: y' :: l').Nodup
⊢ (x :: y :: l).formPerm = (x' :: y' :: l').formPerm ↔
    x :: y :: l ~r x' :: y' :: l' ∨ (x :: y :: l).length ≤ 1 ∧ (x' :: y' :: l').length ≤ 1

Tactic:
simp [-formPerm_cons_cons, formPerm_ext_iff hl hl']

Premises used: List.formPerm_cons_cons, List.formPerm_ext_iff
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
pos : ∀ (h : (l.formPerm ^ n : (a : α) → α) x = x), Membership.mem (α := α) l ((l.formPerm ^ n : (a : α) → α) x : α)
neg : ∀ (h : ¬(l.formPerm ^ n : (a : α) → α) x = x), Membership.mem (α := α) l ((l.formPerm ^ n : (a : α) → α) x : α)
⊢ Membership.mem (α := α) l ((l.formPerm ^ n : (a : α) → α) x : α)

Tactic:
by_cases h : (l.formPerm ^ n) x = x

Premises used: List.formPerm, HPow.hPow, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : (l.formPerm ^ n : (a : α) → α) x = x
⊢ Membership.mem (α := α) l ((l.formPerm ^ n : (a : α) → α) x : α)

Tactic:
simpa [h] using hx
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : ¬(l.formPerm ^ n : (a : α) → α) x = x
⊢ Membership.mem (γ := Set α) {x : α | (l.formPerm ^ n : (a : α) → α) x ≠ x} x

Tactic:
have h : x ∈ { x | (l.formPerm ^ n) x ≠ x } := h
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h_1 : ¬(l.formPerm ^ n : (a : α) → α) x = x
h : Membership.mem (γ := Set α) {x : α | (l.formPerm ^ n : (a : α) → α) x ≠ x} x
⊢ Membership.mem (α := α) (γ := Set α) {x : α | (l.formPerm ^ n : (a : α) → α) x ≠ x}
    ((l.formPerm ^ n : (a : α) → α) x : α)

Tactic:
rw [← set_support_apply_mem] at h

Premises used: Equiv.Perm.set_support_apply_mem