awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ 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'
have h₁ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l)
    (((k + 1) % (x' :: y' :: l').length + n) % (x :: y :: l).length) sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') ((k + 1) % (x' :: y' :: l').length) sorry
Tactic: conv => congr <;> · arg 2; (rw [← Nat.mod_eq_of_lt hk'])
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ 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) ⋯
have h₁ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l)
    (((k + 1) % (x' :: y' :: l').length + n) % (x :: y :: l).length) sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l)
    (((k + n) % (x :: y :: l).length + 1) % (x :: y :: l).length) sorry
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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ 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) ⋯
have h₁ : ((k + 1) % (x' :: y' :: l').length + n) % (x :: y :: l).length =
  ((k + n) % (x :: y :: l).length + 1) % (x :: y :: l).length
Tactic: congr 1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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 + 1) % (x' :: y' :: l').length + n) % (x :: y :: l).length =
    ((k + n) % (x :: y :: l).length + 1) % (x :: y :: l).length
have h₁ : (k + n + 1) % (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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ 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'
have 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) sorry =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') 0 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
Cleared hypotheses: k, hk, hk'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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'
⊢ 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'
have 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) sorry =
        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) sorry =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') (k + 1) 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
Cleared hypotheses: k, hk, hk'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ (l.formPerm : (a : α) → α) x = x ↔ l.length ≤ 1
have 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
Tactic: obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ (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
have rw : (k + 1) % l.length = k ↔ l.length ≤ 1
Tactic: rw [formPerm_apply_getElem _ hl k hk, hl.getElem_inj_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ (k + 1) % l.length = k ↔ l.length ≤ 1
have zero : ∀ (hn : l.length = 0), (k + 1) % 0 = k ↔ LE.le (α := ℕ) 0 1
Tactic: cases hn : l.length
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ (k + 1) % l.length = k ↔ l.length ≤ 1
have succ : ∀ (n : ℕ) (hn : l.length = n + 1), (k + 1) % (n + 1) = k ↔ n + 1 ≤ 1
Tactic: cases hn : l.length
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
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 + 1) % (n + 1) = k ↔ n + 1 ≤ 1
have hk₁ : k < n + 1
Tactic: rw [hn] at hk
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ (k + 1) % (n + 1) = k ↔ n + 1 ≤ 1
have succ : ∀ (hk' : k = n), (k + 1) % (n + 1) = k ↔ n + 1 ≤ 1
Tactic: rcases (Nat.le_of_lt_succ hk).eq_or_lt with hk' | hk'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ (k + 1) % (n + 1) = k ↔ n + 1 ≤ 1
have succ₁ : ∀ (hk' : k < n), (k + 1) % (n + 1) = k ↔ n + 1 ≤ 1
Tactic: rcases (Nat.le_of_lt_succ hk).eq_or_lt with hk' | hk'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ (l.formPerm : (a : α) → α) x ≠ x ↔ 2 ≤ l.length
have rw : 1 < l.length ↔ 2 ≤ l.length
Tactic: rw [Ne, formPerm_apply_mem_eq_self_iff _ hl x hx, not_le]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
⊢ l.formPerm = 1 ↔ l.length ≤ 1
have nil : ∀ (hl : Nodup.{u_1} (α := α) []), Eq.{u_1 + 1} (α := Equiv.Perm α) (formPerm []) 1 ↔ length.{u_1} (α := α) [] ≤ 1
Tactic: rcases l with - | ⟨hd, tl⟩
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ l.formPerm = 1 ↔ l.length ≤ 1
have cons : ∀ (hd : α) (tl : List α) (hl : (hd :: tl).Nodup), (hd :: tl).formPerm = 1 ↔ (hd :: tl).length ≤ 1
Tactic: rcases l with - | ⟨hd, tl⟩
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
⊢ (hd :: tl).formPerm = 1 ↔ (hd :: tl).length ≤ 1
have cons : (hd :: tl).formPerm = 1 ↔ ((hd :: tl).formPerm : (a : α) → α) hd = hd
Tactic: rw [← formPerm_apply_mem_eq_self_iff _ hl hd mem_cons_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
⊢ (hd :: tl).formPerm = 1 ↔ ((hd :: tl).formPerm : (a : α) → α) hd = hd
have cons : (hd :: tl).formPerm = 1 → ((hd :: tl).formPerm : (a : α) → α) hd = hd
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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).formPerm : (a : α) → α) hd = hd
have cons₁ : ((hd :: tl).formPerm : (a : α) → α) hd = hd → (hd :: tl).formPerm = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
h : ((hd :: tl).formPerm : (a : α) → α) hd = hd
⊢ (hd :: tl).formPerm = 1
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
⊢ l.formPerm = l'.formPerm ↔ l ~r l' ∨ l.length ≤ 1 ∧ l'.length ≤ 1
have nil : ∀ (hl : Nodup.{u_1} (α := α) []), formPerm [] = l'.formPerm ↔ [] ~r l' ∨ length.{u_1} (α := α) [] ≤ 1 ∧ l'.length ≤ 1
Tactic: rcases l with (_ | ⟨x, _ | ⟨y, l⟩⟩)
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ l.formPerm = l'.formPerm ↔ l ~r l' ∨ l.length ≤ 1 ∧ l'.length ≤ 1
have cons : ∀ (x : α) (hl : [x].Nodup), [x].formPerm = l'.formPerm ↔ [x] ~r l' ∨ [x].length ≤ 1 ∧ l'.length ≤ 1
Tactic: rcases l with (_ | ⟨x, _ | ⟨y, l⟩⟩)
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ l.formPerm = l'.formPerm ↔ l ~r l' ∨ l.length ≤ 1 ∧ l'.length ≤ 1
have 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
Tactic: rcases l with (_ | ⟨x, _ | ⟨y, l⟩⟩)
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : Nodup.{u_1} (α := α) []
⊢ formPerm [] = l'.formPerm ↔ [] ~r l' ∨ length.{u_1} (α := α) [] ≤ 1 ∧ l'.length ≤ 1
have nil : l'.length ≤ 1 ↔ l' = [] ∨ 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : Nodup.{u_1} (α := α) []
⊢ l'.length ≤ 1 ↔ l' = [] ∨ l'.length ≤ 1
have nil : l' = [] ∨ l'.length ≤ 1 → l'.length ≤ 1
Tactic: refine ⟨fun h => Or.inr h, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
⊢ [x].formPerm = l'.formPerm ↔ [x] ~r l' ∨ [x].length ≤ 1 ∧ l'.length ≤ 1
have cons : l'.length ≤ 1 ↔ [x] ~r l' ∨ 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
⊢ l'.length ≤ 1 ↔ [x] ~r l' ∨ l'.length ≤ 1
have cons : [x] ~r l' ∨ l'.length ≤ 1 → l'.length ≤ 1
Tactic: refine ⟨fun h => Or.inr h, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l' : List α
hl' : l'.Nodup
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
have cons : ∀ (hl' : Nodup.{u_1} (α := α) []),
  (x :: y :: l).formPerm = formPerm [] ↔ x :: y :: l ~r [] ∨ (x :: y :: l).length ≤ 1 ∧ length.{u_1} (α := α) [] ≤ 1
Tactic: rcases l' with (_ | ⟨x', _ | ⟨y', l'⟩⟩)
Cleared hypotheses: l', hl'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ (x :: y :: l).formPerm = l'.formPerm ↔ x :: y :: l ~r l' ∨ (x :: y :: l).length ≤ 1 ∧ l'.length ≤ 1
have cons₁ : ∀ (x' : α) (hl' : [x'].Nodup),
  (x :: y :: l).formPerm = [x'].formPerm ↔ x :: y :: l ~r [x'] ∨ (x :: y :: l).length ≤ 1 ∧ [x'].length ≤ 1
Tactic: rcases l' with (_ | ⟨x', _ | ⟨y', l'⟩⟩)
Cleared hypotheses: l', hl'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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
⊢ (x :: y :: l).formPerm = l'.formPerm ↔ x :: y :: l ~r l' ∨ (x :: y :: l).length ≤ 1 ∧ l'.length ≤ 1
have 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
Tactic: rcases l' with (_ | ⟨x', _ | ⟨y', l'⟩⟩)
Cleared hypotheses: l', hl'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
⊢ Membership.mem (α := α) l ((l.formPerm ^ n : (a : α) → α) x : α)
have pos : ∀ (h : (l.formPerm ^ n : (a : α) → α) x = x), Membership.mem (α := α) l ((l.formPerm ^ n : (a : α) → α) x : α)
Tactic: by_cases h : (l.formPerm ^ n) x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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 : α)
⊢ Membership.mem (α := α) l ((l.formPerm ^ n : (a : α) → α) x : α)
have neg : ∀ (h : ¬(l.formPerm ^ n : (a : α) → α) x = x), Membership.mem (α := α) l ((l.formPerm ^ n : (a : α) → α) x : α)
Tactic: by_cases h : (l.formPerm ^ n) x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
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 : α)
have h₁ : Membership.mem (γ := Set α) {x : α | (l.formPerm ^ n : (a : α) → α) x ≠ x} x
Tactic: have h : x ∈ { x | (l.formPerm ^ n) x ≠ x } := h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
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 (α := α) l ((l.formPerm ^ n : (a : α) → α) x : α)
have h₁ : Membership.mem (α := α) (γ := Set α) {x : α | (l.formPerm ^ n : (a : α) → α) x ≠ x}
  ((l.formPerm ^ n : (a : α) → α) x : α)
Tactic: rw [← set_support_apply_mem] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
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}
    ((l.formPerm ^ n : (a : α) → α) x : α)
⊢ Membership.mem (α := α) l ((l.formPerm ^ n : (a : α) → α) x : α)
have h₁ : Membership.mem (α := α) (γ := Set α) {x : α | (l.formPerm : (a : α) → α) x ≠ x} ((l.formPerm ^ n : (a : α) → α) x : α)
Tactic: replace h := set_support_zpow_subset _ _ h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
⊢ l.formPerm ^ l.length = 1
have H : ∀ (x : α), Eq (α := α) ((l.formPerm ^ l.length : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
x : α
⊢ Eq (α := α) ((l.formPerm ^ l.length : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
have pos : ∀ (hx : x ∈ l), Eq (α := α) ((l.formPerm ^ l.length : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
Tactic: by_cases hx : x ∈ l
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
x : α
pos : ∀ (hx : x ∈ l), Eq (α := α) ((l.formPerm ^ l.length : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
⊢ Eq (α := α) ((l.formPerm ^ l.length : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
have neg : ∀ (hx : x ∉ l), Eq (α := α) ((l.formPerm ^ l.length : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
Tactic: by_cases hx : x ∈ l
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ Eq (α := α) ((l.formPerm ^ l.length : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
have pos : ∀ (k : ℕ) (hk : k < l.length) (hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l),
  Eq (α := α)
    ((l.formPerm ^ l.length : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) : α)
    ((1 : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) : α)
Tactic: obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
Cleared hypotheses: x, hx