awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.List
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
a :
  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
⊢ Membership.mem (γ := Set α) {x : α | (l.formPerm : (a : α) → α) x ≠ x}
    (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn)

Tactic:
rw [Set.mem_setOf_eq, formPerm_apply_getElem _ h]

Premises used: List.formPerm_apply_getElem, Set.mem_setOf_eq
-- Module: Mathlib.GroupTheory.Perm.List
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
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) ⋯ =
        getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn),
    False
⊢ False

Tactic:
rw [nodup_iff_injective_get, Function.Injective] at h

Premises used: List.nodup_iff_injective_get, Function.Injective
-- Module: Mathlib.GroupTheory.Perm.List
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
⊢ (⟨(n + 1) % l.length, ⋯⟩ : Fin l.length) = ⟨n, hn⟩

Tactic:
specialize h H
-- Module: Mathlib.GroupTheory.Perm.List
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
a₁ : ∀ (hn' : n.succ < l.length), False
⊢ False

Tactic:
rcases (Nat.succ_le_of_lt hn).eq_or_lt with hn' | hn'

Premises used: LE.le.eq_or_lt, Nat.succ_le_of_lt
-- Module: Mathlib.GroupTheory.Perm.List
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
⊢ ⟨0, ⋯⟩ = (⟨n, hn⟩ : Fin l.length)

Tactic:
simp only [← hn', Nat.mod_self] at h

Premises used: Nat.mod_self
-- Module: Mathlib.GroupTheory.Perm.List
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

Tactic:
not_exists.mpr h' ?_

Premises used: Iff.mpr, not_exists
-- Module: Mathlib.GroupTheory.Perm.List
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 : ∃ (x : α), l = [x]
⊢ False

Tactic:
refine not_exists.mpr h' ?_

Premises used: Iff.mpr, not_exists
-- Module: Mathlib.GroupTheory.Perm.List
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
a₂ a₃ : Nat.succ 0 = 1
⊢ ∃ (x : α), l = [x]

Tactic:
rw [← length_eq_one_iff, ← hn', (Fin.mk.inj_iff.mp h).symm]

Premises used: List.length_eq_one_iff, Iff.mp, Eq.symm, Fin.mk.inj_iff
-- Module: Mathlib.GroupTheory.Perm.List
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

Tactic:
simp [Nat.mod_eq_of_lt hn'] at h

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
rw : (↑l.formPerm.support : Set α) = (↑l.toFinset : Set α)
⊢ l.formPerm.support = l.toFinset

Tactic:
rw [← Finset.coe_inj]

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

Tactic:
support_formPerm_of_nodup' _ h h'

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

Tactic:
convert! support_formPerm_of_nodup' _ h h'

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

Tactic:
simp [Set.ext_iff]

Premises used: Set.ext_iff
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
⊢ (l.rotate 1).Nodup

Tactic:
simpa using h
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
⊢ (l.rotate 1).Nodup

Tactic:
have h' : Nodup (l.rotate 1) := by simpa using h
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
H : ∀ (x : α), Eq (α := α) (((l.rotate 1).formPerm : (a : α) → α) x : α) ((l.formPerm : (a : α) → α) x : α)
⊢ (l.rotate 1).formPerm = l.formPerm

Tactic:
ext x
-- Module: Mathlib.GroupTheory.Perm.List
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 : α)
neg :
  ∀ (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 : α)

Tactic:
by_cases hx : x ∈ l.rotate 1

Premises used: OfNat.ofNat, List.rotate
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
hx : x ∈ l.rotate 1
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) : α)
⊢ Eq (α := α) (((l.rotate 1).formPerm : (a : α) → α) x : α) ((l.formPerm : (a : α) → α) x : α)

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

Premises used: List.getElem_of_mem, rfl
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
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
pos :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (((k + 1) % (l.rotate 1).length + 1) % l.length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (((k + 1) % l.length + 1) % l.length) ⋯
⊢ 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:
rw [formPerm_apply_getElem _ h', getElem_rotate l, getElem_rotate l, formPerm_apply_getElem _ h]

Premises used: List.formPerm_apply_getElem, List.getElem_rotate
-- Module: Mathlib.GroupTheory.Perm.List
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
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (((k + 1) % (l.rotate 1).length + 1) % l.length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (((k + 1) % l.length + 1) % l.length) ⋯

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
hx : x ∉ l.rotate 1
neg : x ∉ l
⊢ Eq (α := α) (((l.rotate 1).formPerm : (a : α) → α) x : α) ((l.formPerm : (a : α) → α) x : α)

Tactic:
rw [formPerm_apply_of_notMem hx, formPerm_apply_of_notMem]

Premises used: List.formPerm_apply_of_notMem
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
hx : x ∉ l.rotate 1
⊢ x ∉ l

Tactic:
simpa using hx
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
⊢ (l.rotate 0).formPerm = l.formPerm

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
succ : (l.rotate n).Nodup
⊢ (l.rotate (n + 1)).formPerm = l.formPerm

Tactic:
rw [← rotate_rotate, formPerm_rotate_one, hn]

Premises used: List.rotate_rotate, List.formPerm_rotate_one
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
succ : l.rotate n ~r l
⊢ (l.rotate n).Nodup

Tactic:
rwa [IsRotated.nodup_iff]

Premises used: List.IsRotated.nodup_iff
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ l.rotate n ~r l

Tactic:
IsRotated.forall l n

Premises used: List.IsRotated.forall
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ l.rotate n ~r l

Tactic:
exact IsRotated.forall l n

Premises used: List.IsRotated.forall
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
zero : (l.rotate 0).formPerm = l.formPerm
succ : ∀ (n : ℕ) (hn : (l.rotate n).formPerm = l.formPerm), (l.rotate (n + 1)).formPerm = l.formPerm
⊢ (l.rotate n).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

Premises used: List.rotate_rotate, List.IsRotated.nodup_iff, List.IsRotated.forall, List.formPerm_rotate_one
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hd : l.Nodup
h : l ~r l'
obtain : ∀ (n : ℕ), l.formPerm = (l.rotate n).formPerm
⊢ l.formPerm = l'.formPerm

Tactic:
obtain ⟨n, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hd : l.Nodup
n : ℕ
⊢ l.formPerm = (l.rotate n).formPerm

Tactic:
(formPerm_rotate l hd n).symm

Premises used: List.formPerm_rotate, Eq.symm
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hd : l.Nodup
n : ℕ
⊢ l.formPerm = (l.rotate n).formPerm

Tactic:
exact (formPerm_rotate l hd n).symm

Premises used: List.formPerm_rotate, Eq.symm
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
l : List α
a b : α
⊢ (x :: y :: l ++ [a, b]).formPerm = (x :: y :: l ++ [a]).formPerm * swap a b

Tactic:
simpa [mul_assoc] using formPerm_append_pair (y::l) a b

Premises used: mul_assoc, List.cons
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
l : List α
⊢ (a :: b :: l).reverse.formPerm = (a :: b :: l).formPerm⁻¹

Tactic:
simp [formPerm_append_pair, swap_comm, ← formPerm_reverse (b::l)]

Premises used: Equiv.swap_comm, List.cons, List.formPerm_append_pair
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
w : l.Nodup
i : ℕ
h : i < l.length
⊢ (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) ⋯

Tactic:
simp [Nat.mod_eq_of_lt h]

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
w : l.Nodup
i : ℕ
h : i < l.length
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) ⋯
⊢ (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) ⋯

Tactic:
simp [pow_succ', mul_apply, hn, formPerm_apply_getElem _ w,
      ← Nat.add_assoc]

Premises used: List.formPerm_apply_getElem, Nat.add_assoc, Equiv.Perm.mul_apply, pow_succ'
-- Module: Mathlib.GroupTheory.Perm.List
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) ⋯
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) ⋯),
    (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) ⋯
⊢ (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) ⋯

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]

Premises used: List.formPerm_apply_getElem, Nat.mod_eq_of_lt, Nat.add_assoc, Equiv.Perm.mul_apply, pow_succ'
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x : α
l : List α
h : (x :: l).Nodup
n : ℕ
⊢ ((x :: l).formPerm ^ n : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: l) 0 ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: l) ((0 + n) % (x :: l).length) ⋯

Tactic:
formPerm_pow_apply_getElem _ h n 0 (Nat.succ_pos _)

Premises used: List.formPerm_pow_apply_getElem, Nat.succ_pos, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x : α
l : List α
h : (x :: l).Nodup
n : ℕ
h₁ : n = 0 + n
⊢ ((x :: l).formPerm ^ n : (a : α) → α) x =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: l) (n % (x :: l).length) ⋯

Tactic:
convert! formPerm_pow_apply_getElem _ h n 0 (Nat.succ_pos _)

Premises used: List.formPerm_pow_apply_getElem, Nat.succ_pos, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x : α
l : List α
h : (x :: l).Nodup
n : ℕ
⊢ n = 0 + n

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
⊢ (x :: y :: l).formPerm = (x' :: y' :: l').formPerm ↔ x :: y :: l ~r x' :: y' :: l'

Tactic:
⟨fun h => ?_, fun hr => formPerm_eq_of_isRotated hd hr⟩

Premises used: Iff.intro, List.formPerm_eq_of_isRotated
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
refine : ∀ (h : (x :: y :: l).formPerm = (x' :: y' :: l').formPerm), x :: y :: l ~r x' :: y' :: l'
⊢ (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⟩
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : (x :: y :: l).formPerm = (x' :: y' :: l').formPerm
⊢ ∀ (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

Premises used: Equiv.Perm.ext_iff
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h :
  ∀ (x_1 : α),
    Eq (α := α) (((x :: y :: l).formPerm : (a : α) → α) x_1 : α) (((x' :: y' :: l').formPerm : (a : α) → α) x_1 : α)
rw : y' ≠ x'
⊢ Membership.mem (γ := Set α) {z : α | ((x :: y :: l).formPerm : (a : α) → α) z ≠ z} x'

Tactic:
rw [Set.mem_setOf_eq, h x', formPerm_apply_head _ _ _ hd']

Premises used: Set.mem_setOf_eq, List.formPerm_apply_head
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h :
  ∀ (x_1 : α),
    Eq (α := α) (((x :: y :: l).formPerm : (a : α) → α) x_1 : α) (((x' :: y' :: l').formPerm : (a : α) → α) x_1 : α)
⊢ ¬(x' = y' ∨ x' ∈ l') ∧ y' ∉ l' ∧ l'.Nodup

Tactic:
simp only [mem_cons, nodup_cons] at hd'

Premises used: List.nodup_cons, List.mem_cons
-- Module: Mathlib.GroupTheory.Perm.List
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
⊢ (x' ≠ y' ∧ x' ∉ l') ∧ y' ∉ l' ∧ l'.Nodup

Tactic:
push Not at hd'

Premises used: Not
-- Module: Mathlib.GroupTheory.Perm.List
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'

Tactic:
hd'.left.left.symm

Premises used: Ne.symm, And.left
-- Module: Mathlib.GroupTheory.Perm.List
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'

Tactic:
exact hd'.left.left.symm

Premises used: Ne.symm, And.left
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h :
  ∀ (x_1 : α),
    Eq (α := α) (((x :: y :: l).formPerm : (a : α) → α) x_1 : α) (((x' :: y' :: l').formPerm : (a : α) → α) x_1 : α)
⊢ 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
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h :
  ∀ (x_1 : α),
    Eq (α := α) (((x :: y :: l).formPerm : (a : α) → α) x_1 : α) (((x' :: y' :: l').formPerm : (a : α) → α) x_1 : α)
this : Membership.mem (γ := Set α) {z : α | ((x :: y :: l).formPerm : (a : α) → α) z ≠ z} x'
⊢ x' ∈ x :: y :: l

Tactic:
simpa using support_formPerm_le' _ this

Premises used: List.support_formPerm_le'
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h :
  ∀ (x_1 : α),
    Eq (α := α) (((x :: y :: l).formPerm : (a : α) → α) x_1 : α) (((x' :: y' :: l').formPerm : (a : α) → α) x_1 : α)
⊢ 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
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h :
  ∀ (x_1 : α),
    Eq (α := α) (((x :: y :: l).formPerm : (a : α) → α) x_1 : α) (((x' :: y' :: l').formPerm : (a : α) → α) x_1 : α)
hx : x' ∈ x :: y :: l
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'
⊢ x :: y :: l ~r x' :: y' :: l'

Tactic:
obtain ⟨⟨n, hn⟩, hx'⟩ := get_of_mem hx

Premises used: List.get_of_mem
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h :
  ∀ (x_1 : α),
    Eq (α := α) (((x :: y :: l).formPerm : (a : α) → α) x_1 : α) (((x' :: y' :: l').formPerm : (a : α) → α) x_1 : α)
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get (⟨n, hn⟩ : Fin (x :: y :: l).length) = x'
rw : (x :: y :: l).toFinset.card = (x' :: y' :: l').toFinset.card
⊢ (x :: y :: l).length = (x' :: y' :: l').length

Tactic:
rw [← dedup_eq_self.mpr hd, ← dedup_eq_self.mpr hd', ← card_toFinset, ← card_toFinset]

Premises used: Iff.mpr, List.dedup_eq_self, List.card_toFinset
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h :
  ∀ (x_1 : α),
    Eq (α := α) (((x :: y :: l).formPerm : (a : α) → α) x_1 : α) (((x' :: y' :: l').formPerm : (a : α) → α) x_1 : α)
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get (⟨n, hn⟩ : Fin (x :: y :: l).length) = x'
⊢ (x :: y :: l).toFinset.card = (x' :: y' :: l').toFinset.card

Tactic:
congr_arg Finset.card ?_

Premises used: congr_arg, Finset.card