awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
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
have succ : ∀ (h : Nodup.{u_1} (α := α) []) (hn : n + 1 + 1 < length.{u_1} (α := α) []),
  (formPerm [] : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] (n + 1) sorry) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] (n + 1 + 1) hn
Tactic: rcases xs with (_ | ⟨x, _ | ⟨y, l⟩⟩)
Cleared hypotheses: xs, h, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
xs : List α
h : xs.Nodup
hn : n + 1 + 1 < xs.length
succ :
  ∀ (h : Nodup.{u_1} (α := α) []) (hn : n + 1 + 1 < length.{u_1} (α := α) []),
    (formPerm [] : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] (n + 1) ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] (n + 1 + 1) hn
⊢ (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
have succ₁ : ∀ (x : α) (h : [x].Nodup) (hn : n + 1 + 1 < [x].length),
  ([x].formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [x] (n + 1) sorry) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [x] (n + 1 + 1) hn
Tactic: rcases xs with (_ | ⟨x, _ | ⟨y, l⟩⟩)
Cleared hypotheses: xs, h, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
xs : List α
h : xs.Nodup
hn : n + 1 + 1 < xs.length
succ :
  ∀ (h : Nodup.{u_1} (α := α) []) (hn : n + 1 + 1 < length.{u_1} (α := α) []),
    (formPerm [] : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] (n + 1) ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] (n + 1 + 1) hn
succ₁ :
  ∀ (x : α) (h : [x].Nodup) (hn : n + 1 + 1 < [x].length),
    ([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
⊢ (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
have succ₂ : ∀ (x y : α) (l : List α) (h : (x :: y :: l).Nodup) (hn : n + 1 + 1 < (x :: y :: l).length),
  ((x :: y :: l).formPerm : (a : α) → α)
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) (n + 1) sorry) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) (n + 1 + 1) hn
Tactic: rcases xs with (_ | ⟨x, _ | ⟨y, l⟩⟩)
Cleared hypotheses: xs, h, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ ([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
have succ : (1 : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [x] (n + 1) sorry) =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [x] (n + 1 + 1) hn
Tactic: rw [formPerm_singleton, getElem_singleton, getElem_singleton, one_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ ([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
have succ₁ : (1 : (a : α) → α) x = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [x] (n + 1 + 1) hn
Tactic: rw [formPerm_singleton, getElem_singleton, getElem_singleton, one_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ ([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
have succ₂ : (1 : (a : α) → α) x = x
Tactic: rw [formPerm_singleton, getElem_singleton, getElem_singleton, one_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ ([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
have succ₃ : x = x
Tactic: rw [formPerm_singleton, getElem_singleton, getElem_singleton, one_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ ((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
have succ : n + 1 < (y :: l).length
Tactic: specialize IH (y :: l) h.of_cons _
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ ((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
have succ₁ : ∀
  (IH :
    ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n sorry) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) (n + 1) sorry),
  ((x :: y :: l).formPerm : (a : α) → α)
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) (n + 1) sorry) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) (n + 1 + 1) hn
Tactic: specialize IH (y :: l) h.of_cons _
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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) ⋯
⊢ ((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
have succ : Eq (α := α)
  (((y :: l).formPerm : (a : α) → α)
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) (n + 1) sorry) :
    α)
  ((swap x y : (a : α) → α)
      (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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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) ⋯
⊢ 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) :
      α)
have succ : Eq (α := α)
  (((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n sorry) : α)
  ((swap x y : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n sorry) : α)
Tactic: simp only [getElem_cons_succ] at *
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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 ⋯
⊢ 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 ⋯) : α)
have succ : ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n sorry) ≠ x
Tactic: rw [← IH, swap_apply_of_ne_of_ne]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ 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 ⋯) : α)
have succ₁ : ((y :: l).formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l) n sorry) ≠ y
Tactic: rw [← IH, swap_apply_of_ne_of_ne]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
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
⊢ False
have h₁ : (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n sorry :: y :: l).Nodup
Tactic: rw [← hx, IH] at h
Cleared hypotheses: h, IH, hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
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
⊢ False
have h₁ : (x :: getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n sorry :: l).Nodup
Tactic: rw [← hx, IH] at h
Cleared hypotheses: h, IH, hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
h : xs.Nodup
n : ℕ
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
have 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 sorry) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (HAdd.hAdd (α := ℕ) 0 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
Cleared hypotheses: xs, h, n, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ (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
have 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 sorry) =
        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) sorry) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1 + 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
Cleared hypotheses: xs, h, n, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
w : xs.Nodup
i : ℕ
h : i < 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) ⋯
have 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} (α := α) []) sorry
Tactic: rcases xs with - | ⟨x, xs⟩
Cleared hypotheses: xs, w, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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} (α := α) []) ⋯
⊢ (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) ⋯
have 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) sorry
Tactic: rcases xs with - | ⟨x, xs⟩
Cleared hypotheses: xs, w, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
⊢ i ≤ xs.length
have refine : i < xs.length.succ
Tactic: refine Nat.le_of_lt_succ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
i : ℕ
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) ⋯
have this : i ≤ xs.length
Tactic: have : i ≤ xs.length := by
      refine Nat.le_of_lt_succ ?_
      simpa using h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : 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) ⋯
have 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) sorry
Tactic: rcases this.eq_or_lt with (rfl | hn')
Cleared hypotheses: i, h, this
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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) ⋯
⊢ ((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) ⋯
have 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) sorry
Tactic: rcases this.eq_or_lt with (rfl | hn')
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ ((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) ⋯
have cons : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: xs) (i + 1) sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: xs) ((i + 1) % (x :: xs).length) sorry
Tactic: rw [formPerm_apply_lt_getElem (x :: xs) w _ (Nat.succ_lt_succ hn')]