awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 < (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 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)
Tactic: suffices ∀ i < n + w.length, (take n w ++ w)[i]? = (take n w ++ w)[i % p]? by simp_all
-- 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
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
⊢ 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)
have 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)
Tactic: by_cases j_lt_n : j < n
-- 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
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)
⊢ 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)
have 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)
Tactic: by_cases j_lt_n : j < n
-- 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
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)
have j_minus : j - n < w.length
Tactic: have j_minus : j - n < w.length := by lia
-- 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
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
⊢ 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)
have n_le_j : n ≤ j
Tactic: have n_le_j : n ≤ j := le_of_not_gt j_lt_n
-- 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
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 * (n / p)) % p
have rw : (j - n) % p = (j - n) % p
Tactic: rw [Nat.mul_div_cancel' dvd]
-- 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
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
have p₁ : (j - n) % p = (j - p * (n / p)) % 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)
-- 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
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
⊢ 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)
have j_mod : (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)
-- 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
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
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w ((j - n) % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (j % p)
have rw : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (j % p) =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (j % p)
Tactic: rw [j_mod]
-- 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
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
⊢ 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)
have n₁ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (j - (take n w).length) =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (j - n)
Tactic: calc
        (take n w ++ w)[j]? = w[j - (take n w).length]? := getElem?_append_right (by simp_all)
        _ = w[j - n]? := by simp_all
        _ = w[(j - n) % p]? := Eq.symm (mod_w (j - n) (by lia))
        _ = w[j % p]? := by rw [j_mod]
-- 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
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
n₁ :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (j - (take n w).length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (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)
have n₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w ((j - n) % p) =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (j % p)
Tactic: calc
        (take n w ++ w)[j]? = w[j - (take n w).length]? := getElem?_append_right (by simp_all)
        _ = w[j - n]? := by simp_all
        _ = w[(j - n) % p]? := Eq.symm (mod_w (j - n) (by lia))
        _ = w[j % p]? := by rw [j_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
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
⊢ 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_p : ∀ j < n + w.length,
  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: have mod_p : ∀ j < n + length w, (take n w ++ w)[j]? = w[j % p]? := by
    intro j less_j
    by_cases j_lt_n : j < n
    · -- indices within `take n w` can be reduced due to the period of `w`
      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))
    · -- larger indices are indices of `w` decreased by `n`
      have j_minus : j - n < w.length := by lia
      have n_le_j : n ≤ j := le_of_not_gt j_lt_n; clear j_lt_n;
      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)
      calc
        (take n w ++ w)[j]? = w[j - (take n w).length]? := getElem?_append_right (by simp_all)
        _ = w[j - n]? := by simp_all
        _ = w[(j - n) % p]? := Eq.symm (mod_w (j - n) (by lia))
        _ = w[j % p]? := by rw [j_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
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
mod_p :
  ∀ j < n + w.length,
    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)
⊢ i % p < n + w.length
have this : i % p < p
Tactic: have : i % p < p := mod_lt i p_pos
-- 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
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
mod_p :
  ∀ j < n + w.length,
    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)
this : i % p < p
⊢ i % p < n + w.length
have this₁ : p ≤ n
Tactic: have : p ≤ n := le_of_dvd pos dvd
-- 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
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
mod_p :
  ∀ j < n + w.length,
    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) i =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n w ++ w) (i % p)
have less_mod : i % p < n + w.length
Tactic: have less_mod : i % p < n + w.length := by
    have : i % p < p := mod_lt i p_pos; have : p ≤ n := le_of_dvd pos dvd; lia
-- 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
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
mod_p :
  ∀ j < n + w.length,
    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)
less_mod : i % p < 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)
have inr : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n w ++ w) (i % p)
Tactic: rw [mod_p i less_i, mod_p (i % p) less_mod, mod_mod]
-- 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
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
mod_p :
  ∀ j < n + w.length,
    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)
less_mod : i % p < n + w.length
inr :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n w ++ w) (i % p)
⊢ 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 inr₁ : 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: rw [mod_p i less_i, mod_p (i % p) less_mod, mod_mod]
-- 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
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
mod_p :
  ∀ j < n + w.length,
    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)
less_mod : i % p < n + w.length
inr :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n w ++ w) (i % p)
inr₁ :
  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) (take n w ++ w) i =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n w ++ w) (i % p)
have inr₂ : 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_p i less_i, mod_p (i % p) less_mod, mod_mod]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
q k : ℕ
w : List α
per_q : w.HasPeriod q
per_plus : w.HasPeriod (k + q)
⊢ (drop q w).HasPeriod k
have rw : ∀
  (per_q :
    ∀ i < w.length - q,
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
        getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i + q))
  (per_plus :
    ∀ i < w.length - (k + q),
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
        getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i + (k + q))),
  ∀ i < (drop q w).length - k,
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop q w) i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop q w) (i + k)
Tactic: rw [hasPeriod_iff_getElem?] at per_plus per_q ⊢
Cleared hypotheses: per_q, per_plus
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
q k : ℕ
w : List α
per_q :
  ∀ i < w.length - q,
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i + q)
per_plus :
  ∀ i < w.length - (k + q),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i + (k + q))
⊢ ∀ i < (drop q w).length - k,
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop q w) i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop q w) (i + k)
have simp : ∀ i < w.length - q - k,
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (q + i) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (q + (i + k))
Tactic: simp only [length_drop, getElem?_drop]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
⊢ w.HasPeriod (p.gcd q)
have inl : ∀ (per_p : w.HasPeriod 0) (len : 0 + q - Nat.gcd 0 q ≤ w.length), w.HasPeriod (Nat.gcd 0 q)
Tactic: rcases Nat.eq_zero_or_pos p with rfl | p_pos
Cleared hypotheses: p, per_p, len
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
inl : ∀ (per_p : w.HasPeriod 0) (len : 0 + q - Nat.gcd 0 q ≤ w.length), w.HasPeriod (Nat.gcd 0 q)
⊢ w.HasPeriod (p.gcd q)
have inr : ∀ (p_pos : p > 0), w.HasPeriod (p.gcd q)
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
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
⊢ w.HasPeriod (p.gcd q)
have inr : ∀ (per_q : w.HasPeriod 0) (len : p + 0 - p.gcd 0 ≤ w.length), w.HasPeriod (p.gcd 0)
Tactic: rcases Nat.eq_zero_or_pos q with rfl | q_pos
Cleared hypotheses: q, per_q, len
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
inr : ∀ (per_q : w.HasPeriod 0) (len : p + 0 - p.gcd 0 ≤ w.length), w.HasPeriod (p.gcd 0)
⊢ w.HasPeriod (p.gcd q)
have inr₁ : ∀ (q_pos : q > 0), w.HasPeriod (p.gcd q)
Tactic: rcases Nat.eq_zero_or_pos q with rfl | q_pos
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.lt
⊢ w.HasPeriod (p.gcd q)
have p_lt_q : p < q
Tactic: have p_lt_q := Nat.compare_eq_lt.mp hyp
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
⊢ w.HasPeriod (p.gcd q)
have q_lt_p : q < p
Tactic: have q_lt_p : q < p := Nat.compare_eq_gt.mp hyp
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
⊢ p.gcd q < p
have this : p.gcd q ≠ p
Tactic: have : p.gcd q ≠ p := by
          simp [gcd_eq_left_iff_dvd, not_dvd_of_pos_of_lt q_pos q_lt_p]
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
⊢ w.HasPeriod (p.gcd q)
have gcd_lt_p : p.gcd q < p
Tactic: have gcd_lt_p : p.gcd q < p := by
        have : p.gcd q ≠ p := by
          simp [gcd_eq_left_iff_dvd, not_dvd_of_pos_of_lt q_pos q_lt_p]
        exact this.lt_of_le (gcd_le_left q p_pos)
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
⊢ (drop q w).HasPeriod (p - q)
have this : p = p - q + q
Tactic: have : p = (p - q) + q := by lia
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
⊢ w.HasPeriod (p.gcd q)
have per_diff : (drop q w).HasPeriod (p - q)
Tactic: have per_diff : HasPeriod (drop q w) (p - q) := by
        have : p = (p - q) + q := by lia
        exact per_q.drop_of_hasPeriod_add (this ▸ per_p)
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (goal)
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
⊢ (drop q w).HasPeriod q
have apply : (take q w ++ drop q w ++ []).HasPeriod q
Tactic: apply @HasPeriod.factor _ (take q w) (drop q w) [] q
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
⊢ w.HasPeriod (p.gcd q)
have per_q' : (drop q w).HasPeriod q
Tactic: have per_q' : HasPeriod (drop q w) q := by
        apply @HasPeriod.factor _ (take q w) (drop q w) [] q
        all_goals simp_all
-- Lean 4 proof step from Mathlib.Data.List.PeriodicityLemma (hypothesis)
Goal:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
⊢ w.HasPeriod (p.gcd q)
have gcd_stable : (p - q).gcd q = p.gcd q
Tactic: have gcd_stable : (p - q).gcd q = p.gcd q := gcd_sub_self_left (le_of_lt q_lt_p)