awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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) ⋯
have cons : i + 1 = (i + 1) % (x :: xs).length
Tactic: congr
-- 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
⊢ i + 1 = (i + 1) % (x :: xs).length
have cons : i + 1 < (x :: xs).length
Tactic: rw [Nat.mod_eq_of_lt]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
⊢ {x : α | (l.formPerm : (a : α) → α) x ≠ x} = (↑l.toFinset : Set α)
have a : {x : α | (l.formPerm : (a : α) → α) x ≠ x} ≤ (↑l.toFinset : Set α)
Tactic: apply _root_.le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
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 α)
⊢ {x : α | (l.formPerm : (a : α) → α) x ≠ x} = (↑l.toFinset : Set α)
have a₁ : (↑l.toFinset : Set α) ≤ {x : α | (l.formPerm : (a : α) → α) x ≠ x}
Tactic: apply _root_.le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
x : α
hx : x ∈ (↑l.toFinset : Set α)
⊢ Membership.mem (γ := Set α) {x : α | (l.formPerm : (a : α) → α) x ≠ x} x
have hx₁ : x ∈ l
Tactic: simp only [Finset.mem_coe, mem_toFinset] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
x : α
hx : x ∈ l
⊢ Membership.mem (γ := Set α) {x : α | (l.formPerm : (a : α) → α) x ≠ x} x
have 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)
Tactic: obtain ⟨n, hn, 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 α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
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)
have a : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + 1) % l.length) sorry ≠
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn
Tactic: rw [Set.mem_setOf_eq, formPerm_apply_getElem _ h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn ∈ l
H :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + 1) % l.length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn
⊢ False
have a : ∀ (h : ∀ ⦃a₁ a₂ : Fin l.length⦄, l.get a₁ = l.get a₂ → a₁ = a₂) (h' : ∀ (x : α), l ≠ [x]) (n : ℕ) (hn : n < l.length)
  (hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn ∈ l)
  (H :
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + 1) % l.length) sorry =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn),
  False
Tactic: rw [nodup_iff_injective_get, Function.Injective] at h
Cleared hypotheses: h, h', n, hn, hx, H
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : ∀ ⦃a₁ a₂ : Fin l.length⦄, l.get a₁ = l.get a₂ → a₁ = a₂
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn ∈ l
H :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + 1) % l.length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn
⊢ False
have h₁ : (⟨(n + 1) % l.length, sorry⟩ : Fin l.length) = ⟨n, hn⟩
Tactic: specialize h H
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn ∈ l
H :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + 1) % l.length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn
h : (⟨(n + 1) % l.length, ⋯⟩ : Fin l.length) = ⟨n, hn⟩
⊢ False
have a : ∀ (hn' : n.succ = l.length), False
Tactic: rcases (Nat.succ_le_of_lt hn).eq_or_lt with hn' | hn'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn ∈ l
H :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + 1) % l.length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn
h : (⟨(n + 1) % l.length, ⋯⟩ : Fin l.length) = ⟨n, hn⟩
a : ∀ (hn' : n.succ = l.length), False
⊢ False
have a₁ : ∀ (hn' : n.succ < l.length), False
Tactic: rcases (Nat.succ_le_of_lt hn).eq_or_lt with hn' | hn'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn ∈ l
H :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + 1) % l.length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn
h : (⟨(n + 1) % l.length, ⋯⟩ : Fin l.length) = ⟨n, hn⟩
hn' : n.succ = l.length
⊢ False
have h₁ : ⟨0, sorry⟩ = (⟨n, hn⟩ : Fin l.length)
Tactic: simp only [← hn', Nat.mod_self] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn ∈ l
H :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + 1) % l.length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn
hn' : n.succ = l.length
h : ⟨0, ⋯⟩ = (⟨n, hn⟩ : Fin l.length)
⊢ False
have a : ∃ (x : α), l = [x]
Tactic: refine not_exists.mpr h' ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn ∈ l
H :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + 1) % l.length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn
hn' : n.succ = l.length
h : ⟨0, ⋯⟩ = (⟨n, hn⟩ : Fin l.length)
⊢ ∃ (x : α), l = [x]
have a : l.length = 1
Tactic: rw [← length_eq_one_iff, ← hn', (Fin.mk.inj_iff.mp h).symm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn ∈ l
H :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + 1) % l.length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn
hn' : n.succ = l.length
h : ⟨0, ⋯⟩ = (⟨n, hn⟩ : Fin l.length)
a : l.length = 1
⊢ ∃ (x : α), l = [x]
have a₁ : n.succ = 1
Tactic: rw [← length_eq_one_iff, ← hn', (Fin.mk.inj_iff.mp h).symm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn ∈ l
H :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + 1) % l.length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn
hn' : n.succ = l.length
h : ⟨0, ⋯⟩ = (⟨n, hn⟩ : Fin l.length)
a : l.length = 1
a₁ : n.succ = 1
⊢ ∃ (x : α), l = [x]
have a₂ : Nat.succ 0 = 1
Tactic: rw [← length_eq_one_iff, ← hn', (Fin.mk.inj_iff.mp h).symm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
⊢ l.formPerm.support = l.toFinset
have rw : (↑l.formPerm.support : Set α) = (↑l.toFinset : Set α)
Tactic: rw [← Finset.coe_inj]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
⊢ (↑l.formPerm.support : Set α) = (↑l.toFinset : Set α)
have h₁ : (↑l.formPerm.support : Set α) = {x : α | (l.formPerm : (a : α) → α) x ≠ x}
Tactic: convert! support_formPerm_of_nodup' _ h h'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
⊢ (l.rotate 1).formPerm = l.formPerm
have h' : (l.rotate 1).Nodup
Tactic: have h' : Nodup (l.rotate 1) := by simpa using h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
⊢ (l.rotate 1).formPerm = l.formPerm
have H : ∀ (x : α), Eq (α := α) (((l.rotate 1).formPerm : (a : α) → α) x : α) ((l.formPerm : (a : α) → α) x : α)
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
⊢ Eq (α := α) (((l.rotate 1).formPerm : (a : α) → α) x : α) ((l.formPerm : (a : α) → α) x : α)
have pos : ∀ (hx : x ∈ l.rotate 1), Eq (α := α) (((l.rotate 1).formPerm : (a : α) → α) x : α) ((l.formPerm : (a : α) → α) x : α)
Tactic: by_cases hx : x ∈ l.rotate 1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
pos :
  ∀ (hx : x ∈ l.rotate 1), Eq (α := α) (((l.rotate 1).formPerm : (a : α) → α) x : α) ((l.formPerm : (a : α) → α) x : α)
⊢ Eq (α := α) (((l.rotate 1).formPerm : (a : α) → α) x : α) ((l.formPerm : (a : α) → α) x : α)
have neg : ∀ (hx : x ∉ l.rotate 1), Eq (α := α) (((l.rotate 1).formPerm : (a : α) → α) x : α) ((l.formPerm : (a : α) → α) x : α)
Tactic: by_cases hx : x ∈ l.rotate 1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
hx : x ∈ l.rotate 1
⊢ Eq (α := α) (((l.rotate 1).formPerm : (a : α) → α) x : α) ((l.formPerm : (a : α) → α) x : α)
have pos : ∀ (k : ℕ) (hk : k < (l.rotate 1).length)
  (hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) k hk ∈ l.rotate 1),
  Eq (α := α)
    (((l.rotate 1).formPerm : (a : α) → α)
        (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) k hk) :
      α)
    ((l.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) k hk) : α)
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 α
h : l.Nodup
h' : (l.rotate 1).Nodup
k : ℕ
hk : k < (l.rotate 1).length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) k hk ∈ l.rotate 1
⊢ Eq (α := α)
    (((l.rotate 1).formPerm : (a : α) → α)
        (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) k hk) :
      α)
    ((l.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) k hk) : α)
have pos : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (((k + 1) % (l.rotate 1).length + 1) % l.length) sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (((k + 1) % l.length + 1) % l.length) sorry
Tactic: rw [formPerm_apply_getElem _ h', getElem_rotate l, getElem_rotate l, formPerm_apply_getElem _ h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
hx : x ∉ l.rotate 1
⊢ Eq (α := α) (((l.rotate 1).formPerm : (a : α) → α) x : α) ((l.formPerm : (a : α) → α) x : α)
have neg : x ∉ l
Tactic: rw [formPerm_apply_of_notMem hx, formPerm_apply_of_notMem]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ (l.rotate (n + 1)).formPerm = l.formPerm
have succ : (l.rotate n).Nodup
Tactic: rw [← rotate_rotate, formPerm_rotate_one, hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ (l.rotate n).Nodup
have succ : l.rotate n ~r l
Tactic: rwa [IsRotated.nodup_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
⊢ (l.rotate n).formPerm = l.formPerm
have zero : (l.rotate 0).formPerm = l.formPerm
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    rw [← rotate_rotate, formPerm_rotate_one, hn]
    rwa [IsRotated.nodup_iff]
    exact IsRotated.forall l n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
zero : (l.rotate 0).formPerm = l.formPerm
⊢ (l.rotate n).formPerm = l.formPerm
have succ : ∀ (n : ℕ) (hn : (l.rotate n).formPerm = l.formPerm), (l.rotate (n + 1)).formPerm = l.formPerm
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    rw [← rotate_rotate, formPerm_rotate_one, hn]
    rwa [IsRotated.nodup_iff]
    exact IsRotated.forall l n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hd : l.Nodup
h : l ~r l'
⊢ l.formPerm = l'.formPerm
have obtain : ∀ (n : ℕ), l.formPerm = (l.rotate n).formPerm
Tactic: obtain ⟨n, rfl⟩ := h
Cleared hypotheses: l', h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
w : l.Nodup
n i : ℕ
h : i < l.length
⊢ (l.formPerm ^ n : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((i + n) % l.length) ⋯
have zero : (HPow.hPow (β := ℕ) l.formPerm 0 : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h) =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((i + 0) % l.length) sorry
Tactic: induction n with
  | zero => simp [Nat.mod_eq_of_lt h]
  | succ n hn =>
    simp [pow_succ', mul_apply, hn, formPerm_apply_getElem _ w,
      ← Nat.add_assoc]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
w : l.Nodup
n i : ℕ
h : i < l.length
zero :
  (HPow.hPow (β := ℕ) l.formPerm 0 : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((i + 0) % l.length) ⋯
⊢ (l.formPerm ^ n : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((i + n) % l.length) ⋯
have succ : ∀ (n : ℕ)
  (hn :
    (l.formPerm ^ n : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((i + n) % l.length) sorry),
  (l.formPerm ^ (n + 1) : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((i + (n + 1)) % l.length) sorry
Tactic: induction n with
  | zero => simp [Nat.mod_eq_of_lt h]
  | succ n hn =>
    simp [pow_succ', mul_apply, hn, formPerm_apply_getElem _ w,
      ← Nat.add_assoc]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : α
l : List α
h : (x :: l).Nodup
n : ℕ
⊢ ((x :: l).formPerm ^ n : (a : α) → α) x =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: l) (n % (x :: l).length) ⋯
have h₁ : n = 0 + n
Tactic: convert! formPerm_pow_apply_getElem _ h n 0 (Nat.succ_pos _)
-- 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
⊢ (x :: y :: l).formPerm = (x' :: y' :: l').formPerm ↔ x :: y :: l ~r x' :: y' :: l'
have refine : ∀ (h : (x :: y :: l).formPerm = (x' :: y' :: l').formPerm), x :: y :: l ~r x' :: y' :: l'
Tactic: refine ⟨fun h => ?_, fun hr => formPerm_eq_of_isRotated hd hr⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
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 :: y :: l).formPerm = (x' :: y' :: l').formPerm
⊢ x :: y :: l ~r x' :: y' :: l'
have h₁ : ∀ (x_1 : α),
  Eq (α := α) (((x :: y :: l).formPerm : (a : α) → α) x_1 : α) (((x' :: y' :: l').formPerm : (a : α) → α) x_1 : α)
Tactic: rw [Equiv.Perm.ext_iff] at h
Cleared hypotheses: h
-- 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 : α)
⊢ Membership.mem (γ := Set α) {z : α | ((x :: y :: l).formPerm : (a : α) → α) z ≠ z} x'
have rw : y' ≠ x'
Tactic: rw [Set.mem_setOf_eq, h x', formPerm_apply_head _ _ _ hd']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
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 : α)
⊢ y' ≠ x'
have hd'₁ : ¬(x' = y' ∨ x' ∈ l') ∧ y' ∉ l' ∧ l'.Nodup
Tactic: simp only [mem_cons, nodup_cons] at hd'
Cleared hypotheses: hd'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
h :
  ∀ (x_1 : α),
    Eq (α := α) (((x :: y :: l).formPerm : (a : α) → α) x_1 : α) (((x' :: y' :: l').formPerm : (a : α) → α) x_1 : α)
hd' : ¬(x' = y' ∨ x' ∈ l') ∧ y' ∉ l' ∧ l'.Nodup
⊢ y' ≠ x'
have hd'₁ : (x' ≠ y' ∧ x' ∉ l') ∧ y' ∉ l' ∧ l'.Nodup
Tactic: push Not at hd'
Cleared hypotheses: hd'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
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 : α)
⊢ x' ∈ x :: y :: l
have this : Membership.mem (γ := Set α) {z : α | ((x :: y :: l).formPerm : (a : α) → α) z ≠ z} x'
Tactic: have : x' ∈ { z | formPerm (x :: y :: l) z ≠ z } := by
      rw [Set.mem_setOf_eq, h x', formPerm_apply_head _ _ _ hd']
      simp only [mem_cons, nodup_cons] at hd'
      push Not at hd'
      exact hd'.left.left.symm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
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 : α)
⊢ x :: y :: l ~r x' :: y' :: l'
have hx : x' ∈ x :: y :: l
Tactic: have hx : x' ∈ x :: y :: l := by
    have : x' ∈ { z | formPerm (x :: y :: l) z ≠ z } := by
      rw [Set.mem_setOf_eq, h x', formPerm_apply_head _ _ _ hd']
      simp only [mem_cons, nodup_cons] at hd'
      push Not at hd'
      exact hd'.left.left.symm
    simpa using support_formPerm_le' _ this
-- 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
⊢ x :: y :: l ~r x' :: y' :: l'
have obtain : ∀ (n : ℕ) (hn : n < (x :: y :: l).length) (hx' : (x :: y :: l).get (⟨n, hn⟩ : Fin (x :: y :: l).length) = x'),
  x :: y :: l ~r x' :: y' :: l'
Tactic: obtain ⟨⟨n, hn⟩, hx'⟩ := get_of_mem hx
-- 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'
⊢ (x :: y :: l).length = (x' :: y' :: l').length
have rw : (x :: y :: l).toFinset.card = (x' :: y' :: l').toFinset.card
Tactic: rw [← dedup_eq_self.mpr hd, ← dedup_eq_self.mpr hd', ← card_toFinset, ← card_toFinset]
-- 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'
⊢ (x :: y :: l).toFinset.card = (x' :: y' :: l').toFinset.card
have refine : (x :: y :: l).toFinset = (x' :: y' :: l').toFinset
Tactic: refine congr_arg Finset.card ?_
-- 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'
⊢ (x :: y :: l).toFinset = (x' :: y' :: l').toFinset
have rw : Eq.{u_1 + 1} (α := Set α) {x_1 : α | ((x :: y :: l).formPerm : (a : α) → α) x_1 ≠ x_1}
  {x : α | ((x' :: y' :: l').formPerm : (a : α) → α) x ≠ x}
Tactic: rw [← Finset.coe_inj, ← support_formPerm_of_nodup' _ hd (by simp), ←
      support_formPerm_of_nodup' _ hd' (by simp)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
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'
⊢ x :: y :: l ~r x' :: y' :: l'
have hl : (x :: y :: l).length = (x' :: y' :: l').length
Tactic: have hl : (x :: y :: l).length = (x' :: y' :: l').length := by
    rw [← dedup_eq_self.mpr hd, ← dedup_eq_self.mpr hd', ← card_toFinset, ← card_toFinset]
    refine congr_arg Finset.card ?_
    rw [← Finset.coe_inj, ← support_formPerm_of_nodup' _ hd (by simp), ←
      support_formPerm_of_nodup' _ hd' (by simp)]
    simp only [h]