awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : p = 0
pos :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % 0) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
have pos₁ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
Tactic: rw [p_zero, mod_zero]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : ¬p = 0
small : i < p
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
have eq : i % p = i
Tactic: have eq : i % p = i := mod_eq_of_lt small
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : ¬p = 0
small : i < p
eq : i % p = i
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
have neg : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
have len' : i - p < w.length
Tactic: have len' : i - p < w.length := by lia
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
len' : i - p < w.length
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
have IH : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w ((i - p) % p) =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i - p)
Tactic: have IH : w[(i - p) % p]? = w[i - p]? := per.getElem?_mod p (i - p) w len'
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
len' : i - p < w.length
IH :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w ((i - p) % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i - p)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
have per₁ : ∀ i < w.length - p,
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i + p)
Tactic: rw [hasPeriod_iff_getElem?] at per
Cleared hypotheses: per, less, p_zero, large, len', IH
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
p i : ℕ
w : List α
per :
  ∀ i < w.length - p,
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i + p)
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
len' : i - p < w.length
IH :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w ((i - p) % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i - p)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
have minus : i - p < w.length - p
Tactic: have minus : i - p < w.length - p := by lia
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
p i : ℕ
w : List α
per :
  ∀ i < w.length - p,
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i + p)
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
len' : i - p < w.length
IH :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w ((i - p) % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i - p)
minus : i - p < w.length - p
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
have per' : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i - p) =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i - p + p)
Tactic: have per' := per (i - p) minus
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
p i : ℕ
w : List α
per :
  ∀ i < w.length - p,
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i + p)
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
len' : i - p < w.length
IH :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w ((i - p) % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i - p)
minus : i - p < w.length - p
per' :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i - p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i - p + p)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
have per'₁ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i - p) =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
Tactic: simp only [large, Nat.sub_add_cancel] at per'
Cleared hypotheses: per'
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
p i : ℕ
w : List α
per :
  ∀ i < w.length - p,
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i + p)
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
len' : i - p < w.length
IH :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w ((i - p) % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i - p)
minus : i - p < w.length - p
per' :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i - p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
have mod : i % p = (i - p) % p
Tactic: have mod : i % p = (i - p) % p := mod_eq_sub_mod large
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : ¬p = 0
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
have x : i < p ∨ p ≤ i
Tactic: cases lt_or_ge i p with
    | inl small =>
        have eq : i % p = i := mod_eq_of_lt small
        rw [eq]
    | inr large =>
        have len' : i - p < w.length := by lia
        have IH : w[(i - p) % p]? = w[i - p]? := per.getElem?_mod p (i - p) w len'
        rw [hasPeriod_iff_getElem?] at per
        have minus : i - p < w.length - p := by lia
        have per' := per (i - p) minus
        simp only [large, Nat.sub_add_cancel] at per'
        have mod : i % p = (i - p) % p := mod_eq_sub_mod large
        aesop
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
p : ℕ
w : List α
⊢ w.HasPeriod p ↔
    ∀ i < w.length,
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
        getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p)
have mp : w.HasPeriod p →
  ∀ i < w.length,
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
p : ℕ
w : List α
mp :
  w.HasPeriod p →
    ∀ i < w.length,
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
        getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p)
⊢ w.HasPeriod p ↔
    ∀ i < w.length,
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
        getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p)
have mpr : (∀ i < w.length,
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p)) →
  w.HasPeriod p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
p : ℕ
w : List α
mod :
  ∀ i < w.length,
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p)
⊢ w.HasPeriod p
have mpr : ∀ i < w.length - p,
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i + p)
Tactic: rw [hasPeriod_iff_getElem?]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
p : ℕ
w : List α
mod :
  ∀ i < w.length,
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p)
i : ℕ
less : i < w.length - p
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i + p)
have mpr : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w ((i + p) % p)
Tactic: rw [mod (i + p) (by lia), add_mod_right, mod i (by lia)]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
p : ℕ
w : List α
mod :
  ∀ i < w.length,
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p)
i : ℕ
less : i < w.length - p
mpr :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w ((i + p) % p)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i + p)
have mpr₁ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p)
Tactic: rw [mod (i + p) (by lia), add_mod_right, mod i (by lia)]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
p : ℕ
w : List α
mod :
  ∀ i < w.length,
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p)
i : ℕ
less : i < w.length - p
mpr :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w ((i + p) % p)
mpr₁ :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i + p)
have mpr₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p)
Tactic: rw [mod (i + p) (by lia), add_mod_right, mod i (by lia)]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
⊢ v.HasPeriod p
have suffices : ∀ j < v.length - p,
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v j =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v (j + p)
Tactic: suffices ∀ j < v.length - p, v[j]? = v[j + p]? by simpa [hasPeriod_iff_getElem?]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) (j + u.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v j
have rw : j < v.length
Tactic: rw [getElem?_append_right, Nat.add_sub_cancel, getElem?_append_left]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
rw : j < v.length
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) (j + u.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v j
have rw₁ : u.length ≤ j + u.length
Tactic: rw [getElem?_append_right, Nat.add_sub_cancel, getElem?_append_left]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v j =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v (j + p)
have shift_position : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) (j + u.length) =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v j
Tactic: have shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]? := by
    rw [getElem?_append_right, Nat.add_sub_cancel, getElem?_append_left]
    all_goals lia
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) (j + u.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v j
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) (j + u.length + p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v (j + p)
have eq : j + u.length + p - u.length = j + p
Tactic: have eq : j + u.length + p - u.length = j + p := by lia
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) (j + u.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v j
eq : j + u.length + p - u.length = j + p
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) (j + u.length + p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v (j + p)
have rw : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (v ++ w) (j + u.length + p - u.length) =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v (j + p)
Tactic: rw [getElem?_append_right]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) (j + u.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v j
eq : j + u.length + p - u.length = j + p
rw :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (v ++ w) (j + u.length + p - u.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v (j + p)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) (j + u.length + p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v (j + p)
have rw₁ : u.length ≤ j + u.length + p
Tactic: rw [getElem?_append_right]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) (j + u.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v j
eq : j + u.length + p - u.length = j + p
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (v ++ w) (j + u.length + p - u.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v (j + p)
have rw : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v (j + u.length + p - u.length) =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v (j + p)
Tactic: rw [getElem?_append_left]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) (j + u.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v j
eq : j + u.length + p - u.length = j + p
rw :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v (j + u.length + p - u.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v (j + p)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (v ++ w) (j + u.length + p - u.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v (j + p)
have rw₁ : j + u.length + p - u.length < v.length
Tactic: rw [getElem?_append_left]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) (j + u.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v j
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v j =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v (j + p)
have shift_position' : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) (j + u.length + p) =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v (j + p)
Tactic: have shift_position' : (u ++ (v ++ w))[j + u.length + p]? = v[j + p]? := by
    have eq : j + u.length + p - u.length = j + p := by lia
    rw [getElem?_append_right]
    · rw [getElem?_append_left]
      · exact congrArg (getElem? v) eq
      · lia
    · lia
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) (j + u.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v j
shift_position' :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) (j + u.length + p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v (j + p)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v j =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v (j + p)
have this : ∀ i < u.length + (v.length + w.length) - p,
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) i =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) (i + p)
Tactic: have : ∀ i < u.length + (v.length + w.length) - p,
      (u ++ (v ++ w))[i]? = (u ++ (v ++ w))[i + p]? := by
    simp_all [hasPeriod_iff_getElem?]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) (j + u.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v j
shift_position' :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) (j + u.length + p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v (j + p)
this :
  ∀ i < u.length + (v.length + w.length) - p,
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) (i + p)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v j =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v (j + p)
have rw : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) (j + u.length) =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) (j + u.length + p)
Tactic: rw [← shift_position', ← shift_position]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
u w : List α
p : ℕ
per : w.HasPeriod p
h : u <:+: w
⊢ u.HasPeriod p
have obtain : ∀ (s t : List α) (per : (s ++ u ++ t).HasPeriod p), u.HasPeriod p
Tactic: obtain ⟨s, t, rfl⟩ := h
Cleared hypotheses: w, per, h
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
w : List α
p : ℕ
per : w.HasPeriod p
⊢ drop p w <+: w
have rw : take p w ++ drop p w <+: take p w ++ w
Tactic: rw [← prefix_append_right_inj (take p w)]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
⊢ (take n w ++ w).HasPeriod p
have inl : ∀ (dvd : 0 ∣ n) (per : w.HasPeriod 0), (take n w ++ w).HasPeriod 0
Tactic: rcases Nat.eq_zero_or_pos p with rfl | p_pos
Cleared hypotheses: p, dvd, per
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
inl : ∀ (dvd : 0 ∣ n) (per : w.HasPeriod 0), (take n w ++ w).HasPeriod 0
⊢ (take n w ++ w).HasPeriod p
have inr : ∀ (p_pos : p > 0), (take n w ++ w).HasPeriod p
Tactic: rcases Nat.eq_zero_or_pos p with rfl | p_pos
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
⊢ (take n w ++ w).HasPeriod p
have inr : ∀ (dvd : p ∣ 0) (len : 0 ≤ w.length), (take 0 w ++ w).HasPeriod p
Tactic: rcases Nat.eq_zero_or_pos n with rfl | pos
Cleared hypotheses: n, dvd, len
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
inr : ∀ (dvd : p ∣ 0) (len : 0 ≤ w.length), (take 0 w ++ w).HasPeriod p
⊢ (take n w ++ w).HasPeriod p
have inr₁ : ∀ (pos : n > 0), (take n w ++ w).HasPeriod p
Tactic: rcases Nat.eq_zero_or_pos n with rfl | pos
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
⊢ (take n w ++ w).HasPeriod p
have inr : ∀ i < (take n w ++ w).length,
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n w ++ w) i =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n w ++ w) (i % p)
Tactic: rw [hasPeriod_iff_forall_getElem?_mod]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
⊢ ∀ i < (take n w ++ w).length,
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n w ++ w) i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n w ++ w) (i % p)
have mod_w : ∀ i < w.length,
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i
Tactic: have mod_w : ∀ i < w.length, w[i % p]? = w[i]? := (per.getElem?_mod)