awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Palindrome
Goal:
α : Type u_1
l : List α
a : (l ++ l.reverse).reverse = l ++ l.reverse
⊢ (l ++ l.reverse).Palindrome

Tactic:
apply of_reverse_eq

Premises used: List.Palindrome.of_reverse_eq
-- Module: Mathlib.Data.List.Palindrome
Goal:
α : Type u_1
l : List α
a : l.reverse.reverse ++ l.reverse = l ++ l.reverse
a₁ a₂ : l ++ l.reverse = l ++ l.reverse
⊢ (l ++ l.reverse).reverse = l ++ l.reverse

Tactic:
rw [reverse_append, reverse_reverse]

Premises used: List.reverse_reverse, List.reverse_append
-- Module: Mathlib.Data.List.Palindrome
Goal:
α : Type u_1
β : Type u_2
l : List α
f : α → β
p : l.Palindrome
rw : map f l.reverse = map f l
rw₁ rw₂ : map f l = map f l
⊢ (map f l).reverse = map f l

Tactic:
rw [← map_reverse, p.reverse_eq]

Premises used: List.Palindrome.reverse_eq, List.map_reverse
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p : ℕ
w : List α
mp :
  w.HasPeriod p →
    ∀ 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)
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)) →
    w.HasPeriod p
⊢ w.HasPeriod p ↔
    ∀ 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:
constructor
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p : ℕ
w : List α
pref : w <+: take p w ++ w
j : ℕ
len : j < w.length - p
⊢ j < w.length

Tactic:
lia
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p : ℕ
w : List α
pref : w <+: take p w ++ w
j : ℕ
len : j < w.length - p
⊢ j < w.length

Tactic:
have i1 : j < w.length := by lia
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p : ℕ
w : List α
pref : w <+: take p w ++ w
j : ℕ
len : j < w.length - p
i1 : j < w.length
⊢ j + p < w.length

Tactic:
lia
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p : ℕ
w : List α
pref : w <+: take p w ++ w
j : ℕ
len : j < w.length - p
i1 : j < w.length
⊢ j + p < w.length

Tactic:
have i2 : j + p < w.length := by lia
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p : ℕ
w : List α
pref : w <+: take p w ++ w
j : ℕ
len : j < w.length - p
i1 : j < w.length
i2 : j + p < w.length
⊢ p < w.length

Tactic:
lia
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p : ℕ
w : List α
pref : w <+: take p w ++ w
j : ℕ
len : j < w.length - p
i1 : j < w.length
i2 : j + p < w.length
⊢ p < w.length

Tactic:
have min : p < w.length := by lia
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p : ℕ
w : List α
pref : w <+: take p w ++ w
j : ℕ
len : j < w.length - p
i1 : j < w.length
i2 : j + p < w.length
min : p < w.length
⊢ j + p - (take p w).length = j

Tactic:
simp_all [min_eq_left_of_lt]

Premises used: min_eq_left_of_lt
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p : ℕ
w : List α
pref : w <+: take p w ++ w
j : ℕ
len : j < w.length - p
i1 : j < w.length
i2 : j + p < w.length
min : p < w.length
⊢ j + p - (take p w).length = j

Tactic:
have : j + p - (List.take p w).length = j := by
      simp_all [min_eq_left_of_lt]
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p : ℕ
w : List α
pref : w <+: take p w ++ w
j : ℕ
len : j < w.length - p
i1 : j < w.length
i2 : j + p < w.length
min : p < w.length
this : j + p - (take p w).length = j
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w j =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (j + p)

Tactic:
simp_all [getElem_append_right, IsPrefix.getElem pref, min_eq_left_of_lt]

Premises used: min_eq_left_of_lt, List.IsPrefix.getElem, List.getElem_append_right
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p : ℕ
w : List α
lhs :
  ∀ 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)
simp :
  ∀ (i : ℕ) (h : i < w.length - p),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
      some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (p + i) ⋯)
⊢ drop p w <+: w

Tactic:
simp only [prefix_iff_getElem?, length_drop, getElem_drop]

Premises used: List.length_drop, List.getElem_drop, List.prefix_iff_getElem?
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p : ℕ
w : List α
lhs :
  ∀ 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)
i : ℕ
leni : i < w.length - p
⊢ i + p < w.length

Tactic:
lia
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p : ℕ
w : List α
lhs :
  ∀ 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)
i : ℕ
leni : i < w.length - p
⊢ i + p < w.length

Tactic:
have len : i + p < w.length := by lia
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p : ℕ
w : List α
lhs :
  ∀ 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)
i : ℕ
leni : i < w.length - p
len : i + p < w.length
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
    some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (p + i) ⋯)

Tactic:
simp_all only [getElem?_pos, add_comm p i]

Premises used: add_comm, getElem?_pos
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p : ℕ
w : List α
lhs :
  ∀ 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)
⊢ drop p w <+: w

Tactic:
have drop : drop p w <+: w := by
      simp only [prefix_iff_getElem?, length_drop, getElem_drop]
      intro i leni
      have len : i + p < w.length := by lia
      simp_all only [getElem?_pos, add_comm p i]
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p : ℕ
w : List α
lhs :
  ∀ 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)
drop : List.drop p w <+: w
⊢ take p w ++ List.drop p w <+: take p w ++ w

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

Premises used: List.prefix_append_right_inj, List.take
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p : ℕ
w : List α
lhs :
  ∀ 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)
drop : take p w ++ List.drop p w <+: take p w ++ w
⊢ w <+: take p w ++ w

Tactic:
simp_all
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
w : List α
⊢ w.HasPeriod 0

Tactic:
simp [HasPeriod]

Premises used: List.HasPeriod
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
w : List α
p : ℕ
large : w.length ≤ p
⊢ w <+: take p w ++ w

Tactic:
simp_all [(take_eq_self_iff w).mpr large]

Premises used: Iff.mpr, List.take_eq_self_iff
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p : ℕ
⊢ HasPeriod.{u_1} (α := α) [] p

Tactic:
simp
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
pos :
  ∀ (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
neg :
  ∀ (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
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w (i % p) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i

Tactic:
by_cases p_zero : p = 0
-- Module: Mathlib.Data.List.PeriodicityLemma
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
pos₁ pos₂ :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
    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

Tactic:
rw [p_zero, mod_zero]

Premises used: Nat.mod_zero
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : ¬p = 0
small : i < p
⊢ i % p = i

Tactic:
have eq : i % p = i := mod_eq_of_lt small
-- Module: Mathlib.Data.List.PeriodicityLemma
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
neg neg₁ :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) w i =
    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

Tactic:
rw [eq]
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
⊢ i - p < w.length

Tactic:
lia
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
⊢ i - p < w.length

Tactic:
have len' : i - p < w.length := by lia
-- Module: Mathlib.Data.List.PeriodicityLemma
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) % 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'
-- Module: Mathlib.Data.List.PeriodicityLemma
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)
⊢ ∀ 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

Premises used: List.hasPeriod_iff_getElem?
-- Module: Mathlib.Data.List.PeriodicityLemma
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)
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)
⊢ i < w.length

Tactic:
rw [hasPeriod_iff_getElem?] at per

Premises used: List.hasPeriod_iff_getElem?
-- Module: Mathlib.Data.List.PeriodicityLemma
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)
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 = 0

Tactic:
rw [hasPeriod_iff_getElem?] at per

Premises used: List.hasPeriod_iff_getElem?
-- Module: Mathlib.Data.List.PeriodicityLemma
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)
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
⊢ p ≤ i

Tactic:
rw [hasPeriod_iff_getElem?] at per

Premises used: List.hasPeriod_iff_getElem?
-- Module: Mathlib.Data.List.PeriodicityLemma
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)
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
⊢ i - p < w.length

Tactic:
rw [hasPeriod_iff_getElem?] at per

Premises used: List.hasPeriod_iff_getElem?
-- Module: Mathlib.Data.List.PeriodicityLemma
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)
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
⊢ 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:
rw [hasPeriod_iff_getElem?] at per

Premises used: List.hasPeriod_iff_getElem?
-- Module: Mathlib.Data.List.PeriodicityLemma
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)
⊢ i - p < w.length - p

Tactic:
lia
-- Module: Mathlib.Data.List.PeriodicityLemma
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)
⊢ i - p < w.length - p

Tactic:
have minus : i - p < w.length - p := by lia
-- Module: Mathlib.Data.List.PeriodicityLemma
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 - p + p)

Tactic:
have per' := per (i - p) minus
-- Module: Mathlib.Data.List.PeriodicityLemma
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

Tactic:
simp only [large, Nat.sub_add_cancel] at per'

Premises used: Nat.sub_add_cancel
-- Module: Mathlib.Data.List.PeriodicityLemma
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
⊢ i % p = (i - p) % p

Tactic:
have mod : i % p = (i - p) % p := mod_eq_sub_mod large
-- Module: Mathlib.Data.List.PeriodicityLemma
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
mod : i % p = (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

Tactic:
aesop
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : ¬p = 0
⊢ 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

Premises used: Nat.sub_add_cancel, lt_or_ge, List.hasPeriod_iff_getElem?
-- Module: Mathlib.Data.List.PeriodicityLemma
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)
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
⊢ 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
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p : ℕ
w : List α
per : w.HasPeriod p
i : ℕ
len : 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:
Eq.symm (per.getElem?_mod p i w len)

Premises used: List.HasPeriod.getElem?_mod, Eq.symm
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
p : ℕ
w : List α
per : w.HasPeriod p
i : ℕ
len : 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:
exact Eq.symm (per.getElem?_mod p i w len)

Premises used: List.HasPeriod.getElem?_mod, Eq.symm
-- Module: Mathlib.Data.List.PeriodicityLemma
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)
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)
⊢ w.HasPeriod p

Tactic:
rw [hasPeriod_iff_getElem?]

Premises used: List.hasPeriod_iff_getElem?
-- Module: Mathlib.Data.List.PeriodicityLemma
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
⊢ i + p < w.length

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

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

Premises used: Nat.add_mod_right, HAdd.hAdd
-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
this :
  ∀ 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)
⊢ v.HasPeriod p

Tactic:
simpa [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
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)
⊢ v.HasPeriod p

Tactic:
suffices ∀ j < v.length - p, v[j]? = v[j + p]? by simpa [hasPeriod_iff_getElem?]