awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
refine : (x :: y :: l).toFinset = (x' :: y' :: l').toFinset
⊢ (x :: y :: l).toFinset.card = (x' :: y' :: l').toFinset.card

Tactic:
refine congr_arg Finset.card ?_

Premises used: congr_arg, Finset.card
-- 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_1 : α), x :: y :: l ≠ [x_1]

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
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 : α), x' :: y' :: l' ≠ [x]

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
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 :
  Eq.{u_1 + 1} (α := Set α) {x_1 : α | ((x :: y :: l).formPerm : (a : α) → α) x_1 ≠ x_1}
    {x : α | ((x' :: y' :: l').formPerm : (a : α) → α) x ≠ x}
⊢ (x :: y :: l).toFinset = (x' :: y' :: l').toFinset

Tactic:
rw [← Finset.coe_inj, ← support_formPerm_of_nodup' _ hd (by simp), ←
      support_formPerm_of_nodup' _ hd' (by simp)]

Premises used: Finset.coe_inj, List.support_formPerm_of_nodup'
-- 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'
⊢ 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:
simp only [h]
-- 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).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]
-- 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'
hl : (x :: y :: l).length = (x' :: y' :: l').length
h₁ : (x :: y :: l).rotate n = x' :: y' :: l'
⊢ x :: y :: l ~r x' :: y' :: l'

Tactic:
use n
-- 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'
hl : (x :: y :: l).length = (x' :: y' :: l').length
h₁ : ((x :: y :: l).rotate n).length = (x' :: y' :: l').length
h₂ :
  ∀ (i : ℕ) (h₁ : i < ((x :: y :: l).rotate n).length) (h₂ : i < (x' :: y' :: l').length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ((x :: y :: l).rotate n) i h₁ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') i h₂
⊢ (x :: y :: l).rotate n = x' :: y' :: l'

Tactic:
apply List.ext_getElem

Premises used: List.ext_getElem
-- 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'
hl h₁ : (x :: y :: l).length = (x' :: y' :: l').length
h₂ h₃ : (x' :: y' :: l').length = (x' :: y' :: l').length
⊢ ((x :: y :: l).rotate n).length = (x' :: y' :: l').length

Tactic:
rw [length_rotate, hl]

Premises used: List.length_rotate
-- 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'
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₁ :
  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'
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ((x :: y :: l).rotate n) k hk =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') k hk'

Tactic:
rw [getElem_rotate]

Premises used: List.getElem_rotate
-- 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'
hl : (x :: y :: l).length = (x' :: y' :: l').length
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'

Tactic:
Eq.trans ?_ hx'

Premises used: Eq.trans
-- 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'
hl : (x :: y :: l).length = (x' :: y' :: l').length
hk : 0 < ((x :: y :: l).rotate n).length
hk' : 0 < (x' :: y' :: l').length
h₁ :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) ((0 + n) % (x :: y :: l).length) ⋯ =
    (x :: y :: l).get (⟨n, hn⟩ : Fin (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'

Tactic:
refine Eq.trans ?_ hx'

Premises used: Eq.trans
-- 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'
hl : (x :: y :: l).length = (x' :: y' :: l').length
hk : 0 < ((x :: y :: l).rotate n).length
hk' : 0 < (x' :: y' :: l').length
h₁ : (0 + n) % (x :: y :: l).length = n
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) ((0 + n) % (x :: y :: l).length) ⋯ =
    (x :: y :: l).get (⟨n, hn⟩ : Fin (x :: y :: l).length)

Tactic:
congr
-- 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'
hl : (x :: y :: l).length = (x' :: y' :: l').length
hk : 0 < ((x :: y :: l).rotate n).length
hk' : 0 < (x' :: y' :: l').length
⊢ (0 + n) % (x :: y :: l).length = n

Tactic:
simpa using hn
-- 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'
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
a : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) ((k + 1 + n) % (x :: y :: l).length) ⋯
a₁ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') (k + 1) hk'
| 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'

Tactic:
congr
-- 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'
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
a : (k + 1 + n) % (x :: y :: l).length
| getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) ((k + 1 + n) % (x :: y :: l).length) ⋯

Tactic:
arg 2
-- 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'
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
a : ((k + 1) % (x' :: y' :: l').length + n) % (x :: y :: l).length
| (k + 1 + n) % (x :: y :: l).length

Tactic:
rw [← Nat.mod_eq_of_lt hk']

Premises used: Nat.mod_eq_of_lt
-- 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'
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
a : ((k + 1) % (x' :: y' :: l').length + n) % (x :: y :: l).length
| (k + 1 + n) % (x :: y :: l).length

Tactic:
(rw [← Nat.mod_eq_of_lt hk'])

Premises used: Nat.mod_eq_of_lt
-- 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'
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
a : ((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 + n) % (x :: y :: l).length) ⋯

Tactic:
arg 2; (rw [← Nat.mod_eq_of_lt hk'])

Premises used: Nat.mod_eq_of_lt
-- 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'
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
a a₁ : (k + 1 + n) % (x :: y :: l).length
a₂ : ((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 + n) % (x :: y :: l).length) ⋯

Tactic:
· arg 2; (rw [← Nat.mod_eq_of_lt hk'])

Premises used: Nat.mod_eq_of_lt
-- 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'
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
a : k + 1
| getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') (k + 1) hk'

Tactic:
arg 2
-- 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'
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
a : (k + 1) % (x' :: y' :: l').length
| k + 1

Tactic:
rw [← Nat.mod_eq_of_lt hk']

Premises used: Nat.mod_eq_of_lt
-- 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'
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
a : (k + 1) % (x' :: y' :: l').length
| k + 1

Tactic:
(rw [← Nat.mod_eq_of_lt hk'])

Premises used: Nat.mod_eq_of_lt
-- 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'
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
a : (k + 1) % (x' :: y' :: l').length
| getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') (k + 1) hk'

Tactic:
arg 2; (rw [← Nat.mod_eq_of_lt hk'])

Premises used: Nat.mod_eq_of_lt
-- 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'
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
a a₁ : k + 1
a₂ : (k + 1) % (x' :: y' :: l').length
| getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') (k + 1) hk'

Tactic:
· arg 2; (rw [← Nat.mod_eq_of_lt hk'])

Premises used: Nat.mod_eq_of_lt
-- 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'
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
a : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) ((k + 1 + n) % (x :: y :: l).length) ⋯
a₁ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') (k + 1) hk'
a₂ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) ((k + 1 + n) % (x :: y :: l).length) ⋯
a₃ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') (k + 1) hk'
a₄ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) ((k + 1 + n) % (x :: y :: l).length) ⋯
a₅ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') (k + 1) hk'
a₆ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) ((k + 1 + n) % (x :: y :: l).length) ⋯
a₇ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') (k + 1) hk'
| 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'

Tactic:
congr <;> · arg 2; (rw [← Nat.mod_eq_of_lt hk'])

Premises used: Nat.mod_eq_of_lt