awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.PeriodicityLemma
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
rw₁ : u.length ≤ j + u.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

Tactic:
rw [getElem?_append_right, Nat.add_sub_cancel, getElem?_append_left]

Premises used: List.getElem?_append_right, List.getElem?_append_left, Nat.add_sub_cancel
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ j < v.length

Tactic:
lia
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ u.length ≤ j + u.length

Tactic:
lia
-- Module: Mathlib.Data.List.PeriodicityLemma
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

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
-- Module: Mathlib.Data.List.PeriodicityLemma
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
⊢ j + u.length + p - u.length = j + p

Tactic:
lia
-- Module: Mathlib.Data.List.PeriodicityLemma
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
⊢ j + u.length + p - u.length = j + p

Tactic:
have eq : j + u.length + p - u.length = j + p := by lia
-- Module: Mathlib.Data.List.PeriodicityLemma
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)
rw₁ : u.length ≤ j + u.length + 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)

Tactic:
rw [getElem?_append_right]

Premises used: List.getElem?_append_right
-- Module: Mathlib.Data.List.PeriodicityLemma
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)
rw₁ : j + u.length + p - u.length < v.length
⊢ 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_left]

Premises used: List.getElem?_append_left
-- Module: Mathlib.Data.List.PeriodicityLemma
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 (j + u.length + p - u.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v (j + p)

Tactic:
congrArg (getElem? v) eq

Premises used: congrArg, GetElem?.getElem?
-- Module: Mathlib.Data.List.PeriodicityLemma
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 (j + u.length + p - u.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v (j + p)

Tactic:
exact congrArg (getElem? v) eq

Premises used: congrArg, GetElem?.getElem?
-- Module: Mathlib.Data.List.PeriodicityLemma
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
⊢ j + u.length + p - u.length < v.length

Tactic:
lia
-- Module: Mathlib.Data.List.PeriodicityLemma
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
⊢ u.length ≤ j + u.length + p

Tactic:
lia
-- Module: Mathlib.Data.List.PeriodicityLemma
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)

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
-- Module: Mathlib.Data.List.PeriodicityLemma
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)
⊢ ∀ 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:
simp_all [hasPeriod_iff_getElem?]

Premises used: List.hasPeriod_iff_getElem?
-- Module: Mathlib.Data.List.PeriodicityLemma
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)
⊢ ∀ 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?]
-- Module: Mathlib.Data.List.PeriodicityLemma
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)
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)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v j =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v (j + p)

Tactic:
rw [← shift_position', ← shift_position]
-- Module: Mathlib.Data.List.PeriodicityLemma
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)
⊢ j + u.length < u.length + (v.length + w.length) - p

Tactic:
lia
-- Module: Mathlib.Data.List.PeriodicityLemma
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) (u ++ (v ++ w)) (j + u.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (u ++ (v ++ w)) (j + u.length + p)

Tactic:
exact this (j + u.length) (by lia)

Premises used: HAdd.hAdd, List.length
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
u w : List α
p : ℕ
per : w.HasPeriod p
h : u <:+: w
obtain : ∀ (s t : List α) (per : (s ++ u ++ t).HasPeriod p), u.HasPeriod p
⊢ u.HasPeriod p

Tactic:
obtain ⟨s, t, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
u : List α
p : ℕ
s t : List α
per : (s ++ u ++ t).HasPeriod p
⊢ u.HasPeriod p

Tactic:
per.factor

Premises used: List.HasPeriod.factor
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
u : List α
p : ℕ
s t : List α
per : (s ++ u ++ t).HasPeriod p
⊢ u.HasPeriod p

Tactic:
exact per.factor

Premises used: List.HasPeriod.factor
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
w : List α
p : ℕ
per : w.HasPeriod p
rw : take p w ++ drop p w <+: take p w ++ w
⊢ drop p w <+: w

Tactic:
rw [← prefix_append_right_inj (take p w)]

Premises used: List.prefix_append_right_inj, List.take
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
w : List α
p : ℕ
per : w.HasPeriod p
⊢ take p w ++ drop p w <+: take p w ++ w

Tactic:
simp_all [HasPeriod, take_append_drop]

Premises used: List.HasPeriod, List.take_append_drop
-- Module: Mathlib.Data.List.PeriodicityLemma
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
inr : ∀ (p_pos : p > 0), (take n w ++ w).HasPeriod p
⊢ (take n w ++ w).HasPeriod p

Tactic:
rcases Nat.eq_zero_or_pos p with rfl | p_pos

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
n : ℕ
w : List α
len : n ≤ w.length
dvd : 0 ∣ n
per : w.HasPeriod 0
⊢ (take n w ++ w).HasPeriod 0

Tactic:
simp_all [HasPeriod]

Premises used: List.HasPeriod
-- Module: Mathlib.Data.List.PeriodicityLemma
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
inr₁ : ∀ (pos : n > 0), (take n w ++ w).HasPeriod p
⊢ (take n w ++ w).HasPeriod p

Tactic:
rcases Nat.eq_zero_or_pos n with rfl | pos

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p : ℕ
w : List α
per : w.HasPeriod p
p_pos : p > 0
dvd : p ∣ 0
len : 0 ≤ w.length
⊢ (take 0 w ++ w).HasPeriod p

Tactic:
simp_all
-- Module: Mathlib.Data.List.PeriodicityLemma
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
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)
⊢ (take n w ++ w).HasPeriod p

Tactic:
rw [hasPeriod_iff_forall_getElem?_mod]

Premises used: List.hasPeriod_iff_forall_getElem?_mod
-- Module: Mathlib.Data.List.PeriodicityLemma
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 < 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)
-- Module: Mathlib.Data.List.PeriodicityLemma
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
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
this :
  ∀ i < n + 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)
⊢ ∀ 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:
simp_all
-- Module: Mathlib.Data.List.PeriodicityLemma
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
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
inr :
  ∀ i < n + 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)
⊢ ∀ 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:
suffices ∀ i < n + w.length, (take n w ++ w)[i]? = (take n w ++ w)[i % p]? by simp_all
-- Module: Mathlib.Data.List.PeriodicityLemma
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
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
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
pos₁ :
  ∀ (j_lt_n : j < n),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n w ++ w) j =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (j % p)
neg :
  ∀ (j_lt_n : ¬j < n),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n w ++ w) j =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (j % p)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n w ++ w) j =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (j % p)

Tactic:
by_cases j_lt_n : j < n
-- Module: Mathlib.Data.List.PeriodicityLemma
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
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
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_lt_n : j < n
⊢ j < (take n w).length

Tactic:
simp_all
-- Module: Mathlib.Data.List.PeriodicityLemma
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
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
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_lt_n : j < n
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n w) j =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w j

Tactic:
getElem?_take_of_lt j_lt_n

Premises used: List.getElem?_take_of_lt
-- Module: Mathlib.Data.List.PeriodicityLemma
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
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
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_lt_n : j < n
⊢ j < w.length

Tactic:
lia
-- Module: Mathlib.Data.List.PeriodicityLemma
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
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
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_lt_n : j < n
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n w ++ w) j =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (j % p)

Tactic:
calc
        (take n w ++ w)[j]? = (take n w)[j]? := getElem?_append_left (by simp_all)
        _ = w[j]? := getElem?_take_of_lt j_lt_n
        _ = w[j % p]? := Eq.symm (mod_w j (by lia))

Premises used: List.getElem?_append_left, List.getElem?_take_of_lt, Eq.symm, List.take, HAppend.hAppend
-- Module: Mathlib.Data.List.PeriodicityLemma
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
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
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_lt_n : ¬j < n
⊢ j - n < w.length

Tactic:
lia
-- Module: Mathlib.Data.List.PeriodicityLemma
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
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
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_lt_n : ¬j < n
⊢ j - n < w.length

Tactic:
have j_minus : j - n < w.length := by lia
-- Module: Mathlib.Data.List.PeriodicityLemma
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
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
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_lt_n : ¬j < n
j_minus : j - n < w.length
⊢ n ≤ j

Tactic:
have n_le_j : n ≤ j := le_of_not_gt j_lt_n
-- Module: Mathlib.Data.List.PeriodicityLemma
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
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
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_minus : j - n < w.length
n_le_j : n ≤ j
rw rw₁ : (j - n) % p = (j - n) % p
⊢ (j - n) % p = (j - p * (n / p)) % p

Tactic:
rw [Nat.mul_div_cancel' dvd]

Premises used: Nat.mul_div_cancel'
-- Module: Mathlib.Data.List.PeriodicityLemma
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
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
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_minus : j - n < w.length
n_le_j : n ≤ j
⊢ (j - p * (n / p)) % p = j % p

Tactic:
sub_mul_mod ((Nat.mul_div_cancel' dvd).symm ▸ n_le_j)

Premises used: Nat.sub_mul_mod, Eq.rec, Eq.symm, Nat.mul_div_cancel'
-- Module: Mathlib.Data.List.PeriodicityLemma
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
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
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_minus : j - n < w.length
n_le_j : n ≤ j
p₁ : (j - n) % p = (j - p * (n / p)) % p
⊢ (j - n) % p = j % p

Tactic:
calc
          (j - n) % p = (j - p * (n / p)) % p := by rw [Nat.mul_div_cancel' dvd]
          _ = j % p := sub_mul_mod ((Nat.mul_div_cancel' dvd).symm ▸ n_le_j)

Premises used: Nat.sub_mul_mod, HMul.hMul, HSub.hSub, HDiv.hDiv
-- Module: Mathlib.Data.List.PeriodicityLemma
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
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
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_minus : j - n < w.length
n_le_j : n ≤ j
⊢ (j - n) % p = j % p

Tactic:
have j_mod : (j - n) % p = j % p := by
        calc
          (j - n) % p = (j - p * (n / p)) % p := by rw [Nat.mul_div_cancel' dvd]
          _ = j % p := sub_mul_mod ((Nat.mul_div_cancel' dvd).symm ▸ n_le_j)
-- Module: Mathlib.Data.List.PeriodicityLemma
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
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
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_minus : j - n < w.length
n_le_j : n ≤ j
j_mod : (j - n) % p = j % p
⊢ (take n w).length ≤ j

Tactic:
simp_all