awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
IH :
  ∀ (xs : List α) (h : xs.Nodup) (hn : n + 1 < xs.length),
    (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1) hn
x : α
h : [x].Nodup
hn : n + 1 + 1 < [x].length
succ :
  (1 : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [x] (n + 1) ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [x] (n + 1 + 1) hn
succ₁ : (1 : (a : α) → α) x = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [x] (n + 1 + 1) hn
succ₂ : (1 : (a : α) → α) x = x
succ₃ succ₄ : x = x
⊢ ([x].formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [x] (n + 1) ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [x] (n + 1 + 1) hn

Tactic:
rw [formPerm_singleton, getElem_singleton, getElem_singleton, one_apply]

Premises used: List.getElem_singleton, List.formPerm_singleton, Equiv.Perm.one_apply
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
IH :
  ∀ (xs : List α) (h : xs.Nodup) (hn : n + 1 < xs.length),
    (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1) hn
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
succ : n + 1 < (y :: l).length
succ₁ :
  ∀
    (IH :
      ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) =
        getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) (n + 1) ⋯),
    ((x :: y :: l).formPerm : (a : α) → α)
        (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) (n + 1) ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) (n + 1 + 1) hn
⊢ ((x :: y :: l).formPerm : (a : α) → α)
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) (n + 1) ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) (n + 1 + 1) hn

Tactic:
specialize IH (y :: l) h.of_cons _

Premises used: List.cons, List.Nodup.of_cons
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
IH :
  ∀ (xs : List α) (h : xs.Nodup) (hn : n + 1 < xs.length),
    (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1) hn
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
⊢ n + 1 < (y :: l).length

Tactic:
simpa [Nat.succ_lt_succ_iff] using hn

Premises used: Nat.succ_lt_succ_iff
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
IH_1 :
  ∀ (xs : List α) (h : xs.Nodup) (hn : n + 1 < xs.length),
    (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1) hn
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH :
  ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) (n + 1) ⋯
succ :
  Eq (α := α)
    (((y :: l).formPerm : (a : α) → α)
        (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) (n + 1) ⋯) :
      α)
    ((swap x y : (a : α) → α)
        (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) (n + 1 + 1) hn) :
      α)
⊢ ((x :: y :: l).formPerm : (a : α) → α)
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) (n + 1) ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) (n + 1 + 1) hn

Tactic:
simp only [swap_apply_eq_iff, coe_mul, formPerm_cons_cons, Function.comp]

Premises used: Equiv.Perm.coe_mul, Function.comp, Equiv.swap_apply_eq_iff, List.formPerm_cons_cons
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
IH_1 :
  ∀ (xs : List α) (h : xs.Nodup) (hn : n + 1 < xs.length),
    (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1) hn
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH :
  ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) (n + 1) ⋯
succ :
  Eq (α := α)
    (((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) : α)
    ((swap x y : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯) : α)
⊢ Eq (α := α)
    (((y :: l).formPerm : (a : α) → α)
        (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) (n + 1) ⋯) :
      α)
    ((swap x y : (a : α) → α)
        (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) (n + 1 + 1) hn) :
      α)

Tactic:
simp only [getElem_cons_succ] at *

Premises used: List.getElem_cons_succ
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
IH_1 :
  ∀ (xs : List α) (h : xs.Nodup) (hn : n + 1 < xs.length),
    (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1) hn
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH :
  ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯
succ : ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) ≠ x
succ₁ :
  ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) ≠ y
⊢ Eq (α := α)
    (((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) : α)
    ((swap x y : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯) : α)

Tactic:
rw [← IH, swap_apply_of_ne_of_ne]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
IH_1 :
  ∀ (xs : List α) (h : xs.Nodup) (hn : n + 1 < xs.length),
    (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1) hn
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH :
  ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯
hx : ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) = x
⊢ (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯ :: y :: l).Nodup

Tactic:
rw [← hx, IH] at h
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
IH_1 :
  ∀ (xs : List α) (h : xs.Nodup) (hn : n + 1 < xs.length),
    (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1) hn
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH :
  ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯
hx : ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) = x
h₁ : (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯ :: y :: l).Nodup
⊢ ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯

Tactic:
rw [← hx, IH] at h
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
IH_1 :
  ∀ (xs : List α) (h : xs.Nodup) (hn : n + 1 < xs.length),
    (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1) hn
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH :
  ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯
hx : ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) = x
h₁ : (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯ :: y :: l).Nodup
IH₁ :
  ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯
⊢ ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) = x

Tactic:
rw [← hx, IH] at h
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
IH_1 :
  ∀ (xs : List α) (h : xs.Nodup) (hn : n + 1 < xs.length),
    (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1) hn
x y : α
l : List α
hn : n + 1 + 1 < (x :: y :: l).length
h : (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯ :: y :: l).Nodup
IH :
  ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯
hx : ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) = x
⊢ False

Tactic:
simp [getElem_mem] at h

Premises used: List.getElem_mem
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
IH_1 :
  ∀ (xs : List α) (h : xs.Nodup) (hn : n + 1 < xs.length),
    (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1) hn
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH :
  ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯
hx : ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) = y
⊢ (x :: getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯ :: l).Nodup

Tactic:
rw [← hx, IH] at h
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
IH_1 :
  ∀ (xs : List α) (h : xs.Nodup) (hn : n + 1 < xs.length),
    (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1) hn
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH :
  ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯
hx : ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) = y
h₁ : (x :: getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯ :: l).Nodup
⊢ ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯

Tactic:
rw [← hx, IH] at h
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
IH_1 :
  ∀ (xs : List α) (h : xs.Nodup) (hn : n + 1 < xs.length),
    (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1) hn
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH :
  ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯
hx : ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) = y
h₁ : (x :: getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯ :: l).Nodup
IH₁ :
  ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯
⊢ ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) = y

Tactic:
rw [← hx, IH] at h
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
IH_1 :
  ∀ (xs : List α) (h : xs.Nodup) (hn : n + 1 < xs.length),
    (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1) hn
x y : α
l : List α
hn : n + 1 + 1 < (x :: y :: l).length
h : (x :: getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯ :: l).Nodup
IH :
  ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯
hx : ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n ⋯) = y
⊢ False

Tactic:
simp [getElem_mem] at h

Premises used: List.getElem_mem
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
h : xs.Nodup
n : ℕ
hn : n + 1 < xs.length
zero :
  ∀ (xs : List α) (h : xs.Nodup) (hn : HAdd.hAdd (α := ℕ) 0 1 < xs.length),
    (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs 0 ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (HAdd.hAdd (α := ℕ) 0 1) hn
succ :
  ∀ (n : ℕ)
    (IH :
      ∀ (xs : List α) (h : xs.Nodup) (hn : n + 1 < xs.length),
        (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n ⋯) =
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1) hn)
    (xs : List α) (h : xs.Nodup) (hn : n + 1 + 1 < xs.length),
    (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1) ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1 + 1) hn
⊢ (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1) hn

Tactic:
induction n generalizing xs with
  | zero => simpa using formPerm_apply_getElem_zero _ h _
  | succ n IH =>
    rcases xs with (_ | ⟨x, _ | ⟨y, l⟩⟩)
    · simp at hn
    · rw [formPerm_singleton, getElem_singleton, getElem_singleton, one_apply]
    · specialize IH (y :: l) h.of_cons _
      · simpa [Nat.succ_lt_succ_iff] using hn
      simp only [swap_apply_eq_iff, coe_mul, formPerm_cons_cons, Function.comp]
      simp only [getElem_cons_succ] at *
      rw [← IH, swap_apply_of_ne_of_ne] <;>
      · intro hx
        rw [← hx, IH] at h
        simp [getElem_mem] at h

Premises used: Nat.succ_lt_succ_iff, List.getElem_singleton, List.formPerm_singleton, Equiv.Perm.coe_mul, List.formPerm_apply_getElem_zero, Function.comp, Equiv.swap_apply_of_ne_of_ne, Equiv.swap_apply_eq_iff, List.getElem_mem, Equiv.Perm.one_apply, List.formPerm_cons_cons, List.getElem_cons_succ
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
w : xs.Nodup
i : ℕ
h : i < xs.length
nil :
  ∀ (w : Nodup.{u_1} (α := α) []) (h : i < length.{u_1} (α := α) []),
    (formPerm [] : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] i h) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] ((i + 1) % length.{u_1} (α := α) []) ⋯
cons :
  ∀ (x : α) (xs : List α) (w : (x :: xs).Nodup) (h : i < (x :: xs).length),
    ((x :: xs).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: xs) i h) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: xs) ((i + 1) % (x :: xs).length) ⋯
⊢ (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs i h) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs ((i + 1) % xs.length) ⋯

Tactic:
rcases xs with - | ⟨x, xs⟩
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
i : ℕ
w : Nodup.{u_1} (α := α) []
h : i < length.{u_1} (α := α) []
⊢ (formPerm [] : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] i h) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] ((i + 1) % length.{u_1} (α := α) []) ⋯

Tactic:
simp at h
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
⊢ i ≤ xs.length

Tactic:
Nat.le_of_lt_succ ?_

Premises used: Nat.le_of_lt_succ
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
refine : i < xs.length.succ
⊢ i ≤ xs.length

Tactic:
refine Nat.le_of_lt_succ ?_

Premises used: Nat.le_of_lt_succ
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
⊢ i < xs.length.succ

Tactic:
simpa using h
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
⊢ i ≤ xs.length

Tactic:
have : i ≤ xs.length := by
      refine Nat.le_of_lt_succ ?_
      simpa using h
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
cons :
  ∀ (h : xs.length < (x :: xs).length) (this : xs.length ≤ xs.length),
    ((x :: xs).formPerm : (a : α) → α)
        (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: xs) xs.length h) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: xs) ((xs.length + 1) % (x :: xs).length) ⋯
cons₁ :
  ∀ (hn' : i < xs.length),
    ((x :: xs).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: xs) i h) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: xs) ((i + 1) % (x :: xs).length) ⋯
⊢ ((x :: xs).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: xs) i h) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: xs) ((i + 1) % (x :: xs).length) ⋯

Tactic:
rcases this.eq_or_lt with (rfl | hn')

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x : α
xs : List α
w : (x :: xs).Nodup
h : xs.length < (x :: xs).length
this : xs.length ≤ xs.length
⊢ ((x :: xs).formPerm : (a : α) → α)
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: xs) xs.length h) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: xs) ((xs.length + 1) % (x :: xs).length) ⋯

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
hn' : i < xs.length
cons :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: xs) (i + 1) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: xs) ((i + 1) % (x :: xs).length) ⋯
⊢ ((x :: xs).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: xs) i h) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: xs) ((i + 1) % (x :: xs).length) ⋯

Tactic:
rw [formPerm_apply_lt_getElem (x :: xs) w _ (Nat.succ_lt_succ hn')]

Premises used: Nat.succ_lt_succ, List.cons, List.formPerm_apply_lt_getElem
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
hn' : i < xs.length
cons : i + 1 = (i + 1) % (x :: xs).length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: xs) (i + 1) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: xs) ((i + 1) % (x :: xs).length) ⋯

Tactic:
congr
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
hn' : i < xs.length
cons : i + 1 < (x :: xs).length
⊢ i + 1 = (i + 1) % (x :: xs).length

Tactic:
rw [Nat.mod_eq_of_lt]

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
hn' : i < xs.length
⊢ i + 1 < (x :: xs).length

Tactic:
simpa [Nat.succ_eq_add_one]

Premises used: Nat.succ_eq_add_one
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
a : {x : α | (l.formPerm : (a : α) → α) x ≠ x} ≤ (↑l.toFinset : Set α)
a₁ : (↑l.toFinset : Set α) ≤ {x : α | (l.formPerm : (a : α) → α) x ≠ x}
⊢ {x : α | (l.formPerm : (a : α) → α) x ≠ x} = (↑l.toFinset : Set α)

Tactic:
apply _root_.le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
⊢ {x : α | (l.formPerm : (a : α) → α) x ≠ x} ≤ (↑l.toFinset : Set α)

Tactic:
support_formPerm_le' l

Premises used: List.support_formPerm_le'
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
⊢ {x : α | (l.formPerm : (a : α) → α) x ≠ x} ≤ (↑l.toFinset : Set α)

Tactic:
exact support_formPerm_le' l

Premises used: List.support_formPerm_le'
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
x : α
hx : x ∈ (↑l.toFinset : Set α)
⊢ x ∈ l

Tactic:
simp only [Finset.mem_coe, mem_toFinset] at hx

Premises used: List.mem_toFinset, Finset.mem_coe
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
x : α
hx : x ∈ l
a :
  ∀ (n : ℕ) (hn : n < l.length) (hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn ∈ l),
    Membership.mem (γ := Set α) {x : α | (l.formPerm : (a : α) → α) x ≠ x}
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn)
⊢ Membership.mem (γ := Set α) {x : α | (l.formPerm : (a : α) → α) x ≠ x} x

Tactic:
obtain ⟨n, hn, rfl⟩ := getElem_of_mem hx

Premises used: List.getElem_of_mem, rfl