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
⊢ x :: y :: l ~r x' :: y' :: l'
have h₁ : (x :: y :: l).rotate n = x' :: y' :: l'
Tactic: use n
-- 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
⊢ (x :: y :: l).rotate n = x' :: y' :: l'
have h₁ : ((x :: y :: l).rotate n).length = (x' :: y' :: l').length
Tactic: apply List.ext_getElem
-- 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
h₁ : ((x :: y :: l).rotate n).length = (x' :: y' :: l').length
⊢ (x :: y :: l).rotate n = x' :: y' :: l'
have 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₂
Tactic: apply List.ext_getElem
-- 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 h₁ : (x :: y :: l).length = (x' :: y' :: l').length
⊢ ((x :: y :: l).rotate n).length = (x' :: y' :: l').length
have h₂ : (x' :: y' :: l').length = (x' :: y' :: l').length
Tactic: rw [length_rotate, hl]
-- 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).rotate n) k hk =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') k hk'
have h₁ : 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'
Tactic: rw [getElem_rotate]
-- 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
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'
have h₁ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) ((0 + n) % (x :: y :: l).length) sorry =
  (x :: y :: l).get (⟨n, hn⟩ : Fin (x :: y :: l).length)
Tactic: refine Eq.trans ?_ 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'
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) ⋯ =
    (x :: y :: l).get (⟨n, hn⟩ : Fin (x :: y :: l).length)
have h₁ : (0 + n) % (x :: y :: l).length = n
Tactic: congr
-- 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 a : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) ((k + 1 + n) % (x :: y :: l).length) sorry
Tactic: congr
-- 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
a : 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 + n) % (x :: y :: l).length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') (k + 1) hk'
have a₁ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') (k + 1) hk'
Tactic: congr
-- 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) ⋯
have a : (k + 1 + n) % (x :: y :: l).length
Tactic: arg 2
-- 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 + n) % (x :: y :: l).length
have a : ((k + 1) % (x' :: y' :: l').length + n) % (x :: y :: l).length
Tactic: 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
| (k + 1 + n) % (x :: y :: l).length
have a : ((k + 1) % (x' :: y' :: l').length + n) % (x :: y :: l).length
Tactic: (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 + n) % (x :: y :: l).length) ⋯
have a : ((k + 1) % (x' :: y' :: l').length + n) % (x :: y :: l).length
Tactic: 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 + n) % (x :: y :: l).length) ⋯
have a : (k + 1 + n) % (x :: y :: l).length
Tactic: · 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
a 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) ⋯
have a₂ : ((k + 1) % (x' :: y' :: l').length + n) % (x :: y :: l).length
Tactic: · 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) hk'
have a : k + 1
Tactic: arg 2
-- 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
have a : (k + 1) % (x' :: y' :: l').length
Tactic: 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
| k + 1
have a : (k + 1) % (x' :: y' :: l').length
Tactic: (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) hk'
have a : (k + 1) % (x' :: y' :: l').length
Tactic: 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) hk'
have a : k + 1
Tactic: · 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
a a₁ : k + 1
| getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') (k + 1) hk'
have a₂ : (k + 1) % (x' :: y' :: l').length
Tactic: · 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 + n) % (x :: y :: l).length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') (k + 1) hk'
have a : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) ((k + 1 + n) % (x :: y :: l).length) sorry
Tactic: 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
a : 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 + n) % (x :: y :: l).length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x' :: y' :: l') (k + 1) hk'
have a₁ : 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'])