awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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:
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_minus : j - n < w.length
n_le_j : n ≤ j
j_mod : (j - n) % p = j % p
⊢ 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_minus : j - n < w.length
n_le_j : n ≤ j
j_mod : (j - n) % p = j % p
rw 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)
⊢ 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:
rw [j_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
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)
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)
⊢ 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]? = 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]

Premises used: List.getElem?_append_right, HSub.hSub, Eq.symm, List.take, List.length, 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 < 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]
-- 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
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 < p

Tactic:
have : i % p < p := mod_lt i p_pos
-- 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
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
⊢ p ≤ n

Tactic:
have : p ≤ n := le_of_dvd pos dvd
-- 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
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_1 : i % p < p
this : p ≤ n
⊢ i % p < 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
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

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
-- 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
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)
inr₂ 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)
⊢ 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 [mod_p i less_i, mod_p (i % p) less_mod, mod_mod]

Premises used: Nat.mod_mod, HMod.hMod
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
q k : ℕ
w : List α
per_q : w.HasPeriod q
per_plus : w.HasPeriod (k + q)
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)
⊢ (drop q w).HasPeriod k

Tactic:
rw [hasPeriod_iff_getElem?] at per_plus per_q ⊢

Premises used: List.hasPeriod_iff_getElem?
-- Module: Mathlib.Data.List.PeriodicityLemma
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))
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))
⊢ ∀ 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:
simp only [length_drop, getElem?_drop]

Premises used: List.getElem?_drop, List.length_drop
-- Module: Mathlib.Data.List.PeriodicityLemma
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 : ℕ
i_lt : 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 (i + q)

Tactic:
congrArg (getElem? w) (add_comm q i)

Premises used: congrArg, add_comm, GetElem?.getElem?
-- Module: Mathlib.Data.List.PeriodicityLemma
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 : ℕ
i_lt : i < w.length - q - k
⊢ i < w.length - q

Tactic:
lia
-- Module: Mathlib.Data.List.PeriodicityLemma
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 : ℕ
i_lt : i < w.length - q - k
⊢ i < w.length - (k + q)

Tactic:
lia
-- Module: Mathlib.Data.List.PeriodicityLemma
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 : ℕ
i_lt : i < w.length - q - k
⊢ i + (k + q) = q + (i + k)

Tactic:
lia
-- Module: Mathlib.Data.List.PeriodicityLemma
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 : ℕ
i_lt : 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:
calc
     w[q + i]? = w[i + q]? := congrArg (getElem? w) (add_comm q i)
     _ = w[i]? := (per_q i (by lia)).symm
     _ = w[i + (k + q)]? := per_plus i (by lia)
     _ = w[q + (i + k)]? := congr_arg (getElem? w) (by lia)

Premises used: congrArg, add_comm, congr_arg, HAdd.hAdd, GetElem?.getElem?, Eq.symm
-- Module: Mathlib.Data.List.PeriodicityLemma
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)
inr : ∀ (p_pos : p > 0), w.HasPeriod (p.gcd q)
⊢ w.HasPeriod (p.gcd q)

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
w : List α
q : ℕ
per_q : w.HasPeriod q
per_p : w.HasPeriod 0
len : 0 + q - Nat.gcd 0 q ≤ w.length
⊢ w.HasPeriod (Nat.gcd 0 q)

Tactic:
simp_all [HasPeriod]

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

Tactic:
rcases Nat.eq_zero_or_pos q with rfl | q_pos

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

Tactic:
simp_all
-- Module: Mathlib.Data.List.PeriodicityLemma
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
⊢ p < q

Tactic:
have p_lt_q := Nat.compare_eq_lt.mp hyp
-- Module: Mathlib.Data.List.PeriodicityLemma
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
p_lt_q : p < q
⊢ w.HasPeriod (p.gcd q)

Tactic:
exact (gcd_comm q p ▸ per_q.gcd) per_p (add_comm p q ▸ len)
-- Module: Mathlib.Data.List.PeriodicityLemma
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.eq
⊢ w.HasPeriod (p.gcd q)

Tactic:
simpa [(Nat.compare_eq_eq).mp hyp]

Premises used: Nat.compare_eq_eq, Iff.mp
-- Module: Mathlib.Data.List.PeriodicityLemma
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 < p

Tactic:
have q_lt_p : q < p := Nat.compare_eq_gt.mp hyp
-- Module: Mathlib.Data.List.PeriodicityLemma
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

Tactic:
simp [gcd_eq_left_iff_dvd, not_dvd_of_pos_of_lt q_pos q_lt_p]

Premises used: Nat.not_dvd_of_pos_of_lt, Nat.gcd_eq_left_iff_dvd
-- Module: Mathlib.Data.List.PeriodicityLemma
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

Tactic:
have : p.gcd q ≠ p := by
          simp [gcd_eq_left_iff_dvd, not_dvd_of_pos_of_lt q_pos q_lt_p]
-- Module: Mathlib.Data.List.PeriodicityLemma
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
this : p.gcd q ≠ p
⊢ p.gcd q < p

Tactic:
this.lt_of_le (gcd_le_left q p_pos)

Premises used: Ne.lt_of_le, Nat.gcd_le_left
-- Module: Mathlib.Data.List.PeriodicityLemma
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
this : p.gcd q ≠ p
⊢ p.gcd q < p

Tactic:
exact this.lt_of_le (gcd_le_left q p_pos)

Premises used: Ne.lt_of_le, Nat.gcd_le_left
-- Module: Mathlib.Data.List.PeriodicityLemma
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

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)
-- Module: Mathlib.Data.List.PeriodicityLemma
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
⊢ p = p - q + q

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

Tactic:
have : p = (p - q) + q := by lia
-- Module: Mathlib.Data.List.PeriodicityLemma
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
this : p = p - q + q
⊢ (drop q w).HasPeriod (p - q)

Tactic:
per_q.drop_of_hasPeriod_add (this ▸ per_p)

Premises used: List.HasPeriod.drop_of_hasPeriod_add, Eq.rec
-- Module: Mathlib.Data.List.PeriodicityLemma
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
this : p = p - q + q
⊢ (drop q w).HasPeriod (p - q)

Tactic:
exact per_q.drop_of_hasPeriod_add (this ▸ per_p)

Premises used: List.HasPeriod.drop_of_hasPeriod_add
-- Module: Mathlib.Data.List.PeriodicityLemma
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)

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)
-- Module: Mathlib.Data.List.PeriodicityLemma
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)
apply : (take q w ++ drop q w ++ []).HasPeriod q
⊢ (drop q w).HasPeriod q

Tactic:
apply @HasPeriod.factor _ (take q w) (drop q w) [] q

Premises used: List.HasPeriod.factor
-- Module: Mathlib.Data.List.PeriodicityLemma
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)
⊢ (take q w ++ drop q w ++ []).HasPeriod q

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

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

Tactic:
have per_q' : HasPeriod (drop q w) q := by
        apply @HasPeriod.factor _ (take q w) (drop q w) [] q
        all_goals simp_all
-- Module: Mathlib.Data.List.PeriodicityLemma
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
⊢ (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)
-- Module: Mathlib.Data.List.PeriodicityLemma
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
gcd_stable : (p - q).gcd q = p.gcd q
rw : q ≤ w.length - q
⊢ q ≤ (drop q w).length

Tactic:
rw [length_drop]

Premises used: List.length_drop
-- Module: Mathlib.Data.List.PeriodicityLemma
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
gcd_stable : (p - q).gcd q = p.gcd q
rw : (p - q).gcd q ≤ p - q
⊢ p.gcd q ≤ p - q

Tactic:
rw [← gcd_stable]
-- Module: Mathlib.Data.List.PeriodicityLemma
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
gcd_stable : (p - q).gcd q = p.gcd q
apply : 0 < p - q
⊢ (p - q).gcd q ≤ p - q

Tactic:
apply gcd_le_left q

Premises used: Nat.gcd_le_left
-- Module: Mathlib.Data.List.PeriodicityLemma
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
gcd_stable : (p - q).gcd q = p.gcd q
⊢ 0 < p - q

Tactic:
lia